proof(L3): add parallel step rules S_Region_Exit_Echo + S_Drop_Echo (slice 3c)#194
Merged
hyperpolymath merged 1 commit intoMay 27, 2026
Conversation
…slice 3c) Slice 3c of the L3 wiring sequence. Owner-approved 2026-05-27: PARALLEL step rules in Semantics.v that emit echo residues at irreversible boundaries. Legacy S_Region_Exit + S_Drop are untouched (kept for backward-compat with non-echo typing paths). The new rules pair with the typing rules added in slice 3b: * S_Region_Exit_Echo + T_Region_L1_Echo / T_Region_Active_L1_Echo * S_Drop_Echo + T_Drop_L1_Echo Each emits [EEcho T v] (resp. [EEcho T (ELoc l r)]) where T is quantified universally; preservation_l3 (slice 4) picks T to match the typing derivation. Changes (formal/Semantics.v) * New step rule S_Region_Exit_Echo : same trigger as S_Region_Exit (is_value v, In r R, expr_free_of_region r v), same memory + region effects (mem_free_region, remove_first r), but emits EEcho T v instead of v. Quantified over T. * New step rule S_Drop_Echo : same trigger as S_Drop (EDrop (ELoc l r)), same memory effect (CFree), but emits EEcho T (ELoc l r) instead of EUnit. Quantified over T. Cascade fixes * step_from_eregion: extended from 3-disjunct classification to 4-disjunct (Enter / Exit / Exit_Echo / Step). Exit_Echo's shape matches Exit's except the output is [exists T, e1 = EEcho T e]. * no_leaks_gen: 4th case handled mirroring Exit. EEcho T e is a value (VEcho), so multi_step from there can only be reflexive; memory cleanup discharge via mem_free_region_clears is identical. * step_R_change_shape: explicit bullet for S_Region_Exit_Echo — same R-shape as S_Region_Exit (remove_first r R, In r R). What is NOT in this slice (still deferred) * G (echo context) threading through compound rules — slice 3d * preservation_l3 — slice 4 Build oracle * coqc 8.18.0 closes the full formal/ tree (incl. cascades through step_from_eregion + no_leaks_gen + step_R_change_shape). * Net debt unchanged (3 outer Admitted in Semantics_L1.v, all pre-existing). 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>
2 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
## Summary The original PROOF-NEEDS.md §2 task \"thread G (echo context) alongside R through compound rules\" was speculative — the design question was whether L3 wiring would need a NEW context parameter on every \`has_type_l1\` constructor. Under the **owner-approved parallel-rules design** landed via slices 3a–3c ([#192](../pull/192), [#193](../pull/193), [#194](../pull/194)): - Echoes are runtime VALUES of type \`TEcho T\` (slice 1 + 3a). - They flow through the EXISTING \`ctx\` G context like any other value — no new context parameter needed. - \`T_Observe_L1\` consumes them like any ordinary expression (slice 2). - The two paths (legacy + echo-aware) coexist via parallel typing/step rules, not via context augmentation (slices 3b + 3c). So the G-threading task is **OBSOLETE**. PROOF-NEEDS.md §2 updated to mark it struck-through with explanation. The L3 wiring sequence proceeds directly from 3c to slice 4 (\`preservation_l3\` capstone). ## No code changes Documentation-only update to PROOF-NEEDS.md §2. ## Refs - PROOF-NEEDS.md §2 (L3 wiring) - PRs #192, #193, #194 for the prerequisite slices that obviated this task - PRESERVATION-DESIGN.md §6.3 (L3 design) ## Test plan - [x] No code changes (docs-only) - [ ] 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 3c of the L3 wiring sequence. Owner-approved 2026-05-27: PARALLEL step rules in Semantics.v that emit echo residues at irreversible boundaries. Legacy `S_Region_Exit` + `S_Drop` are untouched (kept for backward-compat with non-echo typing paths).
The new rules pair with the typing rules added in slice 3b (#193):
Each emits `EEcho T v` (resp. `EEcho T (ELoc l r)`) where T is quantified universally; `preservation_l3` (slice 4) picks T to match the typing derivation.
Changes (formal/Semantics.v)
```coq
S_Region_Exit_Echo : forall mu R r v T,
is_value v ->
In r R ->
expr_free_of_region r v ->
(mu, R, ERegion r v) -->>
(mem_free_region mu r, remove_first r R, EEcho T v)
S_Drop_Echo : forall mu R l r T,
(mu, R, EDrop (ELoc l r)) -->>
(mem_write mu l CFree, R, EEcho T (ELoc l r))
```
Cascade fixes
What is NOT in this slice (still deferred)
Build oracle
Refs
Test plan
🤖 Generated with Claude Code