proof(L3): extend AST with TEcho + EEcho (L3 wiring slice 1)#190
Merged
hyperpolymath merged 1 commit intoMay 27, 2026
Merged
Conversation
…g slice 1) Foundation for L3 wiring (PROOF-NEEDS.md §2). Echo.v calculus (12 Qed, 0 admits) is already in place; this commit adds the surface AST needed before T_Observe and step-emission rules can land in subsequent slices. Changes (formal/Syntax.v) * New ty constructor TEcho : ty -> ty. The type of an echo value witnessing an irreversible step that erased a value of type T. Documented at PRESERVATION-DESIGN.md §6.3. * New expr constructor EEcho : ty -> expr -> expr. Runtime-only residue value, mirroring the ELoc pattern (no surface syntax). * New is_value constructor VEcho : echoes-of-values-are-values so S_Region_Exit / S_Drop can reduce to a normal form. * Cascade-mechanical updates: expr_free_of_region propagates into the witness sub-expression; shift / subst recurse into the witness; the witness type annotation T is closed. Cascade fixes * formal/Typing.v free_regions gains a TEcho T' => free_regions T' case (linear in the witness). * formal/Semantics_L1.v value_R_G_preserving_l1 gains a VEcho case closed by inversion (no L1 typing rule produces EEcho yet, so the hypothesis is vacuous in this slice). What is NOT in this slice (deliberately deferred per slice plan) * T_Observe typing rule (slice 2) * S_Region_Exit / S_Drop echo emission in step rules (slice 2) * G (echo context) threading through compound rules (slice 3) * preservation_l3 (slice 4) is_linear_ty is deliberately not extended — TEcho hits the catch- all returning false in this slice. The linearity discipline lives in the (forthcoming) T_Observe rule's modality dispatch, not in is_linear_ty. Revisit in slice 2 if the rule shape demands it. Build oracle * coqc 8.18.0 closes the full formal/ tree (Syntax / Typing / TypingL1 / Semantics / Semantics_L1 / Counterexample / TypingL2). * Net debt: unchanged on this branch (Semantics_L1.v: 23 Qed + 3 Admitted, all pre-existing). Refs PROOF-NEEDS.md §2 (L3 wiring). Refs PRESERVATION-DESIGN.md §6. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
merged commit a1abf47
into
proof/semantics-l1-affine-bullet-fix
4 of 13 checks passed
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
…ice 2) Slice 2 of 4 in the L3 wiring sequence. Slice 1 (PR #190) added the TEcho / EEcho AST surface; this slice adds the explicit observation rule that consumes an echo. Changes (formal/Syntax.v) * New expr constructor EObserve : expr -> expr. Surface-writable (unlike EEcho which is runtime-only). Modality dispatch lives in the typing rule, not the constructor. * Cascade-mechanical: expr_free_of_region, shift, subst all recurse into the sub-expression. Changes (formal/TypingL1.v) * New typing rule T_Observe_L1 : has_type_l1 m R G e (TEcho T) R' G' -> has_type_l1 m R G (EObserve e) (TBase TUnit) R' G'. Modality- polymorphic: fires in both Linear and Affine modes. What differs across modes is the OBLIGATION shape, not the rule: Linear discipline makes the echo a must-observe (an unobserved TEcho in scope is a typing failure); Affine permits implicit lowering (no T_Observe required). The mandatoriness is to be enforced via is_linear_ty TEcho or the implicit-drop discipline in a follow-up slice — the present rule is the necessary precondition. Cascade fixes (formal/Semantics_L1.v) * shift_typing_gen_l1_m: explicit T_Observe_L1 bullet (commutes with the witness sub-expression via the IH). * subst_typing_gen_l1_m: explicit T_Observe_L1 bullet (same shape). * region_shrink_preserves_typing_l1_gen_m: explicit T_Observe_L1 bullet added before Admitted (closes via IH; would otherwise be silently absorbed by the outer Admitted). * All other inductions (typing_preserves_bindings_l1, unrestricted_flag_unchanged_l1, count_occ_le_l1_m, region_liveness_at_split_l1_gen) absorb T_Observe_L1 via their existing catch-all patterns (T_Observe_L1 propagates the IH unchanged on G' and R' — no new structural obligation). What is NOT in this slice (deliberately deferred) * S_Region_Exit / S_Drop echo emission in step rules. The step relation lives in Semantics.v which is owner-touchy (CLAUDE.md Owner directive 2026-05-27 anti-pattern detector). Will escalate before slice 3. * G (echo context) threading through compound rules — slice 3 * preservation_l3 — slice 4 * is_linear_ty TEcho_ = true (mandatoriness enforcement) — follow-up Build oracle * coqc 8.18.0 closes the full formal/ tree. * Net debt unchanged on this branch (3 Admitted in Semantics_L1.v, all pre-existing from prior slices). Refs PROOF-NEEDS.md §2 (L3 wiring). Refs PRESERVATION-DESIGN.md §6.3. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
…ice 2) (#191) ## Summary Slice 2 of 4 in the L3 wiring sequence. [Slice 1 (#190)](../pull/190) added the `TEcho` / `EEcho` AST surface; this slice adds the explicit observation rule that consumes an echo. ## Changes (formal/Syntax.v) - New `expr` constructor `EObserve : expr -> expr`. Surface-writable (unlike `EEcho` which is runtime-only). - Cascade-mechanical: `expr_free_of_region`, `shift`, `subst` all recurse into the sub-expression. ## Changes (formal/TypingL1.v) - New typing rule: ```coq T_Observe_L1 : has_type_l1 m R G e (TEcho T) R' G' -> has_type_l1 m R G (EObserve e) (TBase TUnit) R' G' ``` Modality-polymorphic: fires in both Linear and Affine modes. What differs across modes is the **obligation shape**, not the rule: - **Linear** discipline makes the echo a must-observe (an unobserved `TEcho` in scope is a typing failure). - **Affine** permits implicit lowering (no `T_Observe` required). The mandatoriness is to be enforced via `is_linear_ty TEcho` or the implicit-drop discipline in a follow-up — the present rule is the necessary precondition. ## Cascade fixes (formal/Semantics_L1.v) - `shift_typing_gen_l1_m`: explicit `T_Observe_L1` bullet (commutes with the witness sub-expression via the IH). - `subst_typing_gen_l1_m`: explicit `T_Observe_L1` bullet (same shape). - `region_shrink_preserves_typing_l1_gen_m`: explicit `T_Observe_L1` bullet added before \`Admitted\` (closes via IH; would otherwise be silently absorbed by the outer Admitted). - All other inductions (\`typing_preserves_bindings_l1\`, \`unrestricted_flag_unchanged_l1\`, \`count_occ_le_l1_m\`, \`region_liveness_at_split_l1_gen\`) absorb \`T_Observe_L1\` via their existing catch-all patterns (T_Observe_L1 propagates the IH unchanged on G' and R' — no new structural obligation). ## What is NOT in this slice (deliberately deferred) - **\`S_Region_Exit\` / \`S_Drop\` echo emission in step rules.** The step relation lives in \`Semantics.v\` which is owner-touchy (CLAUDE.md Owner directive 2026-05-27 anti-pattern detector). Will escalate before slice 3. - \`G\` (echo context) threading through compound rules → slice 3 - \`preservation_l3\` → slice 4 - \`is_linear_ty TEcho_ = true\` (mandatoriness enforcement) → follow-up ## Build oracle - \`coqc 8.18.0\` closes the full formal/ tree. - Net debt unchanged on this branch (3 Admitted in \`Semantics_L1.v\`, all pre-existing from prior slices). ## Refs - \`PROOF-NEEDS.md §2\` (L3 wiring) - \`PRESERVATION-DESIGN.md §6.3\` (echo enters the typing rules) - \`formal/Echo.v\` (12 Qed L3 calculus) ## Test plan - [x] \`coqc 8.18.0\` closes full formal/ tree - [x] No new Admitted / Axiom (3 Admitted unchanged from base) - [ ] CI rust-ci → Coq proofs job passes - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
…a) (#192) ## Summary Slice 3a of the L3 wiring sequence. Slices [1 (#190)](../pull/190) and [2 (#191)](../pull/191) added the AST surface and the observation consumer; this slice closes the typing for the runtime echo VALUE form so that the forthcoming step rules (\`S_Region_Exit_Echo\`, \`S_Drop_Echo\` — slice 3b) have a type-preserving target. ## Changes (formal/TypingL1.v) New typing rule: \`\`\`coq T_Echo_L1 : forall m R G v T, is_value v -> R; G |=L1[m] v : T -| R; G -> R; G |=L1[m] EEcho T v : TEcho T -| R; G \`\`\` Modality-polymorphic. Echoes are runtime values that preserve both \`R\` and \`G\` (no resource state change at the typing layer), mirroring \`T_Borrow_Val_L1\`'s value-of-value pattern. ## Cascade fixes (formal/Semantics_L1.v) - \`value_R_G_preserving_l1\` \`VEcho\` case: was \`inversion Ht\` expecting vacuity; now inverts to \`T_Echo_L1\` which gives \`R_out = R\` and \`G_out = G\` directly. - \`shift_typing_gen_l1_m\`: explicit \`T_Echo_L1\` bullet (uses \`shift_preserves_value\` for the value premise + IH for the witness typing). - \`subst_typing_gen_l1_m\`: explicit \`T_Echo_L1\` bullet (uses \`subst_preserves_value\` + IH). - \`region_shrink_preserves_typing_l1_gen_m\`: explicit \`T_Echo_L1\` bullet before \`Admitted\` (closes via IH on the witness; the \`is_value\` premise is preserved by structure). The new constructor's insertion before \`T_Observe_L1\` in the inductive declaration shifted the bullet indices in three proofs; each now has the matching \`T_Echo_L1\` bullet. ## What is NOT in this slice (still deferred) - \`S_Region_Exit_Echo\` / \`S_Drop_Echo\` step rules in \`Semantics.v\` — **slice 3b** (parallel-rule strategy approved 2026-05-27) - \`T_Region_L1_Echo\` / \`T_Drop_L1_Echo\` (parallel typing rules matching the new step-rule output type) — slice 3b - \`G\` (echo context) threading through compound rules — slice 3c - \`preservation_l3\` — slice 4 ## Build oracle - \`coqc 8.18.0\` closes the full formal/ tree. - Net debt unchanged (3 Admitted in \`Semantics_L1.v\`, all pre-existing). ## Refs - \`PROOF-NEEDS.md §2\` (L3 wiring) - \`PRESERVATION-DESIGN.md §6.3\` (echo enters the typing rules) - \`formal/Echo.v\` (12 Qed L3 calculus) ## Test plan - [x] \`coqc 8.18.0\` closes full formal/ tree - [x] No new Admitted / Axiom (3 Admitted unchanged) - [ ] CI rust-ci → Coq proofs job passes - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <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
1 participant
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
Foundation for L3 wiring (PROOF-NEEDS.md §2). Echo.v calculus (12 Qed, 0 admits) is already in place; this PR adds the surface AST needed before [T_Observe] and step-emission rules can land in subsequent slices.
This is slice 1 of 4 in the L3 wiring sequence:
Changes (formal/Syntax.v)
tyconstructorTEcho : ty -> ty. The type of an echo value witnessing an irreversible step that erased a value of typeT. Documented atPRESERVATION-DESIGN.md §6.3.exprconstructorEEcho : ty -> expr -> expr. Runtime-only residue value, mirroring theELocpattern (no surface syntax).is_valueconstructorVEchosoS_Region_Exit/S_Dropcan reduce to a normal form.expr_free_of_region,shift,substall recurse into the witness sub-expression. The witness type annotationTis closed.Cascade fixes
formal/Typing.vfree_regionsgains aTEcho T' => free_regions T'case (linear in the witness).formal/Semantics_L1.vvalue_R_G_preserving_l1gains aVEchocase closed by inversion (no L1 typing rule producesEEchoyet, so the hypothesis is vacuous in this slice).What is NOT in this slice (deliberately deferred per slice plan)
T_Observetyping rule → slice 2S_Region_Exit/S_Dropecho emission in step rules → slice 2G(echo context) threading through compound rules → slice 3preservation_l3→ slice 4is_linear_tyis deliberately not extended —TEchohits the catch-all returningfalsein this slice. The linearity discipline lives in the (forthcoming)T_Observerule's modality dispatch, not inis_linear_ty. Revisit in slice 2 if the rule shape demands it.Build oracle
coqc 8.18.0closes the full formal/ tree (Syntax / Typing / TypingL1 / Semantics / Semantics_L1 / Counterexample / TypingL2).Semantics_L1.v: 23 Qed + 3 Admitted, all pre-existing).Refs
PROOF-NEEDS.md §2(L3 wiring)PRESERVATION-DESIGN.md §6(L3 design — fiber + observation discipline)formal/Echo.v(12 Qed L3 calculus this builds toward integrating)Test plan
coqc 8.18.0closes full formal/ tree🤖 Generated with Claude Code