Repository navigation
proofs(agda): the wager experiment, stages 5 to 7 (T6, T7, the cross-check) and the final verdict - #89
Merged
Conversation
Add the Stage 5 statements to Wager/Statements.agda as types: for each nominal coercion of the source the two translated types have one normal form (T6), the coercion becomes conversion, and no term remains. The statements are frozen from this commit. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
Give the inhabitants of the Stage 5 statements: - T6: for each nominal coercion of the source, the two translated types have one normal form; - the coercion becomes conversion of the target; - no term remains: the translation of a cast along a nominal coercion is the translation of the term under the cast. The proof of the first two statements is the lemma that Stage 4 needed for the typing of a cast. Add accepted and rejected closed examples. One example shows that the converse of T6 is false for the row scheme. Record the design choices DC-5.1 and DC-5.2, the ledger notes, the gate watch and the draft verdict for Stage 5. The Agda gate now has 65 modules. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 3 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
hyperpolymath
marked this pull request as ready for review
November 10, 2026 10:55
hyperpolymath
enabled auto-merge (squash)
November 10, 2026 10:55
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Owner
Author
CI status at
|
| Check | Cause | Fix |
|---|---|---|
Validate K9 contracts |
11 errors in 18 scanned K9 files. The errors are in governance contracts and in template files that are not filled. | No fix exists yet. Proposed: fill or remove the template files, and add the signature field that the validator requires. |
Hypatia neurosymbolic scan |
6 critical and 4 high findings. The 10 error lines are: 6 x "Descriptile in retired location", 3 x "CI policy requires a retired descriptile path", 1 x dependabot-automerge.yml writes without contents: write. |
No fix exists yet. Proposed: move the descriptiles from .machine_readable/6a2/ to .machine_readable/descriptiles/ and update each reference to the old path. |
SonarQube |
The scanner cannot authenticate (the SONAR_TOKEN secret). The SonarCloud Code Analysis app check passes. |
No fix is possible in the repository files. The owner must set the secret or remove the job. |
Each proposed fix changes governance files (.a2ml, K9 contracts, workflows). This work has an instruction not to edit .a2ml files. For this reason the fixes are not in this pull request, and they wait for a decision of the owner.
Generated by Claude Code
… simply typed term Stage 6 (T7, local equality assumptions) has two options, and PLAN.adoc says that the owner makes the choice. This commit does not make the choice. It adds one lemma about the unchanged target calculus, which each of the two options needs. - `Wager.L2.Erasure.erT`: the erased type of a closed target type, read from the normal form. A trope state and a grade vanish. - `Wager.L2.Erasure.erase-typed`: if a target term has a type, then its erasure has the erased type in the untyped calculus. The lemma holds for each signature and each set of grade operations. - `Wager.L2.Erasure.identity-one-type`: a typed target term that erases to the identity function has an arrow type whose two sides have one erased type. The target has conversion only, so it has no hypothetical equality. T7 has no statement yet. `Statements.agda` and `Proofs.agda` do not change. The ledgers do not change: the lemma adds no relation and no rule to the target calculus. Records: MANIFEST and Everything (66 modules), the marker `gate:agda gated=66` and the Stage 6 row in PROOF-STATUS.adoc, the T7 row and the count of files with the silenced warning in VERDICT.adoc (37 of 66; a test without the flag found the warning in the new file). Local gates: check-proofs agda (66 modules), check-proof-status, scan-dangerous, check-root-shape, check-no-md-in-docs pass. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
The owner chose the two options of Stage 6, option 2 (a separation) first (DC-6.1). This commit has the definitions and the statement of the separation. It has no proof of the statement. - `Wager/Local/Source.agda`: the source calculus of Stage 6. It has base types, functions, sums and the type `⟨ τ ~ σ ⟩ ρ` of a GADT constructor field (a value with evidence of an equality). The match `lopen` brings the equality into scope as a local assumption. Erasure removes casts and evidence. - `Wager/Local/Gadt.agda`: the GADT `G` and the program `gadt-eval b α`, the function `eval` at the closed instance `a := α`. - `Wager/Statements.agda`: `T7-Statements.T7-Separation`. For each base type b and each closed type α, no typed target term has the erasure of `gadt-eval b α` together with a type that has the erased type of the source type. The statement is for each target signature and each set of grade operations. - `DESIGN-CHOICES.adoc`: DC-6.1 (the choice of the owner), DC-6.2 (a type is closed; the type variable of the task is an Agda variable), DC-6.3 (the source calculus), DC-6.4 (what "the target cannot type" means, and what the statement does not exclude). - MANIFEST and Everything (68 modules), the marker `gate:agda gated=68`. Local gates: check-proofs agda (68 modules), check-proof-status, scan-dangerous, check-root-shape pass. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
The statement `T7-Separation` was committed before this proof. It did not change. - `Wager/Local/Separation.agda`: the proof. The erasure of the program `gadt-eval b α` has no simple type `(p + p) → b`: the first branch uses the value at the type b, and the second branch uses the same value at a sum type. A typed target term erases to a term with a simple type (`Wager.L2.Erasure.erase-typed`). - `Wager/Proofs.agda`: `t7-separation`, for each target signature and each set of grade operations. - `Wager/Examples/Stage6.agda`: the program at two instances; the erased text does not depend on the instance; the first branch runs; with no assumption `Int ~ Int + Int` has no evidence; the instance of T7 for the signature of Stage 5; the identity function has no type `Int → Int + Int`. One accepted example shows what T7 does not exclude: a typed target term with the same erasure at another type of the data. What the theorem does not say (DC-6.4, VERDICT.adoc): it does not say "the program has no translation". It excludes a translation that keeps the erased type and the erased term. A type is closed in this development (DC-6.2), so the statement is about each closed instance of the program and not about a polymorphic program. Type safety of the source calculus of Stage 6 is not proved. Records: both ledgers (two relations of the class "source"; no entry for the target; the rule-diff ledger stays empty), TOOLCHAIN.adoc (gate watch: a false lemma, a `postulate` and a changed program each fail the gate), VERDICT.adoc (T7 part 1 PROVED, part 2 NOT ATTEMPTED; findings F17 and F18), DESIGN-CHOICES.adoc (identifiers for DC-6.2 and DC-6.4; audit of the silenced warning: 39 of 70 files), PROOF-STATUS.adoc (marker `gate:agda gated=70`, row of Stage 6), CHANGELOG.adoc. Audit at the end of the part: each of the 49 Agda identifiers that the new texts cite exists. 6 sentences said more than Agda checked, and they are corrected. Local gates: check-proofs agda (70 modules), check-proof-status, scan-dangerous, check-root-shape, check-no-md-in-docs pass. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
hyperpolymath
changed the title
…entity type The owner chose the two options of Stage 6, the separation first. Part 1 is done. This commit starts part 2: it has the definitions and the frozen statements, and no proof. Definitions (Wager/Identity): - Family.agda: the identity type as a family of base constants of a signature. `Id A B` is a base constant, `rfl A` is a literal of the base type `Id A A`. Equality evidence is now a term. - Term.agda: the term syntax of the target with one more former, `cast e t`, and two erasures: `keepⁱ` (the reference, which evaluates the evidence of each cast) and `eraseⁱ` (the evidence is absent). - Typing.agda: the target judgement with one new rule, `t-cast`, which uses the evidence at the grade 𝟘. Statements (Wager.Statements.T7-Identity-Statements): T7-Conservative, T7-Conservative-Erasure, T7-Intro, T7-Canonicity, T7-Erasure, T7-Erasure-First-Order, T7-Grade, T7-Assumption. DESIGN-CHOICES.adoc: DC-6.5 (the family), DC-6.6 (one former, one rule), DC-6.7 (what "erasure of its proofs is sound" means, and what is not done). The gate count is 73. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
…de 0 The statements were frozen in bf5122c. This commit has the proofs, one signature with an identity family, the examples and the records. Proved (Wager.Proofs, for each signature that has an identity family and each set of grade operations): - t7-erasure, t7-erasure-first-order: for a closed typed term, the reference program (which evaluates the evidence of each cast) and the program with no evidence in its casts evaluate to observationally equal values. - t7-intro, t7-canonicity: closed evidence for `Id A B` exists exactly when A and B are convertible. - t7-conservative, t7-conservative-erasure: the target is a part of the extension, with the same erasure. - t7-grade, t7-assumption (these two need the laws of a grade algebra): evidence costs nothing, and a local equality assumption is a variable at the grade 0. Wager/Identity/Instance.agda builds one signature that has a family. Wager/Examples/Stage6Identity.agda has accepted and rejected closed examples, and the GADT program of part 1 with data that holds the evidence. Limits (DESIGN-CHOICES.adoc DC-6.5 to DC-6.8, VERDICT.adoc): - Equality evidence is now a term. The verdict gives the trade and does not decide if the extension adds a relation: the owner decides. - The erasure removes the evidence of a cast and no other evidence. - The behaviour proof does not use the grade of the rule. A test with the grade 1 in the rule shows this. - No reduction relation, progress or preservation for the extension. - Not shown: that each signature has an extension with a family. Gate watch: 6 deliberate defects, each one FAIL, each one removed (TOOLCHAIN.adoc). Clean build: 76 modules, about 43 s, no warning. check-proofs.sh agda, scan-dangerous.sh and check-proof-status.sh pass. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
…ent cross-check The owner asked for the optional Stage 7 on 2026-11-10. Stages 1 to 5 are complete. This commit has the model and the frozen statements, and no proof. - Wager/Univalent/Model.agda: the interpretation of a closed target type in the cubical universe. A newtype instance is a wrapper `Box`, and `unboxEquiv : Box Z ≃ Z` is its transition. `𝓡` is the realisability relation, `Denotes` is the denotation of a term transformer, and `pathOf` is the path of a representational coercion, made from `ua unboxEquiv`, `sym`, composition and congruence. - Wager.Statements.Stage7-Statements: Coercion-Denotes-Transport, Coercion-Denotes-Transport-Back, Coerce-Function-Is-Transport. - DESIGN-CHOICES.adoc: DC-7.1 (the model), DC-7.2 (the denotation is by realisers, and why), DC-7.3 (the path). The gate count is 77. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
…verdict Stage 7. The statements were frozen in 75da545. - Wager/Univalent/CrossCheck.agda: in a realisability model of the target types in the cubical universe, where a newtype instance is a wrapper that is equivalent to its content, the translation of each representational coercion denotes transport along a path made with `ua` (coercion-denotes-transport, coercion-denotes-transport-back, coerce-function-is-transport). For each source signature that passes the role check, each state scheme, each grade algebra and each interpretation of the base constants. - Wager/Examples/Stage7.agda: transport along the path of `Age ~ Int` gives 7 from `box 7` by computation; congruence below a newtype; 2 rejected examples. - The denotation is by realisers. The development has no denotation of each typed term (DESIGN-CHOICES.adoc, DC-7.2). The final verdict (VERDICT.adoc). - W does not hold as written. W holds for the fragment with 2 additions: trope states with an index, and, for a whole program, a grade algebra with an unrestricted grade 1. - T0, T1, T3, T4, T6: PROVED. T2, T5: PROVED WITH CHANGE. T7: the two parts are PROVED. Stage 7: PROVED. - Two decisions are with the owner: the class of the kinding judgement (R1), and the class of the identity family of Stage 6, part 2. - A draft ADR text, not filed: 11 candidate obligations with no ET number, and 4 decisions for the owner. OBLIGATIONS.adoc is not changed. Records: RELATION-LEDGER (R25, specification only), RULE-DIFF-LEDGER, TOOLCHAIN (gate watch: 5 deliberate defects, each one FAIL), PROOF-STATUS, CHANGELOG. Clean build: 79 modules, about 48 s, no warning. check-proofs.sh agda, scan-dangerous.sh and check-proof-status.sh pass. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK
hyperpolymath
changed the title
hyperpolymath
disabled auto-merge
November 10, 2026 17:16
|
4 of 8 tasks
hyperpolymath
added a commit
that referenced
this pull request
Nov 10, 2026
## Summary Adds the v2 thin journal that STATE option B (ruled 2026-11-10) sends the journal sections of STATE v1 to. You said it is just a file in the repo, so this is that file: `docs/status/JOURNAL.adoc`. ## Changes - **`docs/status/JOURNAL.adoc` (new).** The five STATE v2 fields from `standards` `1-formats/templates/STATE.a2ml.v2.spec.adoc`: `phase`, `last_action`, `next_action`, `session_marker`, `updated`, plus a `Blockers` table. It is AsciiDoc, not the spec's `@state` block, because A2ML is retired and no new `.a2ml` may be created. - **`docs/practice/AI-CONVENTIONS.adoc`.** Session startup step 2 now reads the journal, so agents actually use it. STATE v1 is marked legacy. - **`systemet_chora.deed`.** Comments only: STATE's `[position] phase = "implementation"` now has a home (the journal's free-text `phase`), where the last PR left it as an open owner question. Milestones stay in `ROADMAP.adoc`. ## Where each field came from STATE v1 is stale (2026-07-29), and this repo has moved a lot since, so the journal is checked against primary sources. The file has a `Provenance` section saying which is which. - `phase`: `docs/status/PROOF-STATUS.adoc` (summary table and the ET-1/ET-2 rows). **ET-2 is closed for the β-fragment only**, which is more precise than STATE v1's wording. - `last_action` and the `wager-owner-decisions` blocker: the merge commit of #89 and `Wager/VERDICT.adoc` (R1, R23, R24 checked there). - `et-16-further-adr` blocker: `docs/theory/OBLIGATIONS.adoc` (ET-14, ET-16, ADR-0002). - `next_action` (the η-long normalizer `nfE`, issue #32) is in `PROOF-STATUS.adoc`, but that it is the *intended* next step is carried from STATE v1. `session_marker` asks you to confirm. - `state-archive-rewire` blocker: the archive step is blocked because `openssf-compliance.yml`, the Must invariant, `validate-template.sh`, the e2e test and the arrival-pack generator still require `STATE.a2ml`. ## Not carried, because stale STATE v1 listed two blockers I did not carry: issue 18 (the `descriptiles/6a2` migration, "blocked: contractiles.mjs needs Node, estate-denied") and issue 30 (the K9 gate "now real and red"). The migration is done (the ROADMAP records the pure renames), K9 is green on the last merged PR, and Node is not outright banned under the Bun > Deno > pnpm > npm order. ## Decision for you The journal says it **governs over** STATE v1's journal sections where they disagree, so the two don't double-track while STATE stays live. That is my reading of option B. Say so if you want it worded differently. ## RSR Quality Checklist ### Required - [ ] Tests pass — N/A: docs and comments only. - [ ] Code is formatted — N/A. - [ ] Linter is clean — `deed_lint.js` reports OK on the deed. - [x] No banned language patterns; no `unsafe`; no banned functions. - [x] SPDX headers present on the new file. - [x] No secrets, credentials, or `.env` files included. ### As Applicable - [ ] `.machine_readable/descriptiles/STATE.a2ml` updated — not changed (see above). - [x] Documentation updated. ## Testing - `deed_lint.js` → OK. - Every path the journal cites exists, including `Wager/VERDICT.adoc` and ADR-0002. - `scripts/check-root-shape.sh` and `scripts/check-no-md-in-docs.sh` → PASS. No `.a2ml` created. --- _Generated by [Claude Code](https://claude.ai/code/session_01J1XmMC49T8sZ3uUuvrgB7y)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The last stages of the wager experiment in Cubical Agda, and the final verdict. Stages 0 to 4 are in
mainsince pull requests 87 and 88.0. Equality evidence is a term.verification/proofs/agda/Wager/VERDICT.adocis final. It has a draft ADR text that is not filed.The result: W does not hold as written. W holds for the fragment with 2 additions.
𝟙is unrestricted. The translation of a coercion alone is typed in each grade algebra.T0, T1, T3, T4 and T6 are PROVED. T2 and T5 are PROVED WITH CHANGE. The two parts of T7 are PROVED. The cross-check of Stage 7 is PROVED.
Two decisions are with the owner: the class of the kinding judgement with a graded context (R1), and the class of the identity family of Stage 6, part 2 (R23, R24). The verdict gives the facts for each answer and does not decide.
The experiment claims no ET obligation. It does not change
docs/theory/OBLIGATIONS.adoc,AFFIRMATION.adocor any.a2mlfile.Changes
Stage 5
Wager/Statements.agda: the three statements of T6, committed before their inhabitants (T6,T6-Conversion,T6-No-Term).Wager/Proofs.agda:t6,t6-conversion,t6-no-term. The proof of the first two is the lemmaWager.Trans.Nominal.nominal-nfof Stage 4. That proof existed before the statements were written, andVERDICT.adocrecords this.Wager/Examples/Stage5.agda: accepted and rejected closed examples.Stage 6, part 1 (the separation)
Wager/L2/Erasure.agda:erase-typed(a typed target term erases to a term with a simple type) andidentity-one-type.Wager/Local/Source.agda,Wager/Local/Gadt.agda: a small source calculus with local equality assumptions, and one GADT program.T7-Separationand its prooft7-separation: for each closed instance of the program, no typed closed term of the target has the erasure of the program together with a type that has the erased type of the source type.Stage 6, part 2 (the identity type)
Wager/Identity/Family.agda: the identity type as a family of base constants of a signature.Id A Bis a base constant, andrfl Ais a literal of the base typeId A A. The type language and conversion do not change.Wager/Identity/Term.agda,Typing.agda: one new term former (cast e t) and one new rule (t-cast), which uses the evidence at the grade𝟘.Wager/Identity/Soundness.agdaandWager/Proofs.agda, for each signature that has a family and each set of grade operations:t7-erasure,t7-erasure-first-order: for a closed typed term, the program that evaluates the evidence of each cast and the program with no evidence in its casts evaluate to observationally equal values.t7-intro,t7-canonicity: closed evidence forId A Bexists exactly when A and B are convertible.t7-conservative,t7-conservative-erasure: the target is a part of the extension.t7-grade,t7-assumption(these two need the laws of a grade algebra): evidence costs nothing, and a local equality assumption is a variable at the grade𝟘.Wager/Identity/Instance.agda: one signature that has a family.Stage 7 (the optional cross-check)
Wager/Univalent/Model.agda: an interpretation of the closed target types in the cubical universe. A newtype instance is a wrapperBox, andunboxEquiv : Box Z ≃ Zis its transition.pathOfis the path of a representational coercion, made fromua unboxEquiv,sym, composition and congruence.Wager/Univalent/CrossCheck.agdaandWager/Proofs.agda:coercion-denotes-transport,coercion-denotes-transport-back,coerce-function-is-transport. The translation of each representational coercion denotes transport along its path.Wager/Examples/Stage7.agda: transport along the path ofAge ~ Intgives 7 frombox 7, by computation.Records
DESIGN-CHOICES.adoc(DC-5.1 to DC-7.3), both ledgers,TOOLCHAIN.adoc(a gate watch for each stage),VERDICT.adoc(final, findings F16 to F21, the trade of Stage 6, the draft ADR).docs/status/PROOF-STATUS.adoc: the markergate:agda gated=79and the rows for stages 5 to 7.CHANGELOG.adoc.RSR Quality Checklist
Required
just testor equivalent). Run in the session:scripts/check-proofs.sh agda(PASS, 79 modules),scripts/scan-dangerous.sh(PASS),scripts/check-proof-status.sh(PASS). Not run in the session: the Lean4 gate (no Lean toolchain there). CI runs it.UnsupportedIndexedMatch, DC-0.3).unsafeblocks without// SAFETY:comments (none exist).envfiles includedAs Applicable
STATE.a2mlupdated. Not done on purpose: this is a file of the owner.ECOSYSTEM.a2mlupdated. Not applicable.META.a2mlupdated. Not applicable: no ADR is filed.TOPOLOGY.mdupdated. Not applicable.CHANGELOGor release notes updatedTesting
TOOLCHAIN.adochas the records.7c7f1e0(T7, part 1),bf5122c(T7, part 2),75da545(Stage 7).VERDICT.adocrecords the exceptions.Wager/Proofs.agdaby a script.mainfor reasons outside this work are repaired in pull requests 90 and 92.Screenshots
Not applicable.
🤖 Generated with Claude Code
https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK