Checkpoint: ADR-0007 addition-only mandate + Echo reversibility tiering, STATE refresh

.hypatia-ignore

@@ -11,3 +11,10 @@ vscode-extension/src/Extension.res:cicd_rules/banned_language_file
 web/Main.res:cicd_rules/banned_language_file
 web/MainTest.res:cicd_rules/banned_language_file
 web/Server.res:cicd_rules/banned_language_file
+
+# Frozen archive (playground/experiments/_attic/, see its FROZEN.md): retired
+# demo experiments kept for design lineage, not shipped code. The ArangoDB demo
+# uses a placeholder DB password ("rootpassword"), not a real credential — this
+# is a false-positive that re-fires on every scan. (Disposition keep-frozen vs
+# delete is a checkpoint decision; until then, exempt the false-positive.)
+playground/experiments/_attic/database-demos/arangodb-demo/queries.js:code_safety/js_hardcoded_secret

.machine_readable/6a2/STATE.a2ml

@@ -5,9 +5,9 @@
 [metadata]
 project = "julia-the-viper"
 version = "0.0.1"
-last-updated = "2026-06-02"
+last-updated = "2026-06-13"
 status = "active"
-session = "2026-06-02 — Proof repair complete; Echo Phase 2 design; build-truth CI fixes; documentation refresh"
+session = "2026-06-13 — PR #26 (Lean repair + Echo as structural type-system gate + root-cause Rust-CI fix) and PR #27 (de-vacuation of 8 True-typed believeme theorems) merged; ADR-0007 records the addition-only mandate + Echo reversibility tiering; governance-hardening + number-system-semantics + v2 (c) bridge queued"
 
 [project-context]
 name = "Julia The Viper"
@@ -37,23 +37,30 @@ milestones = [
   "Lean 4 proof repair — COMPLETE (2026-06-02): all 5 libraries compile; zero sorry; JtvCore/Theorems/Operational/Types/Security",
   "Idris2 ABI repair — COMPLETE (2026-06-02): Types.idr compiles; %default total; CanWiden extended; dataIsNeverControl proved",
   "Build-truth CI — COMPLETE (2026-06-02): patacl-core path dep removed; proof-regression.yml fixed; coverage/governance/language-policy CI clean",
-  "Documentation refresh — COMPLETE (2026-06-02): README.adoc, EXPLAINME.adoc, STATUS.adoc, 6a2, contractiles updated to highest standards"
+  "Documentation refresh — COMPLETE (2026-06-02): README.adoc, EXPLAINME.adoc, STATUS.adoc, 6a2, contractiles updated to highest standards",
+  "Lean suite repair + Echo structural type-system gate — COMPLETE (PR #26): JtvEcho.neg_injective fixed; orphan JtvExtended wired into lakefile (8 libs build); Echo admissibility gates BOTH reverse{} and reversible{}->tok, checked structurally and before type inference; fixed a pre-existing failing reverse-block echo test",
+  "Root-cause Rust CI fix — COMPLETE (PR #26): rust-ci.yml + coverage.yml startup-failed since ~2026-05-27 (hashFiles() invalid in a job-level if:); un-gated → Rust build/fmt/clippy/test (3-OS matrix) + coverage now actually run; cleared a hidden clippy lint; pinned coverage upload-artifact; added timeout-minutes across workflows; pinned *.jtv/*.pata to eol=lf",
+  "Proof honesty: believeme de-vacuation — COMPLETE (PR #27): 8 True-typed vacuous theorems (incl. string_not_executable, confluence) replaced with real compiled statements; NO-VACUITY invariant + Int-only semantic-scope recorded in PROOF-CAPABILITY-MATRIX.adoc; 0 sorry/admit/axiom AND 0 True-typed theorems",
+  "ADR-0007 addition-only mandate + Echo reversibility tiering — COMPLETE (2026-06-13): addition-only absolute; reverse-addition (not 2s-complement/not primitive); Harvard-in-von-Neumann AOLD insertability; shortest-path-to-equality + Echo lineage + cross-system routing; group/cancellative/idempotent → Safe/Neutral/Breaking tiering"
 ]
 
 [blockers-and-issues]
 issues = [
   { id = "gap-001", description = "Verification chain incomplete: proofs validate models but not wired to Rust interpreter", severity = "medium", status = "known" },
   { id = "gap-002", description = "typing_coercion in JtvTypes.lean weaker than docstring — proves existence not coercion to target type", severity = "low", status = "known", follow-up = "ADR needed" },
   { id = "gap-003", description = "Coprocessor implementation gated on PataCL Phase 1", severity = "medium", status = "external-dependency" },
-  { id = "gap-004", description = "Reversibility round-trip not guaranteed end-to-end at integration level", severity = "medium", status = "known" }
+  { id = "gap-004", description = "Reversibility round-trip not guaranteed end-to-end at integration level", severity = "medium", status = "known" },
+  { id = "gap-005", description = "Semantic model is Int-only: the 7 number systems are typed but stated-unproven at the value level; type_preservation mechanised only for τ=int (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc)", severity = "medium", status = "known", follow-up = "number-system-semantics work" }
 ]
 
 [critical-next-actions]
 actions = [
-  "PataCL Phase 1 → unblocks JtV coproc implementation Phase 2",
+  "Governance hardening (branch claude/jtv-governance-hardening): pin governance-reusable@main → SHA (consistent with sibling standards reusables); add secret-scanner.yml wrapper (standards reusable exists at 524523c); add 'actions' language to codeql.yml; harden proof-regression download-then-run; NOTE the reusable-call-job missing-timeout Hypatia findings are false-positives (timeout-minutes is invalid on reusable-call jobs)",
+  "Number-system semantics (ADR-0007 D6): value model for the 7 systems + per-system additive-algebra → Echo-tier classification; keep addition-only (×/÷ generated, not primitive); lift type_preservation beyond τ=int",
+  "v2 (c) token/residue neutral-reversal bridge (ADR-0007 D5 Neutral tier): JtvEcho admissibleWithResidue + Neutral-recoverable-given-token theorem; typechecker reversible{}->tok admits Neutral; runtime residue in reversible.rs (or documented conservative scope)",
+  "Echo as first-class function effect ('(b)') — after (c) stabilises",
   "Verification bridge: correlation tests between Lean semantics and Rust interpreter",
-  "Echo Phase 3: residue availability and audit trail implementation",
-  "Reversibility round-trip guarantee: integration-level property test"
+  "PataCL Phase 1 → unblocks JtV coproc implementation Phase 2"
 ]
 
 [maintenance-status]
