From a2e78833182d88efa51a71aa1204021470ab5804 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 06:57:42 +0000 Subject: [PATCH] =?UTF-8?q?feat(typechecker):=20carrier-aware=20Echo=20gat?= =?UTF-8?q?e=20=E2=80=94=20float=20locals=20soundly=20reject=20(ADR-0010)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the float-locals soundness gap flagged in ADR-0010: the Safe-only reverse gate now consults the carrier of the target variable, including float LOCALS. The Echo admissibility check runs at the reverse-block site inside check_control_stmt, where self.env already holds the INFERRED types of params and prior local assignments (locals carry no annotation, but `x = 2.5` records x : Float in the env). So check_echo_admissible / check_echo_admissible_with_residue now build a CarrierEnv from self.env (numeric Type -> BasicType; non-numeric and not-yet-inferred Any omitted -> default Int = Safe) and classify via echo::classify_stmts_in_env. Effect: * `reverse { x += v }` over a float local (or param) is correctly REJECTED under Safe-only -- float reverse-add is lossy (Neutral), was wrongly Safe-admitted before. * `reversible { x += v } -> tok` over a float still ADMITTED -- the token retains the rounding residue (Neutral admissible with residue). * int/rational/complex/symbolic/hex/binary unchanged (Safe). Contained change: no reordering, no new inference pass -- the inferred type env is already populated at the gate. 4 typechecker tests (float carrier rejected; inferred-float-local rejected end-to-end; int contrast ok; float reversible-tok admitted). Whole-suite check: nothing relied on float reverse{} being accepted, so the stricter rule breaks no existing test/example. ADR-0010 + STATE.a2ml updated: slice landed; remaining minor corner noted (carrier-awareness inside reversible-if branches). cargo fmt + clippy clean; 127 lib tests pass. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .machine_readable/6a2/STATE.a2ml | 9 +- crates/jtv-core/src/typechecker.rs | 111 +++++++++++++++++- .../0010-number-system-stratification.adoc | 28 +++-- 3 files changed, 131 insertions(+), 17 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index e5b9209..9cb5d7d 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -7,7 +7,7 @@ project = "julia-the-viper" version = "0.0.1" last-updated = "2026-06-18" status = "active" -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)" +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 + #45 (bridge+ADR-0010) merged; float-LOCALS soundness gate also LANDED (typechecker.rs check_echo_admissible{,_with_residue} seed CarrierEnv from the inferred env self.env → reverse{} over a float local correctly rejected, float routes to reversible{}->tok). lake + cargo green (127 lib tests, 0 sorry/unwrap). NEXT rung: value-level semantics beyond τ=int (gap-005)" [project-context] name = "Julia The Viper" @@ -50,14 +50,14 @@ 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). 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-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 (the float-locals CarrierEnv inference gate landed 2026-06-18)" }, { 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 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)", + "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), value level (number.rs Value::reversal_echo), and the carrier-aware TYPECHECKER GATE (typechecker.rs check_echo_admissible{,_with_residue} seed CarrierEnv from the inferred env self.env → reverse{} over a float LOCAL correctly rejected; float routes to reversible{}->tok). STILL OPEN: lift type_preservation semantics beyond τ=int (gap-005); carrier-awareness inside reversible-if branches (rare corner); 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)') — 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", @@ -87,7 +87,8 @@ sessions = [ { 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 = "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)." } + { 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)." }, + { date = "2026-06-18", subject = "Float-locals soundness slice (typechecker carrier-aware gate). Echo admissibility is checked at the reverse-block site inside check_control_stmt, where self.env already holds the INFERRED types of params + prior local assignments — so typechecker.rs check_echo_admissible{,_with_residue} now build a CarrierEnv from self.env (Type→BasicType for the 7 numeric Types; non-numeric/Any omitted → default Int=Safe) and call echo::classify_stmts_in_env. Effect: a reverse{} over a float LOCAL (typed only by inference, e.g. x = 2.5) is correctly REJECTED under Safe-only (was wrongly Safe-admitted); reversible{}->tok still admits it (token retains the rounding residue). Contained change (no reordering, no new inference pass). 4 typechecker tests (float carrier rejected; inferred-float-local rejected end-to-end; int contrast ok; float reversible-tok admitted). ADR-0010 §Status/§Consequences/§Open updated (slice landed; remaining minor corner = carrier-awareness inside reversible-if branches). cargo fmt/clippy/test green (127 lib tests; cleared a clippy approx_constant deny on a 3.14 literal → 2.5). Whole-suite check: no existing test/example relied on a float reverse{} being accepted, so the stricter rule broke nothing." } ] [design-artefact-locations] diff --git a/crates/jtv-core/src/typechecker.rs b/crates/jtv-core/src/typechecker.rs index e314d60..fe0b78f 100644 --- a/crates/jtv-core/src/typechecker.rs +++ b/crates/jtv-core/src/typechecker.rs @@ -424,6 +424,36 @@ impl TypeChecker { } } + /// Build the Echo `CarrierEnv` from the current type environment, so that + /// reverse-block classification is *carrier-aware*: every numeric variable + /// in scope (parameter or inferred local) contributes its number system, and + /// a `+=` over a `float` carrier therefore grades `Neutral` rather than + /// `Safe` (ADR-0010 / `JtvEcho.lean` SECTION 6). This is what makes the + /// Safe-only reversal gate *sound* over float *locals*: locals carry no + /// annotation, but their type has been inferred and recorded in `self.env` + /// by the time a reverse block is reached. Non-numeric and not-yet-inferred + /// (`Any`) variables are omitted — they fall back to the default `Int` + /// carrier (`Safe`) in `carrier_echo`. + fn carrier_env(&self) -> echo::CarrierEnv { + self.env + .vars + .iter() + .filter_map(|(name, ty)| { + let bt = match ty { + Type::Int => BasicType::Int, + Type::Float => BasicType::Float, + Type::Rational => BasicType::Rational, + Type::Complex => BasicType::Complex, + Type::Hex => BasicType::Hex, + Type::Binary => BasicType::Binary, + Type::Symbolic => BasicType::Symbolic, + _ => return None, + }; + Some((name.clone(), bt)) + }) + .collect() + } + /// Enforce the Echo admissibility rule for a plain `reverse { }` block (and /// a tokenless `reversible { }`) (spec v2 §9) under the **Safe-only** /// reversal policy: the block is well-typed iff its aggregate echo is @@ -434,7 +464,7 @@ impl TypeChecker { /// realisation of `blockEcho_admissible` in `jtv_proofs/JtvEcho.lean`; the /// residue (token) policy is `check_echo_admissible_with_residue`. fn check_echo_admissible(&self, body: &[ReversibleStmt]) -> Result<()> { - let aggregate = echo::classify_stmts(body); + let aggregate = echo::classify_stmts_in_env(body, &self.carrier_env()); if !aggregate.admissible_in_reverse() { return Err(JtvError::EchoViolation(format!( "reverse block has echo {aggregate}: it is not fully reversible. \ @@ -457,7 +487,7 @@ impl TypeChecker { /// the type-checker realisation of `blockEcho_admissibleWithResidue` in /// `jtv_proofs/JtvEcho.lean` (the v2 "(c)" Neutral bridge). fn check_echo_admissible_with_residue(&self, body: &[ReversibleStmt]) -> Result<()> { - let aggregate = echo::classify_stmts(body); + let aggregate = echo::classify_stmts_in_env(body, &self.carrier_env()); if !aggregate.admissible_with_residue() { return Err(JtvError::EchoViolation(format!( "reversible block has echo {aggregate}: it destroys information. \ @@ -712,6 +742,83 @@ mod tests { assert!(checker.check_control_stmt(&stmt).is_ok()); } + #[test] + fn test_reverse_block_rejects_float_carrier() { + // Carrier-aware Safe-only gate: `reverse { x += 5.0 }` over a FLOAT `x` + // is rejected even with no self-reference, because float reverse-add is + // lossy (IEEE-754 non-associative) — EchoNeutral, not Safe (ADR-0010). + use crate::ast::*; + let mut checker = TypeChecker::new(); + checker.env.set_var("x".to_string(), Type::Float); + let block = ReverseBlock { + body: vec![ReversibleStmt::AddAssign( + "x".to_string(), + DataExpr::Number(Number::Float(5.0)), + )], + }; + assert!(matches!( + checker.check_control_stmt(&ControlStmt::ReverseBlock(block)), + Err(JtvError::EchoViolation(_)) + )); + // Contrast: the same block shape over an INT `x` is admissible. + let mut checker2 = TypeChecker::new(); + checker2.env.set_var("x".to_string(), Type::Int); + let block2 = ReverseBlock { + body: vec![ReversibleStmt::AddAssign( + "x".to_string(), + DataExpr::Number(Number::Int(5)), + )], + }; + assert!(checker2 + .check_control_stmt(&ControlStmt::ReverseBlock(block2)) + .is_ok()); + } + + #[test] + fn test_reverse_block_rejects_inferred_float_local() { + // The soundness slice, end-to-end: a float *local* carries no annotation, + // but `x = 2.5` infers `x : Float` into the env, so the following + // `reverse { x += 1.0 }` is correctly rejected — whereas the shape-only + // classifier would have wrongly Safe-admitted it. + use crate::ast::*; + let mut checker = TypeChecker::new(); + let assign = ControlStmt::Assignment(Assignment { + target: "x".to_string(), + value: Expr::Data(DataExpr::Number(Number::Float(2.5))), + }); + assert!(checker.check_control_stmt(&assign).is_ok()); + let block = ControlStmt::ReverseBlock(ReverseBlock { + body: vec![ReversibleStmt::AddAssign( + "x".to_string(), + DataExpr::Number(Number::Float(1.0)), + )], + }); + assert!(matches!( + checker.check_control_stmt(&block), + Err(JtvError::EchoViolation(_)) + )); + } + + #[test] + fn test_reversible_token_admits_float_carrier() { + // Float routes to the token policy: `reversible { x += 1.0 } -> tok` over + // a float `x` is ADMITTED (the token retains the rounding residue), even + // though plain `reverse {}` rejects it. Only EchoBreaking is rejected. + use crate::ast::*; + let mut checker = TypeChecker::new(); + checker.env.set_var("x".to_string(), Type::Float); + let block = ReversibleBlockStmt { + body: vec![ReversibleStmt::AddAssign( + "x".to_string(), + DataExpr::Number(Number::Float(1.0)), + )], + token_binding: Some("tok".to_string()), + }; + assert!(checker + .check_control_stmt(&ControlStmt::ReversibleBlock(block)) + .is_ok()); + } + #[test] fn test_reversible_block_with_token_admits_self_reference() { // A `reversible { x += x } -> tok` block retains a residue (token) for diff --git a/docs/design-decisions/0010-number-system-stratification.adoc b/docs/design-decisions/0010-number-system-stratification.adoc index 027f1f6..18d8f37 100644 --- a/docs/design-decisions/0010-number-system-stratification.adoc +++ b/docs/design-decisions/0010-number-system-stratification.adoc @@ -17,10 +17,10 @@ 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. +*Decided (2026-06-18).* Proof, type-, value-level classifiers and the +carrier-aware typechecker gate all landed (PRs #44, #45, and the float-locals +slice). Realizes ADR-0007 D6; refines its tier vocabulary for the floating-point +case. == Context @@ -127,19 +127,25 @@ The algebra -> tier map has a single home and is mirrored, not duplicated: . *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`. +. *Runtime-value bridge — landed (PR #45).* `Value::reversal_echo`. +. *Float-locals soundness gate — landed.* `check_echo_admissible` / + `check_echo_admissible_with_residue` seed the `CarrierEnv` from the + typechecker's *inferred* type env (`self.env`, which records local types as + statements are checked), so a `reverse { z += v }` over a float *local* — which + carries no annotation — is now correctly rejected under Safe-only, while + `reversible { } -> tok` still admits it (the token retains the rounding + residue). Closes the gap this ADR previously flagged. . *`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`. +* *Carrier-awareness inside reversible `if` branches.* The gate grades the + carrier of a reversible `+=` / `-=` target directly; a plain assignment nested + inside a reversible `if` branch is still treated structurally (`Safe`) without + consulting its carrier. A rare corner — the direct reverse-add case (the common + one) is fully gated. * *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.