proof(L3): add T_Observe_L1 typing rule + EObserve expr (L3 wiring slice 2)#191
Merged
hyperpolymath merged 1 commit intoMay 27, 2026
Merged
Conversation
…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
merged commit d222b70
into
proof/semantics-l1-affine-bullet-fix
4 of 13 checks passed
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
Slice 2 of 4 in the L3 wiring sequence. Slice 1 (#190) added the
TEcho/EEchoAST surface; this slice adds the explicit observation rule that consumes an echo.Changes (formal/Syntax.v)
exprconstructorEObserve : expr -> expr. Surface-writable (unlikeEEchowhich is runtime-only).expr_free_of_region,shift,substall recurse into the sub-expression.Changes (formal/TypingL1.v)
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'What differs across modes is the obligation shape, not the rule:
TEchoin scope is a typing failure).T_Observerequired).The mandatoriness is to be enforced via
is_linear_ty TEchoor 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: explicitT_Observe_L1bullet (commutes with the witness sub-expression via the IH).subst_typing_gen_l1_m: explicitT_Observe_L1bullet (same shape).region_shrink_preserves_typing_l1_gen_m: explicitT_Observe_L1bullet added before `Admitted` (closes via IH; would otherwise be silently absorbed by the outer Admitted).What is NOT in this slice (deliberately deferred)
Build oracle
Refs
Test plan
🤖 Generated with Claude Code