@@ -70,11 +77,16 @@ sessions = [
   { date = "2026-04-27", subject = "C2 reversibility: reversible { } -> tok / reverse tok / abandon tok; ReversalToken(u64) opaque-ID token store; token linearity; typechecker + cli sexpr arms; 5 C2 tests green; commit a6b9e83" },
   { date = "2026-04-27", subject = "WASM extern-coproc bridge: list_coproc_decls on Interpreter + JtvWasm; register_coproc_impl wraps js_sys::Function via unsafe Send+Sync; Value<->JsValue helpers; 4 tests; commit 75be523 — all roadmap items complete" },
   { date = "2026-06-02", subject = "Echo Phase 2 design: retained-loss lineage; EchoSafe/Neutral/Breaking; infer+@echo; 3-way numeric; JtvEcho.lean; ALIGNMENT-AFFINESCRIPT.adoc; spec §7/§12" },
-  { date = "2026-06-02", subject = "Build-truth: patacl-core path dep removed from workspace; [features] patacl = [] pure code feature; proof-regression.yml startup failure fixed; Lean 4 all 5 libs compile; Idris2 Types.idr compiles; CI governance/language-policy/deno-lint fixes; documentation refresh" }
+  { date = "2026-06-02", subject = "Build-truth: patacl-core path dep removed from workspace; [features] patacl = [] pure code feature; proof-regression.yml startup failure fixed; Lean 4 all 5 libs compile; Idris2 Types.idr compiles; CI governance/language-policy/deno-lint fixes; documentation refresh" },
+  { date = "2026-06-13", subject = "PR #26 merged: Lean suite repaired (JtvEcho.neg_injective; orphan JtvExtended wired in → 8 libs); Echo a structural type-system gate over BOTH reverse{} and reversible{}->tok (checked first, before type inference); fixed pre-existing failing reverse-block echo test; root-cause Rust-CI revival (rust-ci/coverage hashFiles-in-job-if startup failure since ~05-27); clippy lint cleared; workflow pins+timeouts; *.jtv/*.pata eol=lf" },
+  { date = "2026-06-13", subject = "PR #27 merged: de-vacuated 8 True-typed believeme theorems (string_not_executable, confluence, no_vulnerable_constructs, no_reverse_joinpoints, dataExpr_no_control, data_evaluation_secure, control_data_noninterference, rev_composition) into real compiled statements; NO-VACUITY + Int-only-scope recorded in capability matrix" },
+  { date = "2026-06-13", subject = "ADR-0007: addition-only mandate (absolute; ×/÷ generated, not primitive); subtraction = reverse addition (not 2s-complement/not primitive); Harvard-in-von-Neumann AOLD insertability; shortest-path-to-equality + Echo lineage + cross-system routing; additive-algebra → reversibility-tier (group→Safe / cancellative→Neutral / idempotent→Breaking; Echo's own join is idempotent)" }
 ]
 
 [design-artefact-locations]
 coproc-adrs = "docs/design-decisions/0001-0006-*.adoc"
