Repository navigation

feat(proofs): query kernel assumptions for every compiled witness (#131) - #132

Merged

hyperpolymath merged 58 commits into

mainfrom

arena/a9dee430-nextgen-typing

Nov 2, 2026

Merged

feat(proofs): query kernel assumptions for every compiled witness (#131)#132
hyperpolymath merged 58 commits into
mainfrom
arena/a9dee430-nextgen-typing

Commits on Nov 1, 2026
- ci(proofs): gate verification/proofs/ with the real all-proofs target
  
  Arena Agent
  and
  arena-agent
  committed
  3d0c6b8
- ci(proofs): annotate proof failures so the failing module is visible
  
  Arena Agent
  and
  arena-agent
  committed
  7325e73
- ci(proofs): annotate only the log tail (GitHub caps 10 annotations per step)
  
  Arena Agent
  and
  arena-agent
  committed
  8d3744b
- ci(proofs): attach the whole failure tail as one newline-encoded annotation
  
  Arena Agent
  and
  arena-agent
  committed
  5a05924
- fix(proofs): resolve the repo's Agda library manifest in proof-check-agda
  
  Arena Agent
  and
  arena-agent
  committed
  f2efcdd
- fix(proofs): activate the repo's Agda library by name, and register it in CI
  
  Arena Agent
  and
  arena-agent
  committed
  4c6b918
- docs(proofs): record the enforcement that now exists, from actual receipts
  
  Arena Agent
  and
  arena-agent
  committed
  a267d58
- Update scripts/check-proof-enrolment.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  ebc14c6
- Update scripts/check-proof-enrolment.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  5e97ae4
- Update scripts/proof-scan-dangerous.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  8356cb6
- docs(proofs): Document helper behavior and error handling in proof scripts and CI
  coderabbitai[bot]
  committed
  ebe0fe4
- proof: audit the ledger and compile declared Rocq/Lean recheck legs
  
  Arena Agent
  and
  arena-agent
  committed
  6c609c4
- proof: make the controls' and ledger's counts visible as annotations
  
  Arena Agent
  and
  arena-agent
  committed
  c4baf54
- proof: substantiate the grade-3 rung and check the ladder's edges
  
  Arena Agent
  and
  arena-agent
  committed
  112a7bf
- docs: pin the grade-3 substantiation to its receipt (run 41314202374)
  
  Arena Agent
  and
  arena-agent
  committed
  3cd1859
- Update .github/workflows/proof-ci.yml
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  1616778
- Update .github/workflows/proof-ci.yml
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  605e12f
- Update PROOF-NEEDS.adoc
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  8721d6a
- Update scripts/check-coordination-boundary.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  d9b2048
- Update tests/proofs/run-controls.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  9838772
- docs(proofs): reconcile the 2026-10-12 ruling and pin the policy it defers to
  
  Arena Agent
  and
  arena-agent
  committed
  759a33e
- feat(proofs): record the trust base beyond this repo, and pin the authority
  
  Arena Agent
  and
  arena-agent
  committed
  b20c279
- docs(proofs): state XP-1's scope — it does not prove echo-types' identity claim
  
  Arena Agent
  and
  arena-agent
  committed
  a0ad1e9
- fix(descriptiles): hexad is not a format and logtalk is not a report format
  
  Arena Agent
  and
  arena-agent
  committed
  be4e51d
- docs(proofs): changelog entry for the 2026-11-01 reconciliation
  
  Arena Agent
  and
  arena-agent
  committed
  d67c337
- feat(proofs): meet mathesis §5/§6 explicitly, clause by clause
  
  Arena Agent
  and
  arena-agent
  committed
  0caf3dd
- docs(proofs): reconcile five proof authorities, and comply with the trusted-base policy
  
  Arena Agent
  and
  arena-agent
  committed
  1db1175
- docs(decisions): point the reconciliation record at the filed upstream issues
  
  Arena Agent
  and
  arena-agent
  committed
  b363509
- proof(agda): corroborate XP-1 under a second Agda, and keep it out of the receipt
  
  Arena Agent
  and
  arena-agent
  committed
  deac507
- proof(ledger): separate sibling formalisations from assumptions and from evidence
  
  Arena Agent
  and
  arena-agent
  committed
  cfbc7b7
- chore(proofs): move agda-stdlib to the latest stable (v2.3 -> v2.4), with evidence
  
  Arena Agent
  and
  arena-agent
  committed
  f42ac27
- fix(proofs): pin agda-stdlib v2.4 to the commit, not the annotated tag object
  
  Arena Agent
  and
  arena-agent
  committed
  6733cee
- Update docs/proof-debt.md
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  d912b78
- Update scripts/check-proof-ledger.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  f2ba299
- Update tests/proofs/run-ledger-controls.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  4c1cbc4
- Update scripts/check-proof-ledger.sh
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  f64b641
- fix(proofs): make control 24 test the rule, not a field-shift accident
  
  Arena Agent
  and
  arena-agent
  committed
  0a8ac46
- chore(ci): temporary diagnostic for action-lock coverage step (removed before merge)
  
  Arena Agent
  and
  arena-agent
  committed
  71e98f9
- chore(ci): retry diagnostic trigger (push-only, arena branches)
  
  Arena Agent
  and
  arena-agent
  committed
  6d31b6e
- chore(ci): temporary verify-local diagnostic inside workflow-linter (reverted before merge)
  
  Arena Agent
  and
  arena-agent
  committed
  efe7e41
- fix(ci): move the actions-lock pin to v0.4.0 so it can read lockfile v0.0.3
  
  Arena Agent
  and
  arena-agent
  committed
  433dff2
- fix(ci): force HTTPS on the toolchain downloads rather than inherit it
  
  Arena Agent
  and
  arena-agent
  committed
  273cea4
- fix(proofs): reach Coq's admit. and stop accepting PROOF-NEEDS as the register
  
  Arena Agent
  and
  arena-agent
  committed
  06ac66a
- fix(proofs): refuse a proven leg whose prover the lane cannot compile
  
  Arena Agent
  and
  arena-agent
  committed
  330c7a5
- fix(proofs): a waiver record must resolve, or it is an obligation removed silently
  
  Arena Agent
  and
  arena-agent
  committed
  10a418d
- fix(proofs): compare documented grades theorem by theorem, not repository-wide
  
  Arena Agent
  and
  arena-agent
  committed
  b6fd240
- fix(proofs): make the admit fixture declare itself so the boundary keeps holding
  
  Arena Agent
  and
  arena-agent
  committed
  47ebe32
- fix(proofs): close four small fail-open paths review found in the instrument
  
  Arena Agent
  and
  arena-agent
  committed
  90a64ba
- fix(proofs): strip comments per language, and stop posting a payload the API rejects
  
  Arena Agent
  and
  arena-agent
  committed
  8e8eaee
- docs(proofs): say which axiom queries the lane actually runs
  
  Arena Agent
  and
  arena-agent
  committed
  7138da2
- fix(proofs): Lean has no `//` comment, and pin the anchor a waiver cites
  
  Arena Agent
  and
  arena-agent
  committed
  733a7af
- feat(proofs): query kernel assumptions for every compiled witness (#131)
  
  hyperpolymath
  and
  arena-agent
  committed
  f69b430
- ci(proofs): surface proof-controls and agda logs in failure annotations
  
  hyperpolymath
  and
  arena-agent
  committed
  58ad6a4
- fix(proofs): resolve Nametab-shortened Rocq stdlib axiom names against coqchk KerNames
  
  hyperpolymath
  and
  arena-agent
  committed
  5f62d66
- Update verification/proofs/agda/MANIFEST
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  e8abc4a
- Update verification/proofs/README.adoc
  
  hyperpolymath
  and
  coderabbitai[bot]
  authored
  809dd12
- docs(proofs): document shell helper behavior and correct scanner comments
  coderabbitai[bot]
  committed
  dabdff9
Commits on Nov 2, 2026
- fix(proofs): tighten Admitted/manifest-order/ledger gates per PR #132 review
  
  hyperpolymath
  and
  arena-agent
  committed
  611e650

Commits

Commits on Nov 1, 2026

Commits on Nov 2, 2026