diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 92e1864..c8d5b1a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -84,12 +84,14 @@ sessions = [ { 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)" }, { date = "2026-06-15", subject = "Bookkeeping/tidying consolidation: confirmed lake build green (8 libs); cleared all Lean unused-variable lint warnings (_-prefix); resolved 4 stray remote branches (flagged 2 stale-merged changelog/tech-debt for UI deletion — content already on main, git 403 blocked programmatic delete; folded codeql weekly->monthly cron; salvaged CODEOWNERS + 17 wiki SPDX headers from estate-standardization-20260607, dropped its superseded pre-repair Lean drafts + old contractiles); ADR-0007 graded-comonad/tropical-grade characterization note; flagged PMPL-1.0 vs MPL-2.0 discrepancy (gap-006)" }, { date = "2026-06-15", subject = "Security-hygiene clean (post-#33): triaged the Hypatia 67-finding report — informational (--exit-zero, gate passed), none originating from #33. Added CodeQL actions language; DELETED the frozen playground/experiments/_attic archive (17 files incl. stray npm package.json + a Julia demo), clearing both criticals + several highs at the source, with all dangling refs cleaned (deno.json excludes, bot_directives/hypatia.a2ml, .hypatia-ignore, playground README/Justfile); documented rsr_check.rs unsafe_block as a verified false-positive (Hypatia matched the RSR checker's own detection string). Deferred to a deliberate governance-hardening pass: secret-scanner.yml creation, scorecard job-perms, curl|sh install hardening." }, - { date = "2026-06-15", subject = "v2 (c) Neutral reversal bridge LANDED (Lean + Rust). Lean: JtvTheorems execBackwardWithToken + rev_forward_backward_with_token (full-state Bennett recovery, unconditional even for self-referential x += x) + rev_backward_naive_fails_self_ref (token necessary); JtvEcho admissibleWithResidue + blockEcho_admissibleWithResidue + admissible_implies_admissibleWithResidue + neutral_residue_only. Rust: echo.rs reclassifies self-reference Breaking->Neutral (token-recoverable, not erasure; Breaking reserved for future non-group/tropical systems per D6); typechecker.rs splits the Echo gate — reversible{}->tok uses check_echo_admissible_with_residue (admits Neutral; tokenless + reverse{} stay Safe-only); reversible.rs RecordedOp::Snapshot records/restores the residue. lake build + cargo test (99 lib + integration) + clippy -D warnings all green." } + { date = "2026-06-15", subject = "v2 (c) Neutral reversal bridge LANDED (Lean + Rust). Lean: JtvTheorems execBackwardWithToken + rev_forward_backward_with_token (full-state Bennett recovery, unconditional even for self-referential x += x) + rev_backward_naive_fails_self_ref (token necessary); JtvEcho admissibleWithResidue + blockEcho_admissibleWithResidue + admissible_implies_admissibleWithResidue + neutral_residue_only. Rust: echo.rs reclassifies self-reference Breaking->Neutral (token-recoverable, not erasure; Breaking reserved for future non-group/tropical systems per D6); typechecker.rs splits the Echo gate — reversible{}->tok uses check_echo_admissible_with_residue (admits Neutral; tokenless + reverse{} stay Safe-only); reversible.rs RecordedOp::Snapshot records/restores the residue. lake build + cargo test (99 lib + integration) + clippy -D warnings all green." }, + { date = "2026-06-17", subject = "License + hardening + ADR-0008. License (gap-006 RESOLVED, PR #36 merged): full per-file SPDX = MPL-2.0 (code) + CC-BY-SA-4.0 (docs); 190 MPL + 77 CC-BY-SA headers; PALIMPSEST.adoc retired; LICENSING.md rewritten; stray MIT/GPL/PMPL/or-later normalised. (PR #34 security clean + #35 v2-c bridge also merged earlier.) Workflow hardening (PR #37 merged): curl|sh installers (proof-regression elan, setup.sh just) -> download-then-run; rsr_check.rs unsafe_block self-trip cleared. Deferred (need hyperpolymath/standards reusable, out of session MCP scope): secret-scanner.yml, scorecard.yml job-perms. ADR-0008 (this commit): neg -> reverse-only; purist/adulterated dialect via feature-gated sugar + discouragement lint + purity certificate (resolves ADR-0007 D2); implementation is follow-on." } ] [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" +neg-dialect-adr = "docs/design-decisions/0008-neg-reverse-only-and-purist-dialect.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" diff --git a/docs/design-decisions/0008-neg-reverse-only-and-purist-dialect.adoc b/docs/design-decisions/0008-neg-reverse-only-and-purist-dialect.adoc new file mode 100644 index 0000000..c53cad0 --- /dev/null +++ b/docs/design-decisions/0008-neg-reverse-only-and-purist-dialect.adoc @@ -0,0 +1,122 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell + += ADR-0008: `neg` is Reverse-Only — the Purist / Adulterated Dialect Split +Jonathan D.A. Jewell +:revdate: 2026-06-18 +:revnumber: 0.1 +:toc: left +:sectnums: + +[.lead] +Resolves the `DataExpr.neg` open tension flagged in ADR-0007 D2. Subtraction is +*reverse addition* (effect-level) in every number system; expression-level +`neg` is a convenience that escapes that discipline. This ADR moves `neg` out of +the purist core into an optional, feature-gated *sugar* aspect, so JtV ships as +two structurally-distinct dialects — *purist* and *adulterated* — and the +compiler stamps every program with a *purity certificate*. + +== Status + +*Decided (2026-06-18).* Resolves the ADR-0007 D2 open tension. Constrains the +Data-plane grammar and the v2 toolchain. Implementation is staged: this ADR is +the decision record; the feature-gating, lint, and certificate are follow-on +work. + +== Context + +ADR-0007 D2 mandated subtraction = reverse addition and flagged the surviving +`DataExpr`/`Negate` (Lean `DataExpr.neg`) *primitive* as an open tension: it lets +a program write expression-level negation/subtraction (`x + neg y`) directly in +the total Data plane, bypassing the reverse/echo mechanism. + +The mission is pedagogical as much as technical: *get people to think differently +about subtraction.* But users must not be hard-limited — if someone wants the old +way to get a job done, that is their choice; JtV simply should not make it the +path of least resistance, and should make its use *visible*. + +=== The level mismatch (why `neg` is tempting) + +Subtraction-as-reverse-addition is an **effect-level** operation: a +`reverse { x += b }` statement that *inverts* a forward step, operating on a +variable, with a token (ADR-0007 D5; the v2 "(c)" Neutral bridge). But `a - b` / +`neg y` is an **expression-level** value — pure, no effect, no token. They live on +different planes. `neg` exists precisely *because* expression-level subtraction +cannot be written as a reverse block (a Control-plane effect is not a Data-plane +value). That mismatch is the whole reason `neg` is the convenient escape hatch, +and the reason a purist should refuse it. + +== Decision + +=== D1 — `neg` leaves the purist core; subtraction is reverse-only there + +The purist Data grammar has **no `neg` / `-` primitive**. In *purist-jtv*, writing +`-` is a *parse error*; the only way to subtract is a `reverse` / `reversible` +block (effect-level), which forces the reverse-addition mindset. This holds for +every number system — the reversibility tier is fixed by its additive algebra +(ADR-0007 D6), and the effect-level reverse *is* the subtraction in each. + +=== D2 — Sugar is an optional, feature-gated aspect (adulterated-jtv) + +`neg` / `-` is re-admitted only under an explicit *sugar* aspect (a compiler +feature / parser mode). *adulterated-jtv* = purist core **+** sugar. The sugar is +structurally separable: the purist core does not contain it. This matches the +AOLD philosophy of ADR-0007 D3 — sugar is just another graftable aspect. + +=== D3 — Sugar works, but is discouraged (a lint, not a wall) + +When sugar is enabled and `neg` / `-` is used, the compiler emits a +*discouragement diagnostic* ("subtraction sugar used — prefer reverse-addition"). +It still compiles and runs; it is not blocked. Users are not limited; the +language simply *nags*, keeping the old way available but non-default. + +=== D4 — The compiler emits a purity certificate + +Every build is stamped *purist* or *adulterated* (and, if adulterated, which +sugar it used). This is the "co-product / pre-final product": the artifact +carries a badge, so reaching for the escape hatch is *visible and accountable*, +not silent. This is the load-bearing piece for the mission — accountability +without prohibition. + +=== D5 — Chosen rung: feature-gated dialect (rungs 2 and 3 are future-purer) + +Three architectures were considered, increasing in purity and cost: + +. *Feature-gated dialect (CHOSEN).* `neg` behind a `sugar` feature; purist mode + rejects it at parse time; adulterated mode admits it with the D3 lint. One + codebase, low cost. +. *Sidecar desugarer.* A separate front-end pass rewrites adulterated → purist + before the core compiler sees anything; the core knows *only* purist-jtv. + Cleanest core, but the level mismatch means `a - b` cannot desugar to a pure + expression — the honest version lifts it into a hidden reverse-computation + (heavier); the dishonest version is a thin alias to a primitive `neg`. + Deferred as a future purity upgrade. +. *Co-product grammar.* Two grammars `Core ⊕ Sugar`; purist-jtv literally cannot + *represent* `neg`. Most principled (pure AOLD), most plumbing. Deferred. + +The feature-gated dialect (1) reaches the purist/adulterated split at low cost and +keeps (2)/(3) open as later purity upgrades. + +== Consequences + +. *Implementation (follow-on).* Add a `sugar` build feature / parser mode; gate the + `Negate` AST node + `-` lexing behind it; emit the D3 lint on use; emit the D4 + purity certificate (in the compiler's machine-readable output and as a header on + emitted artifacts). +. *Mechanisation.* The purist core's `DataExpr` drops `neg`, which *simplifies* the + core proofs (no `neg` cases). The existing `JtvExtended` negation theorems + (`neg_add_distrib`, `simplify_neg_neg`, `sub_eq_add_neg`, …) describe *adulterated* + semantics and move to a sugar/adulterated module, or are re-cast as the denotation + of the reverse mechanism rather than of a primitive. +. *Number systems (ADR-0007 D6).* Reverse-addition is the subtraction in every system + at the effect level; float's non-associative rounding (D6 note) makes its reverse + Neutral/approximate, never Safe — independent of this ADR. +. *Identity preserved.* This *strengthens* the addition-only mandate (D1 of ADR-0007): + the purist Data plane is now genuinely addition-only with no subtraction escape, + while pragmatic users keep an opt-in, accountable path. + +== References + +* `docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc` — D2 (the open tension), D3 (AOLD), D5 (reversal ladder), D6 (algebra → tier). +* `jtv_proofs/JtvExtended.lean` — the current `neg` theorems (to be re-homed under the sugar/adulterated reading). +* `crates/jtv-core/src/ast.rs` — `DataExpr::Negate` (to be feature-gated).