|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// (MPL-2.0 is automatic legal fallback until PMPL is formally recognised) |
| 3 | +// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | + |
| 5 | += ADR-0007: Addition-Only Mandate, Reverse Addition, and the Echo Reversibility Tiering |
| 6 | +Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 7 | +:revdate: 2026-06-13 |
| 8 | +:revnumber: 0.1 |
| 9 | +:toc: left |
| 10 | +:sectnums: |
| 11 | + |
| 12 | +[.lead] |
| 13 | +This ADR records the *core mandate* re-affirmed in the 2026-06 design |
| 14 | +sessions and the new unifying result that ties JtV's number systems, |
| 15 | +its reverse-addition semantics, and the Echo type lattice together: the |
| 16 | +*algebraic structure of a number system determines its reversibility |
| 17 | +tier*, and Echo is the bookkeeping of that tier. It is the durable |
| 18 | +basis for the planned number-system-semantics work and the v2 |
| 19 | +token/residue ("(c)") reversal bridge. Capturing it here makes the |
| 20 | +basis survive any loss of conversational context. |
| 21 | + |
| 22 | +== Status |
| 23 | + |
| 24 | +*Decided / re-affirmed (2026-06-13).* Foundational; constrains all v2 |
| 25 | +and number-system work. Does not supersede prior ADRs; it makes |
| 26 | +explicit an invariant that was always implicit and adds the |
| 27 | +reversibility-tier model. Source of truth for the items it states; |
| 28 | +where any other document disagrees, this ADR is right and the other is |
| 29 | +a bug (mirrors the capability-matrix discipline). |
| 30 | + |
| 31 | +== Context |
| 32 | + |
| 33 | +Across the 2026-06 sessions the proof suite was repaired and made |
| 34 | +honest (PR #26: Lean repair + Echo as a structural type-system gate + |
| 35 | +root-cause CI fix; PR #27: de-vacuation of eight `True`-typed |
| 36 | +"believeme" theorems — see `verification/PROOF-CAPABILITY-MATRIX.adoc`). |
| 37 | +That work surfaced design questions about how far v2 reversibility and |
| 38 | +multi-number-system support may go *without* eroding JtV's identity. |
| 39 | +The answers below are mandates, not preferences. |
| 40 | + |
| 41 | +== Decision |
| 42 | + |
| 43 | +=== D1 — Addition-only is absolute |
| 44 | + |
| 45 | +All of the language is *addition-only*. There is **no multiplication |
| 46 | +primitive** and **no primitive subtraction**. This is a core mandate, |
| 47 | +not a default. It holds for every number system JtV traverses. |
| 48 | + |
| 49 | +* Multiplication, division, and any higher operation are *generated* |
| 50 | + (e.g. via Control loops) — never Data primitives. "Addition + Control |
| 51 | + loops = Turing-complete; addition without loops = total" remains the |
| 52 | + spine. |
| 53 | +* `×`/`÷`, where admissible, are *inverse-structured* operations under |
| 54 | + the relevant algebra ("inverse multiplication or whatever"), not new |
| 55 | + Data-plane tokens. |
| 56 | + |
| 57 | +=== D2 — Subtraction is REVERSE addition (not twos-complement, not a primitive) |
| 58 | + |
| 59 | +Subtraction is the *reversal of an addition* — the `reverse` of `+` |
| 60 | +— recovered via the reverse/echo mechanism, **not** twos-complement |
| 61 | +bit manipulation and **not** a standalone operator. The mechanised |
| 62 | +model already reflects this: `RevOp.execBackward (addAssign x e)` is |
| 63 | +`σ x - eval e`, proved an inverse by `JtvTheorems.rev_forward_backward` |
| 64 | +under exactly the Safe condition `x ∉ e.freeVars`. |
| 65 | + |
| 66 | +[NOTE] |
| 67 | +==== |
| 68 | +*Open tension (flagged, to resolve in the number-system work):* the |
| 69 | +`DataExpr`/`Negate` (Lean `DataExpr.neg`) constructor still exists as a |
| 70 | +*primitive* in the AST. Under D2, negation/subtraction should be |
| 71 | +*generated by reversal*, not a Data primitive. Revisit whether `neg` |
| 72 | +stays, becomes reverse-only sugar, or is removed. |
| 73 | +==== |
| 74 | + |
| 75 | +=== D3 — Turing-completeness = a Harvard block embedded in a von-Neumann host; both are graftable (AOLD) |
| 76 | + |
| 77 | +JtV achieves Turing-completeness by embedding a *Harvard block* |
| 78 | +(the Data/Control-separated, total, addition-only island) inside a |
| 79 | +von-Neumann host language. Crucially, *both* the addition primitive |
| 80 | +*and* the Harvard block are **insertable into other language grammars** |
| 81 | +as aspects — Aspect-Oriented Language Development (AOLD) — exactly as in |
| 82 | +v1. This is the "universal extender": injection-safety and totality are |
| 83 | +retrofitted into legacy grammars by grafting these aspects, not by |
| 84 | +rewriting the host. (See `JtvSecurity.AOLDGuarantee`, |
| 85 | +`no_control_to_data_flow`, and `no_reverse_joinpoints`.) |
| 86 | + |
| 87 | +=== D4 — Computation is shortest-path-to-equality, with Echo as lineage |
| 88 | + |
| 89 | +A result is reached by the *shortest addition-path to equality*. From |
| 90 | +`8` to `10`, the paths `8 + 2` and `8 - 6 + 4` both reach `10`; JtV |
| 91 | +takes `8 + 2` (shorter), and *Echo types record the lineage* of the |
| 92 | +path actually taken. The shortest path may *route through other number |
| 93 | +systems* (`x → … → z`, switching representation mid-path) when that is |
| 94 | +shorter; Echo then carries the *cross-system* provenance. |
| 95 | + |
| 96 | +Consequence: number systems are not merely supported types — they are |
| 97 | +*path-optimisation spaces*, and Echo is the provenance of which spaces |
| 98 | +a computation traversed and what (if anything) was lost crossing them. |
| 99 | + |
| 100 | +=== D5 — Reversal strategy is a fallback ladder (algorithmic, else step down) |
| 101 | + |
| 102 | +Reverse "wherever possible" is *algorithmic*; where an algorithmic |
| 103 | +inverse is infeasible, *step down through lesser tiers of reversibility* |
| 104 | +rather than abandon it outright. This is precisely the Echo lattice read |
| 105 | +as a strategy: |
| 106 | + |
| 107 | +* *Safe* — algorithmic, bijective reverse; no residue needed. |
| 108 | +* *Neutral* — reverse only *from retained lineage* (a residue / linear |
| 109 | + `ReversalToken`, Bennett-style). This is the v2 "(c)" bridge. |
| 110 | +* *Breaking* — no reverse even with lineage; forward-only. |
| 111 | + |
| 112 | +=== D6 — The Echo tier of a number system is fixed by its additive algebra |
| 113 | + |
| 114 | +The unifying result. The algebraic structure of a number system's |
| 115 | +"addition" determines, *a priori*, the best reversibility tier |
| 116 | +attainable in it: |
| 117 | + |
| 118 | +[cols="1,2,2,1",options="header"] |
| 119 | +|=== |
| 120 | +| Additive structure | Example | Reverse addition? | Echo tier |
| 121 | + |
| 122 | +| Group | `ℤ` | always, algorithmic | *Safe* |
| 123 | +| Cancellative monoid | `ℕ` (`a+b=a+c ⇒ b=c`) | only *given the lineage/residue* | *Neutral* |
| 124 | +| Idempotent monoid | tropical / max-plus, lattices, `min`/`max`/`∪` | never, even with lineage | *Breaking* |
| 125 | +|=== |
| 126 | + |
| 127 | +Therefore "switching number system for a shorter path" (D4) also |
| 128 | +*switches reversibility tier*, and Echo records both the hop and the |
| 129 | +residue that a later reverse would require. |
| 130 | + |
| 131 | +[NOTE] |
| 132 | +==== |
| 133 | +*Self-reference / open challenge.* JtV's own Echo lattice |
| 134 | +`{Safe ⊑ Neutral ⊑ Breaking}` under join is itself an *idempotent* |
| 135 | +monoid (`join_idem` is a proved theorem) — so it has **no inverse**, |
| 136 | +which is *why* `Breaking` is one-way and you cannot "un-join" back to |
| 137 | +`Safe`. The standing question "is there a number system with no |
| 138 | +subtraction equivalent at all (not even reverse addition)?" is answered |
| 139 | +*yes* — any non-trivial idempotent additive structure (tropical |
| 140 | +semirings, lattices). In such systems the D5 ladder is *forced*: Safe |
| 141 | +is impossible, so one must keep a residue (Neutral) or accept Breaking. |
| 142 | +==== |
| 143 | + |
| 144 | +== Consequences |
| 145 | + |
| 146 | +. *Number-system semantics work (next-but-one priority).* The Lean model |
| 147 | + is currently `Int`-only (`evalDataExpr : DataExpr → State → Int`); |
| 148 | + the seven systems are *typed* but `stated-unproven` at the value |
| 149 | + level, and `type_preservation` is mechanised only for `τ = int`. The |
| 150 | + semantics layer must (a) give each system a value model, (b) classify |
| 151 | + each by its additive algebra → Echo tier per D6, and (c) keep |
| 152 | + addition-only (D1) — `×`/`÷` generated, not primitive. |
| 153 | +. *v2 "(c)" bridge.* Implements the Neutral tier of D5: `reverse { }` |
| 154 | + stays Safe-only; `reversible { } -> tok` admits Neutral via the |
| 155 | + retained log/token (Bennett). Lean: extend `JtvEcho` with |
| 156 | + `admissibleWithResidue` + a "Neutral recoverable given its token" |
| 157 | + theorem mirroring `rev_forward_backward`. Runtime: `reversible.rs` |
| 158 | + must record/invert residue for Neutral, or the gate stays |
| 159 | + conservative with the scope documented. |
| 160 | +. *Revisit `DataExpr.neg`* per the D2 note. |
| 161 | +. *Identity preserved.* D1–D3 confirm v2/Echo do **not** erode JtV: |
| 162 | + injection-impossibility rests on `no_control_to_data_flow` + disjoint |
| 163 | + Data/Control types + data-inertness; the Data plane stays total, |
| 164 | + pure, addition-only; Echo is a third orthogonal axis living in |
| 165 | + Control's reverse blocks. |
| 166 | + |
| 167 | +== References |
| 168 | + |
| 169 | +* `verification/PROOF-CAPABILITY-MATRIX.adoc` — authoritative proof status. |
| 170 | +* `jtv_proofs/JtvEcho.lean` — Echo lattice + admissibility (impl-semantics source of truth). |
| 171 | +* `jtv_proofs/JtvTheorems.lean` — `rev_forward_backward`, totality, flow separation. |
| 172 | +* `jtv_proofs/JtvSecurity.lean` — `no_control_to_data_flow`, `no_reverse_joinpoints`, `AOLDGuarantee`. |
| 173 | +* PRs #26 (proof repair + structural Echo gate + CI root-fix), #27 (believeme de-vacuation). |
0 commit comments