+addition-only-mandate-adr = "docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc"
+proof-capability-matrix = "verification/PROOF-CAPABILITY-MATRIX.adoc"
 coproc-trajectories = ".machine_readable/COPROC-TRAJECTORIES.a2ml"
 v2-reversibility-design = "docs/language/DESIGN-JTV-V2-REVERSIBILITY.md"
 echo-alignment = "ALIGNMENT-AFFINESCRIPT.adoc"

docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc

@@ -0,0 +1,173 @@
+// SPDX-License-Identifier: MPL-2.0
+// (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
+// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= ADR-0007: Addition-Only Mandate, Reverse Addition, and the Echo Reversibility Tiering
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:revdate: 2026-06-13
+:revnumber: 0.1
+:toc: left
+:sectnums:
+
+[.lead]
+This ADR records the *core mandate* re-affirmed in the 2026-06 design
+sessions and the new unifying result that ties JtV's number systems,
+its reverse-addition semantics, and the Echo type lattice together: the
+*algebraic structure of a number system determines its reversibility
+tier*, and Echo is the bookkeeping of that tier. It is the durable
+basis for the planned number-system-semantics work and the v2
+token/residue ("(c)") reversal bridge. Capturing it here makes the
+basis survive any loss of conversational context.
+
+== Status
+
+*Decided / re-affirmed (2026-06-13).* Foundational; constrains all v2
+and number-system work. Does not supersede prior ADRs; it makes
+explicit an invariant that was always implicit and adds the
+reversibility-tier model. Source of truth for the items it states;
+where any other document disagrees, this ADR is right and the other is
+a bug (mirrors the capability-matrix discipline).
+
+== Context
+
+Across the 2026-06 sessions the proof suite was repaired and made
+honest (PR #26: Lean repair + Echo as a structural type-system gate +
+root-cause CI fix; PR #27: de-vacuation of eight `True`-typed
+"believeme" theorems — see `verification/PROOF-CAPABILITY-MATRIX.adoc`).
+That work surfaced design questions about how far v2 reversibility and
+multi-number-system support may go *without* eroding JtV's identity.
+The answers below are mandates, not preferences.
+
+== Decision
+
+=== D1 — Addition-only is absolute
+
+All of the language is *addition-only*. There is **no multiplication
+primitive** and **no primitive subtraction**. This is a core mandate,
+not a default. It holds for every number system JtV traverses.
+
+* Multiplication, division, and any higher operation are *generated*
+  (e.g. via Control loops) — never Data primitives. "Addition + Control
+  loops = Turing-complete; addition without loops = total" remains the
+  spine.
+* `×`/`÷`, where admissible, are *inverse-structured* operations under
+  the relevant algebra ("inverse multiplication or whatever"), not new
+  Data-plane tokens.
+
+=== D2 — Subtraction is REVERSE addition (not twos-complement, not a primitive)
+
+Subtraction is the *reversal of an addition* — the `reverse` of `+`
+— recovered via the reverse/echo mechanism, **not** twos-complement
+bit manipulation and **not** a standalone operator. The mechanised
+model already reflects this: `RevOp.execBackward (addAssign x e)` is
+`σ x - eval e`, proved an inverse by `JtvTheorems.rev_forward_backward`
+under exactly the Safe condition `x ∉ e.freeVars`.
+
+[NOTE]
+====
+*Open tension (flagged, to resolve in the number-system work):* the
+`DataExpr`/`Negate` (Lean `DataExpr.neg`) constructor still exists as a
+*primitive* in the AST. Under D2, negation/subtraction should be
+*generated by reversal*, not a Data primitive. Revisit whether `neg`
+stays, becomes reverse-only sugar, or is removed.
+====
+
+=== D3 — Turing-completeness = a Harvard block embedded in a von-Neumann host; both are graftable (AOLD)
+
+JtV achieves Turing-completeness by embedding a *Harvard block*
+(the Data/Control-separated, total, addition-only island) inside a
+von-Neumann host language. Crucially, *both* the addition primitive
+*and* the Harvard block are **insertable into other language grammars**
+as aspects — Aspect-Oriented Language Development (AOLD) — exactly as in
+v1. This is the "universal extender": injection-safety and totality are
+retrofitted into legacy grammars by grafting these aspects, not by
+rewriting the host. (See `JtvSecurity.AOLDGuarantee`,
+`no_control_to_data_flow`, and `no_reverse_joinpoints`.)
+
+=== D4 — Computation is shortest-path-to-equality, with Echo as lineage
+
+A result is reached by the *shortest addition-path to equality*. From
+`8` to `10`, the paths `8 + 2` and `8 - 6 + 4` both reach `10`; JtV
+takes `8 + 2` (shorter), and *Echo types record the lineage* of the
+path actually taken. The shortest path may *route through other number
+systems* (`x → … → z`, switching representation mid-path) when that is
+shorter; Echo then carries the *cross-system* provenance.
+
+Consequence: number systems are not merely supported types — they are
+*path-optimisation spaces*, and Echo is the provenance of which spaces
+a computation traversed and what (if anything) was lost crossing them.
+
+=== D5 — Reversal strategy is a fallback ladder (algorithmic, else step down)
+
+Reverse "wherever possible" is *algorithmic*; where an algorithmic
+inverse is infeasible, *step down through lesser tiers of reversibility*
+rather than abandon it outright. This is precisely the Echo lattice read
+as a strategy:
+
+* *Safe* — algorithmic, bijective reverse; no residue needed.
+* *Neutral* — reverse only *from retained lineage* (a residue / linear
+  `ReversalToken`, Bennett-style). This is the v2 "(c)" bridge.
+* *Breaking* — no reverse even with lineage; forward-only.
+
+=== D6 — The Echo tier of a number system is fixed by its additive algebra
+
+The unifying result. The algebraic structure of a number system's
+"addition" determines, *a priori*, the best reversibility tier
+attainable in it:
+
+[cols="1,2,2,1",options="header"]
+|===
+| Additive structure | Example | Reverse addition? | Echo tier
+
+| Group | `ℤ` | always, algorithmic | *Safe*
+| Cancellative monoid | `ℕ` (`a+b=a+c ⇒ b=c`) | only *given the lineage/residue* | *Neutral*
+| Idempotent monoid | tropical / max-plus, lattices, `min`/`max`/`∪` | never, even with lineage | *Breaking*
+|===
+
+Therefore "switching number system for a shorter path" (D4) also
+*switches reversibility tier*, and Echo records both the hop and the
+residue that a later reverse would require.
+
+[NOTE]
+====
+*Self-reference / open challenge.* JtV's own Echo lattice
+`{Safe ⊑ Neutral ⊑ Breaking}` under join is itself an *idempotent*
+monoid (`join_idem` is a proved theorem) — so it has **no inverse**,
+which is *why* `Breaking` is one-way and you cannot "un-join" back to
+`Safe`. The standing question "is there a number system with no
+subtraction equivalent at all (not even reverse addition)?" is answered
+*yes* — any non-trivial idempotent additive structure (tropical
+semirings, lattices). In such systems the D5 ladder is *forced*: Safe
+is impossible, so one must keep a residue (Neutral) or accept Breaking.
+====
+
+== Consequences
+
+. *Number-system semantics work (next-but-one priority).* The Lean model
+  is currently `Int`-only (`evalDataExpr : DataExpr → State → Int`);
+  the seven systems are *typed* but `stated-unproven` at the value
+  level, and `type_preservation` is mechanised only for `τ = int`. The
+  semantics layer must (a) give each system a value model, (b) classify
+  each by its additive algebra → Echo tier per D6, and (c) keep
+  addition-only (D1) — `×`/`÷` generated, not primitive.
+. *v2 "(c)" bridge.* Implements the Neutral tier of D5: `reverse { }`
+  stays Safe-only; `reversible { } -> tok` admits Neutral via the
+  retained log/token (Bennett). Lean: extend `JtvEcho` with
+  `admissibleWithResidue` + a "Neutral recoverable given its token"
+  theorem mirroring `rev_forward_backward`. Runtime: `reversible.rs`
+  must record/invert residue for Neutral, or the gate stays
+  conservative with the scope documented.
+. *Revisit `DataExpr.neg`* per the D2 note.
+. *Identity preserved.* D1–D3 confirm v2/Echo do **not** erode JtV:
+  injection-impossibility rests on `no_control_to_data_flow` + disjoint
+  Data/Control types + data-inertness; the Data plane stays total,
+  pure, addition-only; Echo is a third orthogonal axis living in
+  Control's reverse blocks.
+
+== References
+
+* `verification/PROOF-CAPABILITY-MATRIX.adoc` — authoritative proof status.
+* `jtv_proofs/JtvEcho.lean` — Echo lattice + admissibility (impl-semantics source of truth).
+* `jtv_proofs/JtvTheorems.lean` — `rev_forward_backward`, totality, flow separation.
+* `jtv_proofs/JtvSecurity.lean` — `no_control_to_data_flow`, `no_reverse_joinpoints`, `AOLDGuarantee`.
+* PRs #26 (proof repair + structural Echo gate + CI root-fix), #27 (believeme de-vacuation).