From cf61eb526b749e00a3f8e5b8821d49b9584e7ebc Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 18:13:46 +0000 Subject: [PATCH] chore(proofs): gate L10 echo-types proofs in the canonical suite + e2e example MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Harden and gate what the L10 work landed, fully in-site (local verification; CI billing remains blocked). Gate the two Layer-10 proofs as first-class canonical-proof-suite entries so they get the same nightly enforcement as the M/S/E classics: - New `language` domain in audits/canonical-proof-suite/MANIFEST.a2ml: * L1 — proofs/idris2/EchoResidue.idr, headline `reverseAfterIrreversibleIllTyped` * L2 — proofs/idris2/EchoResidueLinear.idr, headline `reverseLinear` 37 entries total; manifest paren-balanced; the runner's awk parses both with the correct prover/path/symbol. - The runner's `scan_banned` is a whole-file substring match (`grep -qF`), so the two files' own "zero believe_me / assert_total / sorry" disclaimer comments would have false-flagged them as `stub`. Reworded those four comment lines to "no escape hatches" phrasing — meaning preserved, banned tokens gone. Verified locally exactly as the runner invokes (cd into the file's dir, check the basename): both `idris2 --check` exit 0, zero banned constructs, and the expected-symbol has a signature + clause. REPORT.a2ml is intentionally NOT regenerated here — this host has no Rocq 9, so a local run would falsely downgrade the rocq entries; the nightly suite regenerates it with the full toolchain. Also add examples/named_reversibility.007 exercising `reversible as ` / `reverse ` end-to-end: `oo7 parse`, `oo7 check`, and `oo7 run` all pass. CHANGELOG + 6a2 STATE updated; A2ML 6a2 validation clean. https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- .machine_readable/6a2/STATE.a2ml | 4 +-- .machine_readable/session-log.txt | 2 ++ CHANGELOG.md | 1 + audits/canonical-proof-suite/MANIFEST.a2ml | 40 ++++++++++++++++++++-- examples/named_reversibility.007 | 33 ++++++++++++++++++ proofs/idris2/EchoResidue.idr | 4 +-- proofs/idris2/EchoResidueLinear.idr | 4 +-- 7 files changed, 80 insertions(+), 8 deletions(-) create mode 100644 examples/named_reversibility.007 diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 07c89b6..03018c4 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -7,8 +7,8 @@ @state(version="2.0"): phase: "implementation" next_action: "Layer-10 rung 3b: cross-handler residues through agent state — residue cell in agent state + evaluator runtime Holding/Spent (ResidueCell, takeForReverse:Maybe) + EchoResidueLinear bridge lemma; then continue parser gap fill (types, imports, locales, choreographies)" -last_action: "Phase-3 rung-3a landed: NAMED residues within a body — new syntax `reversible as {…}` / `reverse ` (anonymous forms unchanged). Additive AST ReversibleAs/ReverseNamed; grammar.pest+grammar.ebnf; typechecker named_residues map (Holding/Spent, static mirror of ResidueCell) with per-function/handler isolation; eval/codegen/formatter/dual_ast/metainterpreter/CFG/oracle threaded. Affine/linear discipline: double-reverse rejected, un-reversed ok, no cross-body leak. 2 parser + 5 typechecker tests (890 oo7-core passing; fmt clean, clippy -D warnings 0). Spec §11b.5 + CHANGELOG + integration doc in lockstep. Prior: phase-2 Linear> (PR #41 merged), phase-1 (PR #34), CI gates (PR #38), 6a2 (PR #39), estate reconcile (PR #40)" -updated: 2026-06-15T17:00:00Z +last_action: "Hardened + gated what landed: (1) gated the L10 echo-types proofs in the canonical-proof-suite MANIFEST — new 'language' domain L1 (EchoResidue.idr / reverseAfterIrreversibleIllTyped) + L2 (EchoResidueLinear.idr / reverseLinear), 37 entries total; reworded their 'zero believe_me/assert_total/sorry' disclaimer comments so the substring banned-scan doesn't false-positive; verified runner-style (banned-clean, idris2 --check exit 0, symbol sig+clause present). (2) Added examples/named_reversibility.007 exercising reversible-as/reverse-name end-to-end (oo7 parse + check + run all PASS). Decided NOT to regenerate REPORT.a2ml locally (no Rocq 9 here → would falsely downgrade rocq entries; nightly CI regenerates). bag-of-actions repo evaluated as a CI-billing workaround and ruled out (it's an Elixir/Zig continuation runtime, not a GitHub Actions runner). Prior: phase-3 rung-3a (PR #42 merged), phase-2 (PR #41), phase-1 (#34), CI gates (#38), 6a2 (#39), estate (#40)" +updated: 2026-06-15T18:15:00Z @blockers: - id: proof-debt diff --git a/.machine_readable/session-log.txt b/.machine_readable/session-log.txt index 13bdb43..4049485 100644 --- a/.machine_readable/session-log.txt +++ b/.machine_readable/session-log.txt @@ -31,3 +31,5 @@ [2026-06-14 01:25:37] Session ended (continuation): item-2 estate-standardization reconcile MERGED (PR #40) → main is one reconciled line. Then resumed ORIGINAL WORK = Layer-10 PHASE 2 (residue as a linear undo-capability). (a) Idris2: proofs/idris2/EchoResidueLinear.idr (NEW, %default total, zero believe_me, idris2 --check clean) — reverseLinear consumes (1 e : Echo f y) (Idris2 quantity 1 = "consumed exactly once" proof, mirroring 007's planned Linear>); reverseLinearCorrect (recovered input maps back to y, intrinsic via the dependent pair); ResidueCell Holding/Spent = the residue carried as agent STATE between handlers; takeForReverse (later handler consumes the cell; Spent→Nothing); holdingReverses/spentDoesNotReverse (cross-handler reversal succeeds iff a residue was retained); cellMode bridges a cell back to the phase-1 Reversibility mode. (b) Rust typechecker.rs: residue stack now carries Linear> (push_echo_residue wraps Type::Echo in Type::Linear) — the consumed-once discipline is explicit in the carried type; the single linear use is the take_echo_residue pop in a later reverse. +3 typechecker_tests (l10_phase2_residue_type_is_linear_echo / _double_reverse_of_single_residue_is_error / _retained_residue_is_not_an_error) → 883 oo7-core lib tests passing. CI gates verified LOCALLY: cargo check --offline 0, full oo7-core test suite 922 ok 0 fail, fmt --check 0, clippy (CI-equivalent, no --all-targets) -D warnings exit 0. (c) DESIGN DECISION flagged to user (a plus/interesting): the residue is an AFFINE capability consumed LINEARLY — replaying one log twice is rejected (linear use; structural in the stack), but a reversible block need NOT be paired with a reverse (un-reversed residue is NOT an error; reversibility is a capability, usually unused). The opposite (strict must-reverse / LinearNotConsumed) was deliberately REJECTED as semantically wrong + poor agent ergonomics; the 3 tests lock the affine-drop in so it can't be silently tightened. (d) Docs in lockstep: TYPE-SYSTEM-SPEC §11b.4 + OPERATIONAL-SEMANTICS §11.4 (planned→landed), CHANGELOG phase-2 bullet, docs/echo-residue-integration.adoc (phase-2 section + design-decision subsection + "still open" cross-handler rung), 6a2 STATE.a2ml last/next_action + cleared estate-standardization-unmerged blocker. (e) NOTE — canonical-proof-suite MANIFEST.a2ml NOT touched: phase-1 EchoResidue.idr is not a manifest entry either, so EchoResidueLinear.idr stays alongside it (checked by idris2 --check, not the curated S/E/M suite); the proof-suite workflow ignores unlisted .idr files (no CI risk). STILL OPEN (next rung): cross-handler NAMED residues need residue-binding grammar syntax (let undo = reversible {…}; reverse undo) — Harvard-guarded grammar change, kept as its own rung; formal model (ResidueCell) already in place, only surface syntax missing. Phase-2 work pushed to branch claude/echo-residue-phase2-linear → draft PR. Billing blocker may still gate CI (account-owner action). [2026-06-15 17:39:22] Session continued: Layer-10 PHASE 3 RUNG 3a landed (named residues within a body) on branch claude/echo-residue-phase3-named off main. User chose syntax `reversible as undo {…}` / `reverse undo` (the `as`-binder, agent-ergonomic) and scope "static core first" (within-body, fully static; cross-handler 3b deferred). (a) Grammar: grammar.pest + spec/grammar.ebnf — reversible_block gains optional ("as" ~ ident); new reverse_named = "reverse" ~ ident; Harvard-safe (control rules ref the shared ident token; Harvard guard PASS). (b) AST: ADDITIVE variants ReversibleAs{binding,body} + ReverseNamed{target} — existing Reversible/Irreversible/Reverse untouched, so the 9 exhaustive ControlStmt matches were compiler-enumerated + mirrored (codegen_cranelift/elixir/native, dual_ast, eval, formatter, metainterpreter, semantic_analyser/control_flow, typechecker check_stmt) + oracle check.rs + the two combined typechecker passes (effects, collect_linear_lets). (c) Typechecker: per-body named_residues: HashMap — the static mirror of ResidueCell; bind_named_residue (reversible as → Holding(Linear>)); take_named_residue (reverse → Holding→Spent, else Err); per-function + per-handler mem::take isolation (no cross-body leak). Affine/linear: double reverse rejected (Spent), un-reversed bound name NOT an error, reverse of unknown/spent name = L10_REVERSE_WITHOUT_RESIDUE. (d) Parser: build_reversible_block detects optional ident → ReversibleAs vs Reversible; build_reverse_named. (e) Tests: 2 parser (reversible_as_binds_named_residue, reverse_named_parses) + 5 typechecker (named-reverse-ok, reverse-unknown-errs, double-reverse-errs, unreversed-ok-affine, no-cross-function-leak) → 890 oo7-core lib tests pass; full workspace cargo test 0 failures; cargo fmt --check clean; cargo clippy --offline -D warnings exit 0 (CI-equivalent). (f) Docs in lockstep: TYPE-SYSTEM-SPEC §11b.5 (new), docs/echo-residue-integration.adoc (phase-3 section + rung-3b still-open), CHANGELOG, 6a2 STATE. NO new Idris needed — ResidueCell/reverseLinear already model rung 3a. STILL OPEN rung 3b: cross-handler residues via agent state — irreducibly partly RUNTIME (no static knowledge whether the earlier handler fired; Idris takeForReverse returns Maybe), so it adds a residue cell in agent state + evaluator Holding/Spent + bridge lemma. Pushed to claude/echo-residue-phase3-named → draft PR. Billing may still gate CI (account-owner action); verified locally. + +[2026-06-15 18:13:25] Session continued (in-site, billing still blocked): HARDEN + GATE on branch claude/gate-l10-proofs off main (post-#42-merge). User asked whether the CI billing block could be solved via the hyperpolymath/bag-of-actions repo; investigated (search_repositories + WebFetch of its public README): bag-of-actions is an early-stage Elixir/Zig/WASM distributed-continuation runtime ("mobile continuations / Batons"), NOT a GitHub Actions runner — no Actions integration, no webhook/job scheduling, no arbitrary-task CLI. Cannot run 007's CI; also can't add it to MCP scope (no add_repo this session). Reported; user directed "continue in site." Chose (via AskUserQuestion) "Harden + gate what landed". Delivered: (1) Gated the L10 proofs in audits/canonical-proof-suite/MANIFEST.a2ml — new 'language' domain, L1=EchoResidue.idr (headline reverseAfterIrreversibleIllTyped), L2=EchoResidueLinear.idr (headline reverseLinear); 37 entries total, paren-balanced (490/490), runner awk parses both with correct prover/path/symbol. CRITICAL fix: scan_banned uses grep -qF (substring, whole file) so the two files' own "ZERO believe_me / assert_total / sorry" disclaimer comments would have false-flagged them as stub — reworded all 4 comment lines to "no escape hatches" phrasing (meaning preserved, banned tokens gone). Verified runner-style (the runner cd's into dirname + checks basename, so module EchoResidue matches EchoResidue.idr — my first repo-root test wrongly failed on module-name-vs-path): both exit 0, banned-scan 0 hits, verify_idris2_symbol sig+clause PASS for both headlines. Did NOT regenerate REPORT.a2ml locally (coqc 8.18 can't parse From Stdlib → would falsely downgrade the ~30 rocq entries that need Rocq 9; nightly CI regenerates with full toolchain). (2) New e2e example examples/named_reversibility.007 (agent NamedReversal, on receive, reversible as undo { } + reverse undo in one handler) — built oo7 and ran all three e2e sections: parse PASS, check PASS ("type check passed"), run PASS. CHANGELOG + 6a2 STATE updated; A2ML 6a2 validate clean. Pushing to claude/gate-l10-proofs → draft PR. CI remains billing-blocked (maintainer admin-merges, as with #40/#41/#42); everything verified locally. diff --git a/CHANGELOG.md b/CHANGELOG.md index 675dbe6..2096d7c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,7 @@ All notable changes to this project will be documented in this file. - **Layer 10 — Reversibility (Echo residue): echo-types integrated into the type system.** `reversible`/`irreversible`/`reverse` are no longer checked identically: `Type::Echo` residues are tracked per body (`reversible` retains one, `irreversible` discards it, `reverse` consumes one), and a `reverse` with no residue is `ReverseWithoutResidue` — enforcing OPERATIONAL-SEMANTICS §11.3, previously unenforced. Grounded in echo-types' keystone `A ≃ Σ B (Echo f)` and mechanised in `proofs/idris2/EchoResidue.idr` (`encodeDecode`, `reverseAfterIrreversibleIllTyped`, `collapseHasNoSection`; `%default total`, zero `believe_me`). Surfaced to agents via `agent_api` code `L10_REVERSE_WITHOUT_RESIDUE` (+`mark_reversible`/`retain_echo` remediations). 4 new typechecker tests. Spec: TYPE-SYSTEM-SPEC §"Layer 10", OPERATIONAL-SEMANTICS §11.4; design note `docs/echo-residue-integration.adoc`. - **Layer 10 phase 2 — the residue is a linear undo-capability.** The checker's residue stack now carries `Linear>` (was a bare `Echo`), making the consumed-once discipline explicit in the type. Discipline: *affine capability, linear consumption* — a given reversal log is consumed at most once (a double `reverse` of one residue is rejected) yet a `reversible` block need not be paired with a `reverse` (an un-reversed residue is **not** an error; reversibility is a capability, usually unused). Mechanised in `proofs/idris2/EchoResidueLinear.idr` (`reverseLinear` consumes `(1 e : Echo f y)`; `ResidueCell` Holding/Spent = the residue as agent state; `holdingReverses`/`spentDoesNotReverse`; `%default total`, zero `believe_me`, `idris2 --check` clean). 3 new typechecker tests (883 `oo7-core` lib tests passing). Remaining rung: cross-handler *named* residues (residue-binding grammar syntax, Harvard-guarded — kept separate). Spec/docs updated in lockstep. - **Layer 10 phase 3 (rung 3a) — named residues within a body.** New surface syntax `reversible as { … }` binds the echo residue to a name; `reverse ` replays it (anonymous `reversible {…}`/`reverse {…}` unchanged). The named residue is tracked per body as a `Holding(Linear>)` cell that `reverse` transitions to `Spent` — the static mirror of `ResidueCell` (Holding/Spent) in `EchoResidueLinear.idr`. Same affine/linear discipline: double `reverse ` is rejected (cell already `Spent`); a never-replayed binding is **not** an error; named residues are scoped per body (no cross-body leak). Additive AST variants `ReversibleAs`/`ReverseNamed` (existing variants untouched); grammar (`grammar.pest` + `spec/grammar.ebnf`), parser, typechecker (`named_residues` map + per-function/handler isolation), and the eval/codegen/formatter/dual-ast/metainterpreter/CFG/oracle pipeline all threaded. 2 parser + 5 typechecker tests (890 `oo7-core` lib tests passing; fmt clean, clippy `-D warnings` exit 0). Remaining rung 3b: cross-handler residues through agent state (irreducibly partly runtime — `takeForReverse : Maybe`). Spec: TYPE-SYSTEM-SPEC §11b.5; docs `docs/echo-residue-integration.adoc`. +- **Layer 10 proofs gated in the canonical proof suite.** The L10 echo-types proofs are now first-class suite entries (`audits/canonical-proof-suite/MANIFEST.a2ml`), gated nightly like the M/S/E classics: new `language` domain `L1` (`proofs/idris2/EchoResidue.idr`, headline `reverseAfterIrreversibleIllTyped`) and `L2` (`proofs/idris2/EchoResidueLinear.idr`, headline `reverseLinear`) — 37 entries total. Each gets the runner's banned-construct scan + `idris2 --check` + symbol-defined check; both verified locally (exit 0, zero banned constructs). The two files' "zero believe_me/assert_total/sorry" disclaimer comments were reworded so the substring banned-scan doesn't false-positive on the very tokens they disclaim. New end-to-end example `examples/named_reversibility.007` exercises `reversible as`/`reverse ` through the full pipeline (parse + typecheck + run all pass). - **752 tests** (up from 207 at 0.5.0). CRG-C achieved 2026-04-04 for `oo7-core`. - **31 multi-language backends** via `mk2_bridge::create_backend_registry()`. Real dispatch to `elixir`, `idris2`, `gleam`, `rescript`, `nickel`, `guile`, `psql`, etc. Tier-5 coprocessor backends (CUDA/Vulkan/Metal/OpenCL/FPGA/TPU/DSP) do phase-1 device discovery with documented "kernel launch is future work" status. - **Metainterpreter** (`metainterpreter.rs`, ~3,075 LOC): reify/reflect/step/replay, four modes, 40 inline tests, 18 benches. diff --git a/audits/canonical-proof-suite/MANIFEST.a2ml b/audits/canonical-proof-suite/MANIFEST.a2ml index e57bee9..edea790 100644 --- a/audits/canonical-proof-suite/MANIFEST.a2ml +++ b/audits/canonical-proof-suite/MANIFEST.a2ml @@ -35,7 +35,7 @@ (suite-spec-version "1.1-proposed") (suite-spec-date "2026-04-18") (canonical-doc "audits/canonical-proof-suite/README.adoc") - (last-manifest-update "2026-04-18") + (last-manifest-update "2026-06-15") (status "active")) ;; ======================================================== @@ -446,6 +446,37 @@ (status "not-started") (porting-source "Isabelle HOL Circuits (community); derive from charge + energy conservation")) + ;; ======================================================== + ;; Language metatheory — L1..L2 (007's own Layer-10 proofs) + ;; ======================================================== + ;; + ;; Unlike M/S/E (canonical classics ported into 007's provers), the + ;; L-series gates 007's OWN mechanised metatheory: the Layer-10 + ;; echo-types reversibility proofs that back the type checker. They + ;; live in proofs/idris2/ (load-bearing library modules) rather than + ;; proofs/canonical-proof-suite/, and the runner checks them at that + ;; path. Both are %default total with no escape hatches. + + (entry + (id "L1") + (domain "language") + (theorem "Layer 10 reversibility: `reverse` of an irreversible block is ill-typed (ReverseOk Irrev is uninhabited); an irreversible map's echo residue makes it reversible, A ~= (y : B ** Echo f y)") + (prover "idris2") + (proof-file "proofs/idris2/EchoResidue.idr") + (expected-symbol "reverseAfterIrreversibleIllTyped") + (status "passing") + (porting-source "echo-types EchoTotalCompletion (A ~= Sigma B (Echo f)); 007 OPERATIONAL-SEMANTICS 11.3 + TYPE-SYSTEM-SPEC Layer 10")) + + (entry + (id "L2") + (domain "language") + (theorem "Layer 10 phase 2-3: the echo residue is a linear undo-capability consumed exactly once (reverseLinear over a linear (1 e : Echo f y)); named residues replay at most once") + (prover "idris2") + (proof-file "proofs/idris2/EchoResidueLinear.idr") + (expected-symbol "reverseLinear") + (status "passing") + (porting-source "echo-types EchoLinear (linear strand); 007 TYPE-SYSTEM-SPEC 11b.4 / 11b.5")) + ;; ======================================================== ;; Banned constructs (per CANONICAL-PROOF-SUITE.adoc §pass-condition) ;; ======================================================== @@ -499,4 +530,9 @@ (date "2026-04-18") (author "Jonathan D.A. Jewell") (change "suite-spec-version bumped from 1.0 to 1.1-proposed; 20 new entries added in four priority tiers: M6/S6/E6/M7 (Tier 1 foundational gaps), M8-M11/E7 (Tier 2 classical), S7/E8/M12/S8/E9 (Tier 3 interdisciplinary), M13/M14/S9/S10/E10/E11 (Tier 4 deferred). All new entries at status not-started and with underscored rocq proof-file paths from the outset. Fills zero-coverage holes in logic, probability, chemistry, chem eng, knot theory, relativity, epidemiology, reliability, and power engineering among others.") - (rationale "Author-initiated gap-analysis: v1.0 biased strongly to 20th-century foundational classics and left entire disciplines (logic, probability, chemistry, chem eng, knot theory) with zero coverage. Corresponding standards-repo spec bump pending. Spec-self-mandated 90-day co-signed review window starts at the standards-repo commit for CANONICAL-PROOF-SUITE.adoc; manifest tracks the aspiration, scaffolds may begin immediately in 007. See ~/Desktop/AI-WORK-007.md §3a for the tiered execution plan.")))) + (rationale "Author-initiated gap-analysis: v1.0 biased strongly to 20th-century foundational classics and left entire disciplines (logic, probability, chemistry, chem eng, knot theory) with zero coverage. Corresponding standards-repo spec bump pending. Spec-self-mandated 90-day co-signed review window starts at the standards-repo commit for CANONICAL-PROOF-SUITE.adoc; manifest tracks the aspiration, scaffolds may begin immediately in 007. See ~/Desktop/AI-WORK-007.md §3a for the tiered execution plan.")) + (entry + (date "2026-06-15") + (author "Jonathan D.A. Jewell") + (change "add L-series — L1 (EchoResidue) + L2 (EchoResidueLinear): gate 007's own Layer-10 echo-types reversibility proofs (proofs/idris2/*.idr, idris2, %default total) alongside the M/S/E entries. Reworded the two files' in-file disclaimer comments so the banned-construct substring scan does not false-positive on the very tokens they disclaim.") + (rationale "The Layer-10 proofs are the language's load-bearing metatheory but were checked only ad hoc (idris2 --check) outside the gated suite. Gating gives them the same nightly banned-construct + symbol-defined enforcement as the canonical entries; domain language keeps them honestly distinct from the famous-theorem ports — these prove 007's OWN type system, not classical results.")))) diff --git a/examples/named_reversibility.007 b/examples/named_reversibility.007 new file mode 100644 index 0000000..231d99d --- /dev/null +++ b/examples/named_reversibility.007 @@ -0,0 +1,33 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Example: named reversibility (Layer 10 phase 3, rung 3a). +-- +-- `reversible as { ... }` binds this block's echo residue to a name; +-- a later `reverse ` in the SAME body replays it, consuming it exactly +-- once. This is the named counterpart to the anonymous `reversible {}` / +-- `reverse {}` forms (see reversibility.007), and is fully statically checked: +-- +-- * a second `reverse undo` is a compile-time error (the residue is a linear +-- undo-capability, replayable at most once); +-- * never replaying a bound residue is NOT an error (it is affine — an undo +-- capability may simply go unused); +-- * a `reverse undo` with no matching `reversible as undo` in the same body +-- is the reverse-without-residue error. +-- +-- Mechanised model: proofs/idris2/EchoResidueLinear.idr (ResidueCell +-- Holding/Spent); see spec/TYPE-SYSTEM-SPEC.adoc §11b.5. + +agent NamedReversal { + control { + on receive(amount: Int) { + -- Bind this block's echo residue to `undo`. + reversible as undo { + let snapshot = amount + } + + -- ... later, in the same handler, replay it by name. + reverse undo + } + } +} diff --git a/proofs/idris2/EchoResidue.idr b/proofs/idris2/EchoResidue.idr index 87b7ea9..ca31e70 100644 --- a/proofs/idris2/EchoResidue.idr +++ b/proofs/idris2/EchoResidue.idr @@ -28,7 +28,7 @@ -- enforces (see crates/oo7-core/src/typechecker.rs, Type::Echo and -- ControlStmt::Reverse). -- --- This file carries ZERO `believe_me` / `assert_total` / `idris_crash`. +-- This file uses no Idris2 escape hatches — every proof is genuinely total. module EchoResidue @@ -185,7 +185,7 @@ reverseOkIffLeavesEcho : (m : Reversibility) -> ReverseOk m -> leavesEcho m = Tr reverseOkIffLeavesEcho Rev RevOK = Refl -- ============================================================ --- Summary (zero believe_me, zero sorry, %default total) +-- Summary (no escape hatches, no holes, %default total) -- ============================================================ -- -- echoIntro / echoHits : the residue type and its intro diff --git a/proofs/idris2/EchoResidueLinear.idr b/proofs/idris2/EchoResidueLinear.idr index 1e617ac..0d6d34d 100644 --- a/proofs/idris2/EchoResidueLinear.idr +++ b/proofs/idris2/EchoResidueLinear.idr @@ -23,7 +23,7 @@ -- LATER handler — which is precisely the cross-handler reversal Phase 1 -- could not express. -- --- This file carries ZERO believe_me / assert_total / idris_crash. +-- This file uses no Idris2 escape hatches — every proof is genuinely total. module EchoResidueLinear @@ -109,7 +109,7 @@ cellMode (Holding _) = Rev cellMode Spent = Irrev -- ============================================================ --- Summary (zero believe_me, %default total) +-- Summary (no escape hatches, %default total) -- ============================================================ -- -- reverseLinear : consume the residue exactly once (linearity = proof)