From b743dbefa60b292e40b052e21d3b602a3802e4f1 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 13 Jun 2026 07:26:07 +0000 Subject: [PATCH 1/2] docs: ADR-0007 (addition-only mandate + Echo reversibility tiering) + STATE refresh MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Durable capture of the 2026-06 design basis so it survives context loss. * docs/design-decisions/0007-…: records the core mandates re-affirmed in the 2026-06 sessions — - D1 addition-only is absolute (no ×, no primitive −; ×/÷ generated, not Data primitives); - D2 subtraction = REVERSE addition (not twos-complement, not a primitive) — flags the open `DataExpr.neg`-as-primitive tension; - D3 Turing-completeness via a Harvard block embedded in a von-Neumann host, both graftable as AOLD aspects (universal extender); - D4 computation = shortest-path-to-equality with Echo recording lineage (incl. cross-number-system routing); - D5 reversal is a fallback ladder: algorithmic (Safe) → residue/token (Neutral, Bennett) → Breaking; - D6 the additive algebra of a number system fixes its Echo tier: group→Safe, cancellative monoid→Neutral, idempotent monoid→Breaking (Echo's own join is idempotent — why Breaking is one-way; answers "a number system with no subtraction at all" = idempotent semirings). * .machine_readable/6a2/STATE.a2ml: reflect PR #26 (Lean repair + Echo structural type-system gate + root-cause Rust-CI revival), PR #27 (de-vacuation of 8 True-typed believeme theorems), ADR-0007, the reordered next-actions (governance hardening → number-system semantics → v2 (c) bridge → (b)), and the Int-only semantic-scope gap. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .machine_readable/6a2/STATE.a2ml | 28 ++- ...nly-mandate-and-reversibility-tiering.adoc | 173 ++++++++++++++++++ 2 files changed, 193 insertions(+), 8 deletions(-) create mode 100644 docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 0ec1ebd..54a2b30 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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,7 +37,11 @@ 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] @@ -45,15 +49,18 @@ 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" diff --git a/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc b/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc new file mode 100644 index 0000000..57fad1c --- /dev/null +++ b/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 + += ADR-0007: Addition-Only Mandate, Reverse Addition, and the Echo Reversibility Tiering +Jonathan D.A. Jewell +: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). From 9c99712a18c2e79e142eec4fb1839f48bc913622 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 13 Jun 2026 07:30:26 +0000 Subject: [PATCH 2/2] chore(hypatia): exempt frozen-archive placeholder DB password (false-positive) Hypatia flags a CRITICAL js_hardcoded_secret in playground/experiments/_attic/database-demos/arangodb-demo/queries.js (`password: "rootpassword"`). That is a placeholder in the FROZEN demo archive (_attic/, see FROZEN.md), not a real credential and not shipped code, so it re-fires on every PR. Exempt it via .hypatia-ignore, matching the existing per-file:rule convention. Note: whether to keep the frozen _attic archive or delete it is a checkpoint decision for the maintainer; this only silences the recurring false-positive in the interim. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .hypatia-ignore | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.hypatia-ignore b/.hypatia-ignore index 66163e3..fe83feb 100644 --- a/.hypatia-ignore +++ b/.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