diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index ae62e25..753d3d8 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -50,7 +50,7 @@ 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 (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc). PARTIAL 2026-06-18 (ADR-0010): per-system additive-algebra → Echo-tier CLASSIFICATION landed at proof/type/value level (JtvEcho SECTION 6, echo.rs carrier_echo, number.rs Value::reversal_echo). PARTIAL 2026-06-21: type_preservation lifted past τ=int to the whole integer-represented family {int,hex,binary} (these share the Int carrier; generalised via JtvType.isIntRepr; type_preservation_int recovers τ=int; #print axioms ⇒ no axioms). Remaining open half: value-level semantics for the carrier-DISTINCT systems float/rational/complex/symbolic", severity = "medium", status = "known", follow-up = "value-level semantics for float/rational/complex/symbolic (need their own value carriers; int/hex/binary done 2026-06-21)" }, + { id = "gap-005", description = "Semantic model is Int-only: the 7 number systems are typed but stated-unproven at the value level (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc). PARTIAL 2026-06-18 (ADR-0010): per-system additive-algebra → Echo-tier CLASSIFICATION landed at proof/type/value level (JtvEcho SECTION 6, echo.rs carrier_echo, number.rs Value::reversal_echo). PARTIAL 2026-06-21: type_preservation lifted past τ=int to the whole integer-represented family {int,hex,binary} (these share the Int carrier; generalised via JtvType.isIntRepr; type_preservation_int recovers τ=int; #print axioms ⇒ no axioms). PARTIAL 2026-06-21b: float+complex are f64-based → approxGroup non-associativity WITNESSED in Rust (number.rs mod approx_group_witness) — NOT 0-axiom Lean-provable (opaque @[extern] Float; native_decide would add Lean.ofReduceBool). rational (exact abelian group) + symbolic (assoc/non-comm/non-group) Lean value models DESIGNED in docs/proofs/number-system-value-models.adoc (tracking issue filed). Remaining: land the two designed Lean models", severity = "medium", status = "known", follow-up = "land rational + symbolic 0-axiom Lean value models (designed in docs/proofs/number-system-value-models.adoc); float/complex are honestly Rust-witnessed (f64 opaque in Lean)" }, { 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" } ] @@ -93,7 +93,8 @@ sessions = [ { date = "2026-06-18", subject = "@epi(...) epistemic-grade surface (ADR-0009 D2) — mirror of the @echo surface. @epi(Opaque|Partial|Transparent) annotation on functions: grammar.pest epi_marker; parser.rs marker loop also consumes epi_marker → FunctionDecl.epi_annotation (order-independent with @pure/@echo). Epistemic enum moved epistemic.rs→ast.rs (gains Serialize) with `pub use crate::ast::Epistemic` re-export, same cycle-break as Echo. typechecker.rs check_echo_annotations renamed check_effect_annotations: now checks BOTH axes (inferred.echo ⊑ @echo, inferred.epi ⊑ @epi) against resolved_effects (FunctionEffect carries .echo + .epi). pretty.rs + formatter.rs emit @epi after @echo. 5 new tests (parser @epi + echo&epi-together, typechecker epi accept/reject, round-trip); 138 lib tests, fmt/clippy green. Completes the ADR-0009 D1+D2 function-DECLARATION effect surface. REMAINING on this axis: carry the (echo,epi) row in TypeAnnotation::Function (function-VALUED params) — has a function-type grade-syntax + variance design choice to settle." }, { date = "2026-06-18", subject = "Function-TYPE grade carrying (ADR-0009 D1/D3) — completes the ADR-0009 effect surface. A function type Fn(...) -> T may now carry the (echo,epi) row with PREFIX markers (user choice): @echo(Neutral) @epi(Partial) Fn(Int) -> Int. ast.rs: new EffectGrade { echo: Option, epi: Option } (Default); TypeAnnotation::Function gains a trailing EffectGrade; typechecker Type::Function likewise. grammar.pest function_type now (echo_marker|epi_marker)* ~ 'Fn' ...; parser splits the leading markers from the param/return type_annotations. annotation_to_type carries the grade into Type::Function; Display + pretty.rs + formatter.rs emit the prefix markers (round-trip). coercible_to gains a function-type case: COVARIANT in the grade (grade_leq — a function that loses/reveals LESS is usable where MORE is allowed; None target = unconstrained; None source can't satisfy a Some ceiling; params/return invariant for now). 4 tests (parse graded + ungraded; round-trip; covariance accept/reject/unconstrained); 142 lib tests, fmt/clippy green. HONEST SCOPE: representational/forward-infrastructure — JtV has no first-class function VALUES (no lambdas/indirect calls) yet, so the value-against-type coercion is correct but LATENT until function values land. ADR-0009 D1+D2+D3 declaration+type effect surface now COMPLETE." }, { date = "2026-06-21", subject = "type_preservation lifted past τ=int to the integer-represented family {int,hex,binary} (gap-005 partial). LOCAL LEAN TOOLCHAIN UNBLOCKED: elan 4.2.2 was present but had no toolchain, and `release.lean-lang.org` is off the egress allowlist (its 'Host not in allowlist' page is the stray 'H' that broke elan's release-metadata parse). Bypassed by fetching the v4.12.0 linux tarball straight from GitHub releases (github.com + the asset host ARE allowlisted) and unpacking it into ~/.elan/toolchains/leanprover--lean4---v4.12.0 — elan then recognises the pinned toolchain; full `lake build` exit 0 (suite is mathlib-free, zero packages, no network). PROOF (JtvTypes.lean SECTION 6): inductive TypedValue gains hex + binary constructors (all three number systems share the Int runtime carrier — hex/binary ARE int-represented); new predicate JtvType.isIntRepr {int,hex,binary}↦True else False; type_preservation generalised from `τ=int → …` to `(hτ : τ.isIntRepr) → TypedValue (evalDataExpr e σ) τ`, proved `cases τ <;> first | exact TypedValue.{int,hex,binary} | simp only [JtvType.isIntRepr] at hτ`; type_preservation_int corollary recovers the original τ=int statement (via subst + trivial). `#print axioms` ⇒ BOTH new theorems depend on NO axioms. INVARIANTS held: full lake build exit 0; 0 sorry/admit/axiom (word-boundary grep); 0 True-typed theorems. DOCS synced: PROOF-CAPABILITY-MATRIX (scope-of-model rewrite + new key-theorems row + 'checked 2026-06-04; re-verified 2026-06-21' note), ADR-0007 consequence #1, ADR-0010 §gap-005 + §Open. float/rational/complex/symbolic REMAIN stated-unproven (distinct carriers, each needs its own value model). NOTE for next session: the local toolchain at ~/.elan is ephemeral (container reclaimed on inactivity) — re-run the GitHub-releases bypass to restore `lake build`; CI (proof-regression.yml) is the durable verifier." }, - { date = "2026-06-21", subject = "interpreter_correctness (PROOF-2 / gap-001) rung — denotational correspondence harness. Ties the Lean denotational model evalDataExpr ↔ the Rust interpreter eval_data_expr over the integer fragment the model covers (lit|var|add|neg over σ:String→Int). crates/jtv-core/src/interpreter.rs gains `mod denotational_correspondence`: (1) `denot` re-encodes the four Lean rules in i128; (2) `interpreter_matches_denotational_model_on_int_fragment` EXHAUSTIVELY enumerates every height-≤2 integer-fragment expression (5 lits × 2 vars = 7 leaves → 4039 exprs) across 3 states ≈ 12k cases, asserting interpreter == denot on all; (3) `overflow_is_the_correspondence_boundary` pins that Value::Int is i64 with checked_add/checked_neg → ERRORS at the i64 edge, never wraps (so correspondence boundary is exactly i64 range, Lean ℤ being unbounded); (4) `shared_golden_corpus_matches_lean` mirrors 7 concrete (expr,σ,value) points that are ALSO pinned by `rfl` in JtvCore.lean (cross-side anchor; the 5 new Lean `example`s use State.empty[x↦v] updates, all close by rfl). HONEST BOUND: integer fragment only (strings/float/rational/complex/calls/lists/tuples out of model); within i64 range; exhaustive-up-to-depth, NOT a Lean-mechanised refinement of the Rust evaluator (the deeper PROOF-2 rung). VERIFIED locally: cargo test (145 lib incl. 3 new + full workspace green), cargo fmt --check + clippy -D warnings clean, full lake build exit 0, 0 sorry/admit/axiom, 0 True-typed theorems. DOCS: PROOF-CAPABILITY-MATRIX (interpreter_correctness row JtvCore+interpreter.rs/partial + new 'Interpreter ↔ denotational-model correspondence' section + outstanding-work bullet), gap-001 partial. NEXT on PROOF-2: mechanised refinement (model the Rust evaluator in Lean) and/or extend the harness past the integer fragment." } + { date = "2026-06-21", subject = "interpreter_correctness (PROOF-2 / gap-001) rung — denotational correspondence harness. Ties the Lean denotational model evalDataExpr ↔ the Rust interpreter eval_data_expr over the integer fragment the model covers (lit|var|add|neg over σ:String→Int). crates/jtv-core/src/interpreter.rs gains `mod denotational_correspondence`: (1) `denot` re-encodes the four Lean rules in i128; (2) `interpreter_matches_denotational_model_on_int_fragment` EXHAUSTIVELY enumerates every height-≤2 integer-fragment expression (5 lits × 2 vars = 7 leaves → 4039 exprs) across 3 states ≈ 12k cases, asserting interpreter == denot on all; (3) `overflow_is_the_correspondence_boundary` pins that Value::Int is i64 with checked_add/checked_neg → ERRORS at the i64 edge, never wraps (so correspondence boundary is exactly i64 range, Lean ℤ being unbounded); (4) `shared_golden_corpus_matches_lean` mirrors 7 concrete (expr,σ,value) points that are ALSO pinned by `rfl` in JtvCore.lean (cross-side anchor; the 5 new Lean `example`s use State.empty[x↦v] updates, all close by rfl). HONEST BOUND: integer fragment only (strings/float/rational/complex/calls/lists/tuples out of model); within i64 range; exhaustive-up-to-depth, NOT a Lean-mechanised refinement of the Rust evaluator (the deeper PROOF-2 rung). VERIFIED locally: cargo test (145 lib incl. 3 new + full workspace green), cargo fmt --check + clippy -D warnings clean, full lake build exit 0, 0 sorry/admit/axiom, 0 True-typed theorems. DOCS: PROOF-CAPABILITY-MATRIX (interpreter_correctness row JtvCore+interpreter.rs/partial + new 'Interpreter ↔ denotational-model correspondence' section + outstanding-work bullet), gap-001 partial. NEXT on PROOF-2: mechanised refinement (model the Rust evaluator in Lean) and/or extend the harness past the integer fragment." }, + { date = "2026-06-21", subject = "Number-system value-model rung + session close-out triage. gap-005 advanced for 2 of the 4 carrier-distinct systems, the other 2 designed+issued: (a) FLOAT+COMPLEX approxGroup WITNESS landed (number.rs mod approx_group_witness, 4 tests): non-associativity of Value::Float / Value::Complex add via the public Value::add ((0.1+0.2)+0.3 ≠ 0.1+(0.2+0.3)), commutativity holds. Honest finding: f64 is opaque to Lean's kernel (@[extern] Float; native_decide=Lean.ofReduceBool axiom, forbidden) → these are Rust-witnessed not Lean-proved. (b) RATIONAL (exact abelian group: Q struct + cross-mult equiv + group laws up to equiv) and SYMBOLIC (string-concat: assoc + non-comm counterexample + non-group) Lean value models DESIGNED in new docs/proofs/number-system-value-models.adoc; tracking issue filed. cargo test/fmt/clippy green. Docs: PROOF-CAPABILITY-MATRIX scope-of-model section links the sketch; gap-005 updated. NOTE: parallel-subagent route was attempted but worktree isolation is unavailable in this env (agent cwd not a git repo) — did it directly instead. Close-out triage (branches/wiki/docs audit) recorded in session response." } ] [design-artefact-locations] diff --git a/crates/jtv-core/src/number.rs b/crates/jtv-core/src/number.rs index 698f859..cb344d4 100644 --- a/crates/jtv-core/src/number.rs +++ b/crates/jtv-core/src/number.rs @@ -414,3 +414,63 @@ mod tests { assert_eq!(Value::Unit.reversal_echo(), Echo::Safe); } } + +// =========================================================================== +// approxGroup witness (ADR-0010 / gap-005, value-level) +// +// Float and Complex are IEEE-754 f64-based (`Value::Float(f64)`, +// `Value::Complex(Complex)`), so their `add` is NON-associative: they sit +// at the `approxGroup -> Neutral` tier, never the exact `abelianGroup -> Safe` +// tier (unlike Int/Hex/Binary/Rational). This is the value-level fact behind +// `reversal_echo` returning `Neutral` for float. +// +// It is witnessed HERE (in Rust, against native f64) rather than in Lean +// because Lean's `Float` is an opaque `@[extern]` primitive: f64 arithmetic +// does not reduce in the kernel, and the only way to evaluate it +// (`native_decide`) injects the `Lean.ofReduceBool` axiom, which the jtv_proofs +// 0-axiom invariant forbids. So the faithful check is this differential +// witness. (Rational and Symbolic, being exact, DO admit 0-axiom Lean value +// models — see docs/proofs/number-system-value-models.adoc + the tracking +// issue.) +// =========================================================================== +#[cfg(test)] +mod approx_group_witness { + use super::*; + + #[test] + fn float_add_is_non_associative() { + let (a, b, c) = (Value::Float(0.1), Value::Float(0.2), Value::Float(0.3)); + let left = a.add(&b).unwrap().add(&c).unwrap(); // (0.1 + 0.2) + 0.3 + let right = a.add(&b.add(&c).unwrap()).unwrap(); // 0.1 + (0.2 + 0.3) + assert_ne!( + left, right, + "float add must be non-associative (approxGroup, not an exact group)" + ); + } + + #[test] + fn float_add_is_commutative() { + let (a, b) = (Value::Float(0.1), Value::Float(0.2)); + assert_eq!(a.add(&b).unwrap(), b.add(&a).unwrap()); + } + + #[test] + fn complex_add_inherits_f64_non_associativity() { + let a = Value::Complex(Complex64::new(0.1, 1.0)); + let b = Value::Complex(Complex64::new(0.2, 1.0)); + let c = Value::Complex(Complex64::new(0.3, 1.0)); + let left = a.add(&b).unwrap().add(&c).unwrap(); + let right = a.add(&b.add(&c).unwrap()).unwrap(); + assert_ne!( + left, right, + "complex add is componentwise f64 -> non-associative (approxGroup)" + ); + } + + #[test] + fn complex_add_is_commutative() { + let a = Value::Complex(Complex64::new(0.1, 2.0)); + let b = Value::Complex(Complex64::new(0.2, 3.0)); + assert_eq!(a.add(&b).unwrap(), b.add(&a).unwrap()); + } +} diff --git a/docs/proofs/number-system-value-models.adoc b/docs/proofs/number-system-value-models.adoc new file mode 100644 index 0000000..374faa9 --- /dev/null +++ b/docs/proofs/number-system-value-models.adoc @@ -0,0 +1,90 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += Number-system value models (gap-005) — status + design sketch +:toc: +:revdate: 2026-06-21 + +Value-level semantics for JtV's seven number systems. The Lean denotational +model (`evalDataExpr`) is `Int`-only; this document tracks lifting *value-level* +algebraic facts to the other systems, faithful to the Rust interpreter +(`crates/jtv-core/src/number.rs`). It elaborates the `gap-005` row of +`verification/PROOF-CAPABILITY-MATRIX.adoc` and realises ADR-0010's +algebra → Echo-tier classification at the value level. + +== Status table (faithful to `number.rs`) + +[cols="1,2,2,2,1",options="header"] +|=== +| System | Rust rep | `add` | Algebra | Value-level status + +| `int` / `hex` / `binary` | `i64` | `checked_add` | exact abelian group | *Verified* — share the `Int` carrier; `type_preservation` (`JtvTypes.lean`, 0 axioms) +| `rational` | `Ratio` | exact fraction `+` | exact abelian group | *Designed* (Lean) — see §Rational +| `symbolic` | `String` | `"{a} + {b}"` concat | associative, non-commutative, non-group | *Designed* (Lean) — see §Symbolic +| `float` | `f64` | raw IEEE `+` | approxGroup (non-associative) | *Witnessed* (Rust) — see §Float/Complex +| `complex` | `Complex` | componentwise `f64` | approxGroup (inherits f64) | *Witnessed* (Rust) — see §Float/Complex +|=== + +== Float / Complex — why a Rust witness, not a Lean proof + +`float` and `complex` are IEEE-754 `f64`-based, so their addition is +*non-associative*: they are `approxGroup → Neutral` (ADR-0010), never the exact +`abelianGroup → Safe` tier. + +This fact is *witnessed in Rust* (`number.rs`, `mod approx_group_witness`): +`(0.1 + 0.2) + 0.3 ≠ 0.1 + (0.2 + 0.3)` through `Value::Float`/`Value::Complex` ++ `Value::add`, with commutativity shown to hold. + +It is **not** provable as a 0-axiom Lean theorem. Lean's `Float` is an opaque +`@[extern]` primitive: f64 arithmetic does not reduce in the kernel +(`decide`/`rfl` cannot evaluate `0.1 + 0.2`), and the only evaluator +(`native_decide`) injects the `Lean.ofReduceBool` axiom — which the jtv_proofs +0-axiom invariant forbids. So the differential witness against native f64 is the +faithful check; a Lean "proof" here would be either vacuous or axiom-bearing. + +== Rational — Lean exact-group model (design sketch) + +Faithful to `Value::Rational(Ratio)` (exact, auto-reduced). Mathlib- and +Batteries-free, so build from Lean-core `Int`: + +[source,lean] +---- +structure Q where + num : Int + den : Int + den_nz : den ≠ 0 +def Q.add (a b : Q) : Q := ⟨a.num * b.den + b.num * a.den, a.den * b.den, …⟩ +def Q.neg (a : Q) : Q := ⟨-a.num, a.den, a.den_nz⟩ +def Q.zero : Q := ⟨0, 1, by decide⟩ +def Q.equiv (a b : Q) : Prop := a.num * b.den = b.num * a.den -- cross-mult +---- + +Targets (0 axioms, no `sorry`/`native_decide`): `equiv` is a setoid +(refl/symm/trans), `add` respects `equiv`, and the abelian-group laws *up to* +`equiv` — `qadd_comm`, `qadd_assoc`, `qadd_zero`, `qadd_left_neg` — via core +`Int` ring lemmas. Establishes `rational = exact abelian group → Safe`. + +Honest bound: i64 overflow not modelled (unbounded `Int`); worked up to +cross-multiplication (no reduced-form normalisation). `equiv` transitivity is +the fiddliest step (Int cancellation by nonzero denominators). + +== Symbolic — Lean free-algebra model (design sketch) + +Faithful to `Value::Symbolic(String)`: `add a b = a ++ " + " ++ b`, +`neg s = "-(" ++ s ++ ")"`. Carrier `String` (or `List Char`). + +Targets (0 axioms): `sadd_assoc` (the `" + "` separator flattens — both sides +are `a ++ " + " ++ b ++ " + " ++ c`, via append-associativity); +`sadd_not_comm` (concrete counterexample `"a + b" ≠ "b + a"` by `decide`); +a non-group witness (`sadd` strictly grows length → no inverse / no identity). +Establishes `symbolic = associative, non-commutative, non-group → Breaking` +— symbolic *retains* structure where int/rational collapse it. + +== The full ladder (where this sits) + +* *int/hex/binary* — done (`type_preservation`). +* *float/complex* — approxGroup witnessed (this is the maximal honest 0-axiom + Lean statement; the real content lives in Rust). +* *rational/symbolic* — Lean models designed above; tracked as an issue. +* The deeper rung (separate): a *multi-sorted evaluator* `evalDataExpr` that + produces these carriers, so `type_preservation` extends to them directly. + That is a model refactor, not covered here. diff --git a/verification/PROOF-CAPABILITY-MATRIX.adoc b/verification/PROOF-CAPABILITY-MATRIX.adoc index 7b86624..9457f0a 100644 --- a/verification/PROOF-CAPABILITY-MATRIX.adoc +++ b/verification/PROOF-CAPABILITY-MATRIX.adoc @@ -64,9 +64,15 @@ theorem, guarded by `JtvType.isIntRepr`, covers all three; it depends on **zero axioms**. `type_preservation_int` recovers the original `τ = int` statement as a corollary. So: addition-only Data totality/determinism/algebra, int-represented- family type preservation, and the Echo/reversibility layer are proved over the -integer model; `rational`/`float`/`complex`/`symbolic` semantics remain -`stated-unproven` at the value level (they need distinct value carriers). (This is -orthogonal to v2 — Echo is representation-agnostic.) +integer model. The carrier-distinct systems are tracked in +`docs/proofs/number-system-value-models.adoc`: `float`/`complex` are `f64`-based, +so their non-associativity (`approxGroup → Neutral`) is *witnessed in Rust* +(`number.rs`, `mod approx_group_witness`) — it is **not** 0-axiom provable in +Lean (opaque `@[extern]` `Float`; `native_decide` would add `Lean.ofReduceBool`). +`rational` (exact abelian group) and `symbolic` (associative, non-commutative, +non-group) admit real 0-axiom Lean value models — *designed* in that doc, +remaining `stated-unproven` until landed. (This is orthogonal to v2 — Echo is +representation-agnostic.) == Believeme remediation (2026-06-04)