diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 4c7998b..e5b9209 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-15" +last-updated = "2026-06-18" status = "active" -session = "2026-06-15 — bookkeeping/tidying consolidation: lake build green (8 libs, 0 sorry/admit/axiom, 0 vacuity, 0 lint warnings); 4 stray branches resolved (2 stale-merged flagged for UI deletion — git push --delete returned 403 — + codeql weekly->monthly cron folded + estate-standardization salvaged: CODEOWNERS + 17 wiki SPDX headers); ADR-0007 gains the graded-comonad/tropical-grade characterization note; PMPL-1.0 vs MPL-2.0 header discrepancy flagged for governance decision (gap-006); v2 (c) Neutral reversal bridge LANDED (Lean + Rust, green); number-system-semantics (gap-005) remains the next rung" +session = "2026-06-18 — Echo arc completed + number systems stratified. (b) Echo+Epistemic first-class DONE (proof side, ADR-0009): JtvEcho.lean SECTION 5 = Epistemic lattice + Echo×Epistemic product FunctionEffect lattice + comm/assoc/idem composition laws (matching the already-merged echo.rs/epistemic.rs/effect.rs). Number systems STRATIFIED (ADR-0007 D6 realized as ADR-0010): JtvEcho.lean SECTION 6 3-level NumAlgebra tower 1:1 with the Echo lattice (hex/binary=ℤ-encodings collapse to int's tier; float=approxGroup→Neutral); echo.rs carrier-aware classification (CarrierEnv; reversible += graded shape⊔carrier; default-carrier=Int sound) + effect.rs param-seeded env; number.rs runtime-value bridge Value::reversal_echo. PR #44 merged (rebase); bridge+ADR-0010 PR next. lake + cargo green (124 lib tests, 0 sorry/unwrap). NEXT rung: float-LOCALS soundness slice (thread typechecker inferred types into CarrierEnv) + value-level semantics (gap-005)" [project-context] name = "Julia The Viper" @@ -50,22 +50,22 @@ issues = [ { 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-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" }, + { 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). PARTIAL 2026-06-18 (ADR-0010): per-system additive-algebra → Echo-tier CLASSIFICATION now landed at proof/type/value level (JtvEcho SECTION 6, echo.rs carrier_echo, number.rs Value::reversal_echo); the remaining open half is the type_preservation/round-trip SEMANTICS beyond τ=int", severity = "medium", status = "known", follow-up = "value-level semantics for τ≠int; float-locals CarrierEnv inference slice" }, { id = "gap-006", description = "RESOLVED 2026-06-15: license decision = MPL-2.0 (code) + CC-BY-SA-4.0 (docs), full per-file. 75 doc headers -> CC-BY-SA-4.0; code stragglers (3 PMPL-1.0 workflows, MPL-2.0-or-later, PLMP/GPL typos, and a deliberate MIT-OR-GPL-3.0-or-later-OR-Palimpsest tri-license on formatter/repl/rsr_check) -> MPL-2.0; PALIMPSEST.adoc (both copies) retired; LICENSING.md rewritten; PMPL badges replaced. Follow-ups: populate LICENSES/ with canonical MPL-2.0 + CC-BY-SA-4.0 texts; add SPDX headers to ~49 header-less docs.", severity = "low", status = "resolved", follow-up = "LICENSES/ texts + header-less docs" } ] [critical-next-actions] actions = [ "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", + "Number-system stratification (ADR-0007 D6 / ADR-0010) — LANDED 2026-06-18: per-system additive-algebra → Echo-tier classification at proof level (JtvEcho.lean SECTION 6), type level (echo.rs carrier_echo + CarrierEnv carrier-aware += grading, effect.rs param-seeded env) and value level (number.rs Value::reversal_echo). STILL OPEN: (a) thread typechecker INFERRED types into CarrierEnv so float LOCALS grade Neutral — param-only today, so a reverse{} over a float local is wrongly Safe-admitted (soundness slice, NEXT); (b) lift type_preservation semantics beyond τ=int (gap-005); keep addition-only (×/÷ generated)", "v2 (c) token/residue neutral-reversal bridge — LANDED 2026-06-15 (ADR-0007 D5 Neutral tier): JtvEcho admissibleWithResidue + blockEcho_admissibleWithResidue; JtvTheorems execBackwardWithToken + rev_forward_backward_with_token + rev_backward_naive_fails_self_ref; echo.rs self-ref Breaking->Neutral; typechecker.rs check_echo_admissible_with_residue (token unlocks Neutral); reversible.rs RecordedOp::Snapshot residue. NEXT: (b) Echo as a first-class function effect", - "Echo as first-class function effect ('(b)') — after (c) stabilises", + "Echo as first-class function effect ('(b)') — LANDED 2026-06-18 (ADR-0009): echo.rs function_echo + epistemic.rs function_epistemic + effect.rs FunctionEffect row + resolved_effects call-graph fixpoint; JtvEcho.lean SECTION 5 mechanises the Echo×Epistemic product lattice + comm/assoc/idem composition laws", "Verification bridge: correlation tests between Lean semantics and Rust interpreter", "PataCL Phase 1 → unblocks JtV coproc implementation Phase 2" ] [maintenance-status] -last-run-utc = "2026-06-15T00:00:00Z" +last-run-utc = "2026-06-18T00:00:00Z" last-result = "pass" # unknown | pass | warn | fail [session-history] @@ -86,7 +86,8 @@ sessions = [ { 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-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." }, - { date = "2026-06-18", subject = "neg-dialect impl slice 1 + ADR-0009. PR #39 merged: jtv-core dialect.rs purity certificate (ADR-0008 D4) -- read-only AST scan stamping a program purist-jtv vs adulterated-jtv by counting expression-level neg sugar; reverse-block subtraction stays purist; 5 tests; cleared a self-introduced Hypatia unwrap_dangerous_default critical via Option::iter().sum(). ADR-0009 (this commit): Echo + Epistemic as first-class GRADED FUNCTION EFFECTS -- Echo grade {Safe<=Neutral<=Breaking} carried in the arrow, composing by the existing join; Epistemic = knowledge/observability axis {Opaque<=Partial<=Transparent} as a parallel graded effect (dual to Echo: loss vs revelation); product-lattice effect row; orthogonal to Purity + the dialect certificate. Implementation slice-wise (Echo-effect first). Still parked: (b) impl, number-system semantics, license wave-2, standards-blocked hardening (secret-scanner/scorecard)." } + { date = "2026-06-18", subject = "neg-dialect impl slice 1 + ADR-0009. PR #39 merged: jtv-core dialect.rs purity certificate (ADR-0008 D4) -- read-only AST scan stamping a program purist-jtv vs adulterated-jtv by counting expression-level neg sugar; reverse-block subtraction stays purist; 5 tests; cleared a self-introduced Hypatia unwrap_dangerous_default critical via Option::iter().sum(). ADR-0009 (this commit): Echo + Epistemic as first-class GRADED FUNCTION EFFECTS -- Echo grade {Safe<=Neutral<=Breaking} carried in the arrow, composing by the existing join; Epistemic = knowledge/observability axis {Opaque<=Partial<=Transparent} as a parallel graded effect (dual to Echo: loss vs revelation); product-lattice effect row; orthogonal to Purity + the dialect certificate. Implementation slice-wise (Echo-effect first). Still parked: (b) impl, number-system semantics, license wave-2, standards-blocked hardening (secret-scanner/scorecard)." }, + { date = "2026-06-18", subject = "Echo arc completed + number-system stratification (PR #44 merged via rebase → main: SECTION 5+6 + carrier-aware echo; then bridge+ADR-0010 PR). (b) Echo+Epistemic first-class DONE on the proof side: JtvEcho.lean SECTION 5 = Epistemic lattice (hidden/bounded/full) + Echo×Epistemic product FunctionEffect lattice + comm/assoc/idem composition laws (mirrors the already-merged echo.rs/epistemic.rs/effect.rs). Number systems STRATIFIED (ADR-0007 D6 realized as ADR-0010): JtvEcho.lean SECTION 6 = 3-level NumAlgebra tower (abelianGroup/approxGroup/nonGroup) 1:1 with the Echo lattice; theorems hex_binary_collapse (hex/binary are ℤ-encodings, share int's tier) / exact_groups_safe / float_not_safe (IEEE-754 non-associative → approxGroup → Neutral) / no_current_system_breaks / reversal_tier_by_algebra. echo.rs made carrier-aware: NumAlgebra/additive_algebra/carrier_echo + CarrierEnv threaded through classify_*_in_env/function_echo_in_env; a reversible += is graded shape⊔carrier (float += → Neutral); shape-only wrappers preserve prior behaviour (empty env ⇒ Int=Safe); default-carrier=Int is sound (literals default to int). effect.rs own_effect seeds the env from param annotations. number.rs runtime-value bridge Value::number_system + Value::reversal_echo (delegates to carrier_echo — single source of truth). ADR-0010 reconciles with ADR-0007 D6 (float is approxGroup not D6-cancellative; D6's cancellative/idempotent Neutral/Breaking routes anticipated-but-uninhabited). lake + cargo fmt/clippy/test green (124 lib tests), 0 sorry/admit/axiom, no unwrap/unwrap_or. OPEN: float-LOCALS soundness slice (locals carry no annotation → thread typechecker inferred types into CarrierEnv, else a reverse{} over a float local is wrongly Safe-admitted); value-level type_preservation beyond τ=int (gap-005)." } ] [design-artefact-locations] @@ -94,6 +95,7 @@ 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" echo-epistemic-effects-adr = "docs/design-decisions/0009-echo-epistemic-first-class-function-effects.adoc" +number-system-stratification-adr = "docs/design-decisions/0010-number-system-stratification.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/crates/jtv-core/src/number.rs b/crates/jtv-core/src/number.rs index 3751d4b..698f859 100644 --- a/crates/jtv-core/src/number.rs +++ b/crates/jtv-core/src/number.rs @@ -1,5 +1,6 @@ // Number system implementation supporting 7 types -use crate::ast::Number; +use crate::ast::{BasicType, Number}; +use crate::echo::{carrier_echo, Echo}; use crate::error::{JtvError, Result}; use num_complex::Complex64; use num_rational::Ratio; @@ -26,6 +27,50 @@ pub enum Value { Unit, } +// ============================================================================ +// NUMBER-SYSTEM STRATIFICATION — runtime-value bridge to Echo (ADR-0010) +// ============================================================================ +// The runtime-value counterpart of the type-level `echo::carrier_echo` +// (`BasicType -> Echo`) and the Lean `JtvEcho.lean` SECTION 6 stratification: +// a runtime `Value`'s reversal tier is forced by the additive algebra of its +// number system. The algebra -> tier map is NOT duplicated here — it is taken +// from `echo::carrier_echo`, so there is a single source of truth. + +impl Value { + /// The number system this runtime value belongs to, or `None` for the + /// non-numeric carriers (bool / string / list / tuple / token / unit) — + /// which have no additive algebra and so cannot be `+=` targets. + pub fn number_system(&self) -> Option { + Some(match self { + Value::Int(_) => BasicType::Int, + Value::Float(_) => BasicType::Float, + Value::Rational(_) => BasicType::Rational, + Value::Complex(_) => BasicType::Complex, + Value::Hex(_) => BasicType::Hex, + Value::Binary(_) => BasicType::Binary, + Value::Symbolic(_) => BasicType::Symbolic, + Value::Bool(_) + | Value::String(_) + | Value::List(_) + | Value::Tuple(_) + | Value::ReversalToken(_) + | Value::Unit => return None, + }) + } + + /// The Echo reversal tier forced by this value's additive algebra — the + /// runtime-value counterpart of `echo::carrier_echo` and `JtvEcho.lean` + /// SECTION 6 (`abelianGroup -> Safe`, `approxGroup -> Neutral`, + /// `nonGroup -> Breaking`). A non-numeric value induces no additive-reversal + /// obligation, hence `Safe`. + pub fn reversal_echo(&self) -> Echo { + match self.number_system() { + Some(ty) => carrier_echo(&ty), + None => Echo::Safe, + } + } +} + impl Value { // Addition operation (the only arithmetic operation in Data Language) pub fn add(&self, other: &Value) -> Result { @@ -338,4 +383,34 @@ mod tests { let result = a.add(&b).unwrap(); assert!(matches!(result, Value::Float(_))); } + + #[test] + fn value_number_system_maps_carriers() { + assert_eq!(Value::Int(0).number_system(), Some(BasicType::Int)); + assert_eq!(Value::Float(0.0).number_system(), Some(BasicType::Float)); + assert_eq!(Value::Hex(0).number_system(), Some(BasicType::Hex)); + assert_eq!(Value::Binary(0).number_system(), Some(BasicType::Binary)); + assert_eq!( + Value::Symbolic("x".to_string()).number_system(), + Some(BasicType::Symbolic) + ); + // Non-numeric carriers have no additive algebra. + assert_eq!(Value::Bool(true).number_system(), None); + assert_eq!(Value::Unit.number_system(), None); + assert_eq!(Value::ReversalToken(0).number_system(), None); + } + + #[test] + fn value_reversal_echo_mirrors_section6() { + // Exact abelian groups -> Safe (incl. the ℤ-encodings hex/binary). + assert_eq!(Value::Int(0).reversal_echo(), Echo::Safe); + assert_eq!(Value::Hex(0).reversal_echo(), Echo::Safe); + assert_eq!(Value::Binary(0).reversal_echo(), Echo::Safe); + assert_eq!(Value::Symbolic("x".to_string()).reversal_echo(), Echo::Safe); + // Float -> Neutral (non-associative, lossy reverse-add). + assert_eq!(Value::Float(1.5).reversal_echo(), Echo::Neutral); + // Non-numeric -> Safe (no additive-reversal obligation). + assert_eq!(Value::Bool(true).reversal_echo(), Echo::Safe); + assert_eq!(Value::Unit.reversal_echo(), Echo::Safe); + } } diff --git a/docs/design-decisions/0010-number-system-stratification.adoc b/docs/design-decisions/0010-number-system-stratification.adoc new file mode 100644 index 0000000..027f1f6 --- /dev/null +++ b/docs/design-decisions/0010-number-system-stratification.adoc @@ -0,0 +1,155 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell + += ADR-0010: Number-System Stratification by Additive Algebra +Jonathan D.A. Jewell +:revdate: 2026-06-18 +:revnumber: 0.1 +:toc: left +:sectnums: + +[.lead] +Realizes ADR-0007 D6 ("additive algebra fixes the reversibility tier") for JtV's +seven number systems. The reversal `Echo` of `+` over a carrier is *not* a +per-system stipulation: it is read off the carrier's additive algebra by a +single map. Adding a number system becomes *stratification* — classify it by its +algebra — not a re-proof of the reversibility spine. + +== Status + +*Decided (2026-06-18).* Proof layer and type-/value-level classifiers landed +(PR #44 + this PR). One slice remains open for soundness over float *locals* +(see Open / deferred). Realizes ADR-0007 D6; refines its tier vocabulary for the +floating-point case. + +== Context + +* ADR-0007 D6 states the principle as `group -> Safe / cancellative -> Neutral / + idempotent -> Breaking`: the additive algebra of a carrier determines whether + reverse-add is exact, structurally lossy, or impossible. +* `gap-005`: JtV's semantic model is Int-only — the seven systems are *typed* + but value-level reversibility was stated-unproven beyond `int`. +* Echo (`echo.rs` / `JtvEcho.lean`) is a 3-valued lattice + `Safe ⊑ Neutral ⊑ Breaking`. A tier map therefore has a 3-valued codomain. + +== Decision + +=== D1 — A 3-level additive-algebra tower, 1:1 with the Echo lattice + +[source] +---- +NumAlgebra reverse-add Echo +---------- ----------- ---- +abelianGroup total & exact (exact inverses) Safe +approxGroup lossy (non-associative / rounding) Neutral +nonGroup impossible (+ not invertible) Breaking +---- + +Three levels suffice precisely because the Echo codomain is 3-valued: a finer +carrier tower (`Monoid ⊂ CancellativeMonoid ⊂ Group`) would collapse onto the +same three tiers. + +=== D2 — Classification of the seven systems + +[cols="1,1,1",options="header"] +|=== +| System | Additive algebra | Echo + +| int, rational, complex, symbolic | abelianGroup | Safe +| hex, binary | abelianGroup (= int) | Safe +| float | approxGroup | Neutral +|=== + +* *hex/binary collapse:* hex and binary are *encodings of ℤ*, not distinct + algebras (the `JtvType` constructors are literally "represented as int"), so + they carry int's tier exactly. Encoding ≠ algebra. +* *float is the qualified case:* IEEE-754 `+` is non-associative + (`(a+b)+c ≠ a+(b+c)`) and non-cancellative under rounding + (`(x+v)-v ≠ x`), so reverse-add is lossy — `Neutral`, not `Safe`. This is the + one place the surface slogan "addition-only ⇒ reversible" is qualified by the + carrier. +* *Breaking is presently empty,* reserved for a future non-invertible system. + +=== D3 — Reconciliation with ADR-0007 D6 (honest note) + +D6's vocabulary is `group / cancellative / idempotent`, chosen for *exact* +algebras (ℤ a group, ℕ a cancellative monoid, tropical/min-plus idempotent). +The realized tower here is `abelianGroup / approxGroup / nonGroup`. They are not +the same decomposition, and float is why: + +* float has (exact) additive inverses yet is *not a group* (non-associative), so + it sits in neither D6 `group` nor D6 `cancellative`; it is an *approximate* + group. The `approxGroup` level names this realized inhabitant of the `Neutral` + tier. +* Among the seven systems, D6's `cancellative` Neutral-route (e.g. ℕ) and its + `idempotent` Breaking-route (tropical) are *anticipated but uninhabited*. + Were ℕ or a tropical system added, both towers agree at the `Echo` level + (cancellative ⇒ Neutral, idempotent ⇒ Breaking) — they meet at + `Safe/Neutral/Breaking`. D6 is the principle; this ADR is the realized map. + +=== D4 — Carrier-aware Echo classification + +Echo classification of a reversible `+=` is graded by the *join* of two +independent loss sources: + +[source] +---- +echo(x += v) = shape(x += v) ⊔ carrier_echo(typeof x) +---- + +* `shape` — self-reference (`x += x`) is `Neutral` (token-recoverable), else + `Safe`. +* `carrier_echo` — the D1 map applied to the target's number system; `float` + lifts the grade to `Neutral` regardless of shape. + +A `CarrierEnv` (variable -> `BasicType`) is threaded through classification. +*Default-carrier soundness:* a variable absent from the env is treated as `Int` +(`Safe`), not "unknown-lossy". JtV numeric literals default to `int` +(`inferType (lit _) = int` in Lean), so an unannotated numeric *is* int; the only +lossy carrier (float) is exactly the one that must be annotated/inferred to +exist — so the default cannot under-report loss for a *typed* program. + +=== D5 — One algebra, three surfaces + +The algebra -> tier map has a single home and is mirrored, not duplicated: + +* *Proof:* `JtvEcho.lean` SECTION 6 (`NumAlgebra`, `NumSystem.echo`, + `hex_binary_collapse`, `float_not_safe`, `reversal_tier_by_algebra`). +* *Type level:* `echo.rs` `additive_algebra` / `carrier_echo` (`BasicType -> + Echo`), consumed by the carrier-aware classifiers and `effect::own_effect`. +* *Value level:* `number.rs` `Value::number_system` / `Value::reversal_echo` + (runtime value -> Echo), delegating to `echo::carrier_echo`. + +== Consequences + +. *Proof layer — landed (PR #44).* SECTION 6 stratification under + `--safe`-equivalent discipline (zero `sorry`/`admit`/`axiom`). +. *Type-level carrier-aware Echo — landed (PR #44).* `float` `+=` grades + `Neutral` when the carrier is known; shape-only wrappers keep all prior + behaviour (empty env ⇒ Int). +. *Runtime-value bridge — landed (this PR).* `Value::reversal_echo`. +. *`gap-005` partially addressed:* the seven systems are now *classified* by + additive algebra at type and value level. The orthogonal half — lifting + `type_preservation` semantics beyond `τ = int` — remains open. + +== Open / deferred + +* *Float-locals soundness slice (required, next).* The `CarrierEnv` is seeded + from *parameter* annotations only. JtV locals carry no annotation (the + `Assignment` node has no type field), so a float *local* — typed only by + inference — currently grades `Safe`, and a `reverse { z += v }` over it would + be wrongly admitted under the Safe-only policy. Closing this needs the + typechecker's *inferred* types threaded into the `CarrierEnv`. +* *Uninhabited D6 routes.* If ℕ (cancellative) or a tropical/min-plus + (idempotent) system is added, give it its `NumAlgebra` level and the + Neutral/Breaking tier follows; no spine re-proof. +* *Value-level semantics (`gap-005`).* `type_preservation` / round-trip proofs + for `τ ≠ int`. + +== References + +* `docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc` — D6 (algebra → tier), the principle realized here. +* `jtv_proofs/JtvEcho.lean` — SECTION 6 (stratification) + SECTION 1 (Echo lattice). +* `crates/jtv-core/src/echo.rs` — `additive_algebra` / `carrier_echo` / `CarrierEnv` (type level). +* `crates/jtv-core/src/number.rs` — `Value::number_system` / `Value::reversal_echo` (value level). +* `docs/design-decisions/0009-echo-epistemic-first-class-function-effects.adoc` — Echo as a function effect (consumes the carrier grade).