diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 889d983..089a39e 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,7 +5,7 @@ [metadata] project = "jtv" version = "0.0.1" -last-updated = "2026-06-18" +last-updated = "2026-06-21" status = "active" session = "2026-06-18 — Surface Echo grades (ADR-0009 D1) + repo rename julia-the-viper→jtv. SURFACE ECHO: @echo(Safe|Neutral|Breaking) annotation on functions (grammar echo_marker + parser loop, order-independent with @pure); FunctionDecl.echo_annotation — the Echo enum moved ast.rs with an echo.rs `pub use` re-export to break the ast↔echo cycle; upper-bound check typechecker.rs check_echo_annotations (inferred ⊑ annotated, against the carrier-aware call-graph-composed effect.rs resolved_effects); pretty.rs + formatter.rs emit @echo (round-trip). 133 lib tests, fmt/clippy green. RENAME: full julia-the-viper→jtv slug + Julia the Viper→JtV prose across the repo (PR #47 merged) + nextgen-languages catalogue (#87 merged, rebuilt after main dropped all submodules); etymology kept as a README/CLAUDE footnote; the GitHub Settings repo-rename is the user's remaining manual step. NEXT rung: grade in TypeAnnotation::Function (function-valued params) [LANDED 2026-06-18, prefix-marker syntax] (the @epi(...) surface LANDED 2026-06-18); value-level semantics beyond τ=int (gap-005)" @@ -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; 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-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-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" } ] @@ -91,7 +91,8 @@ sessions = [ { 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." }, { date = "2026-06-18", subject = "Surface Echo grades (ADR-0009 D1) — Bundle A (parameterised syntax + upper-bound policy). @echo(Safe|Neutral|Breaking) annotation on functions: grammar.pest echo_marker = '@echo' '(' echo_grade ')' and function_decl markers now (purity_marker|echo_marker)*; parser.rs consumes leading markers in a loop (order-independent with @pure) → FunctionDecl.echo_annotation. The Echo enum moved echo.rs→ast.rs (gains Serialize) with a `pub use crate::ast::Echo` re-export in echo.rs to break the ast↔echo cycle so FunctionDecl can hold it; all `echo::Echo` sites unchanged. UPPER-BOUND check typechecker.rs check_echo_annotations (3rd pass of check_program): inferred ⊑ annotated against the carrier-aware call-graph-composed effect.rs resolved_effects — a function may declare MORE loss than it incurs, never less (modular: caller checks against callee's declared ceiling). The reverse-gate still uses the ACTUAL inferred grade, so an annotation can't loosen reversal soundness. pretty.rs + formatter.rs emit @echo after purity (round-trip fidelity, pinned by a pretty round_trip test). 6 new tests (2 parser incl. either-order, 3 typechecker accept/reject/absent, 1 round-trip); 133 lib tests, fmt/clippy green. effect.rs header note refreshed. REMAINING: grade in TypeAnnotation::Function (function-valued params) [LANDED 2026-06-18, prefix-marker syntax]; parallel @epi(...) surface." }, { 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-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." } ] [design-artefact-locations] 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 index bc7b6fa..0224dc9 100644 --- a/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc +++ b/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc @@ -171,11 +171,13 @@ basis for the v2 `(c)` Neutral bridge and the number-system → tier map. . *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. + the carrier-distinct systems (`float`/`rational`/`complex`/`symbolic`) + are *typed* but `stated-unproven` at the value level. `type_preservation` + is mechanised for the whole *integer-represented family* `{int, hex, + binary}` (these share the `Int` carrier; generalised via `isIntRepr`, + zero axioms). The semantics layer must (a) give each remaining 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 (LANDED 2026-06-15).* Implements the Neutral tier of D5: `reverse { }` stays Safe-only; `reversible { } -> tok` admits Neutral via the retained log/token (Bennett). Lean: `JtvEcho` diff --git a/docs/design-decisions/0010-number-system-stratification.adoc b/docs/design-decisions/0010-number-system-stratification.adoc index 18d8f37..6b9e917 100644 --- a/docs/design-decisions/0010-number-system-stratification.adoc +++ b/docs/design-decisions/0010-number-system-stratification.adoc @@ -137,7 +137,11 @@ The algebra -> tier map has a single home and is mirrored, not duplicated: 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. + `type_preservation` semantics beyond `τ = int` — is now done for the whole + *integer-represented family* `{int, hex, binary}` (hex/binary share the `Int` + carrier, so the generalised `type_preservation` covers them via `isIntRepr`; + zero axioms). It remains open for `float`/`rational`/`complex`/`symbolic`, + which need their own value models. == Open / deferred @@ -150,7 +154,8 @@ The algebra -> tier map has a single home and is mirrored, not duplicated: (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`. + for the carrier-distinct systems `float`/`rational`/`complex`/`symbolic` + (the int-represented family `{int, hex, binary}` is now covered). == References diff --git a/jtv_proofs/JtvTypes.lean b/jtv_proofs/JtvTypes.lean index fcd69c0..e5bd3ba 100644 --- a/jtv_proofs/JtvTypes.lean +++ b/jtv_proofs/JtvTypes.lean @@ -420,20 +420,63 @@ theorem total_no_loops (s : ControlStmt) (h : s.respectsPurity Purity.total = tr -- SECTION 6: TYPE SOUNDNESS -- ============================================================================ -/-- Typed values: runtime values with their types -/ +/-- Typed values: runtime values with their types. + + `int`, `hex`, and `binary` share the same `Int` runtime carrier — + hex and binary are int-represented (see `JtvType`) — so an evaluated + `Int` legitimately inhabits any of the three. The remaining number + systems (`float`/`rational`/`complex`/`symbolic`) have distinct + runtime carriers that the `Int`-only evaluation model does not build, + so they are deliberately absent here (see PROOF-CAPABILITY-MATRIX + §"Scope of the semantic model"). -/ inductive TypedValue : Int → JtvType → Prop where - | int : ∀ n, TypedValue n JtvType.int + | int : ∀ n, TypedValue n JtvType.int + | hex : ∀ n, TypedValue n JtvType.hex + | binary : ∀ n, TypedValue n JtvType.binary + +/-- The integer-represented type family: exactly the `JtvType`s whose + runtime values are plain `Int`s (`int`, `hex`, `binary`). These are + the types for which `type_preservation` holds under the `Int`-only + evaluation model. -/ +def JtvType.isIntRepr : JtvType → Prop + | JtvType.int => True + | JtvType.hex => True + | JtvType.binary => True + | _ => False /-- - **Theorem (Type Preservation)**: - If Γ ⊢ e : τ and e evaluates to v, then v has type τ. + **Theorem (Type Preservation, integer-represented family)**: + If `Γ ⊢ e : τ` with `τ` an integer-represented type (`int`, `hex`, or + `binary`) and `e` evaluates to `v`, then `v` has type `τ`. Because the + three int-represented types share the `Int` carrier, the evaluated + value inhabits whichever of them the type system assigned. + + This lifts the previous `τ = int` mechanisation to the full int- + represented family; `float`/`rational`/`complex`/`symbolic` remain + `stated-unproven` at the value level pending their own evaluation + models (they do not share the `Int` carrier). -/ theorem type_preservation (Γ : TypeEnv) (e : DataExpr) (τ : JtvType) (σ : State) - (_h : DataTyping Γ e τ) : - -- For integer types, the result is an integer + (_h : DataTyping Γ e τ) (hτ : τ.isIntRepr) : + TypedValue (evalDataExpr e σ) τ := by + cases τ <;> + first + | exact TypedValue.int (evalDataExpr e σ) + | exact TypedValue.hex (evalDataExpr e σ) + | exact TypedValue.binary (evalDataExpr e σ) + | simp only [JtvType.isIntRepr] at hτ + +/-- + **Corollary**: the original `τ = int` preservation statement, recovered + from the int-represented-family theorem. Kept so the `int`-only claim + remains directly citable. +-/ +theorem type_preservation_int (Γ : TypeEnv) (e : DataExpr) (τ : JtvType) (σ : State) + (h : DataTyping Γ e τ) : τ = JtvType.int → TypedValue (evalDataExpr e σ) JtvType.int := by - intro _hτ - exact TypedValue.int (evalDataExpr e σ) + intro hτ + subst hτ + exact type_preservation Γ e JtvType.int σ h trivial /-- **Theorem (Progress for Typed Terms)**: diff --git a/verification/PROOF-CAPABILITY-MATRIX.adoc b/verification/PROOF-CAPABILITY-MATRIX.adoc index e263c64..86873fa 100644 --- a/verification/PROOF-CAPABILITY-MATRIX.adoc +++ b/verification/PROOF-CAPABILITY-MATRIX.adoc @@ -30,12 +30,15 @@ and the other document is a bug. | Claimed somewhere but neither mechanized nor written down rigorously. |=== -== Mechanization invariant (checked, 2026-06-04) +== Mechanization invariant (checked, 2026-06-04; re-verified 2026-06-21) -`grep -rc 'sorry\|admit\|axiom' jtv_proofs/*.lean` ⇒ *0* across all eight +`grep -rnwE 'sorry|admit|axiom' jtv_proofs/*.lean` ⇒ *0* across all eight libraries. The proof layer is `sorry`-free, and `lake build` is green from a clean tree. The `proof-regression.yml` workflow runs `lake build` on every -change to `jtv_proofs/**`. +change to `jtv_proofs/**`. Re-verified locally 2026-06-21 under the pinned +`leanprover/lean4:v4.12.0` toolchain (full `lake build` exit 0); the +generalised `type_preservation` / `type_preservation_int` each +`#print axioms` ⇒ *does not depend on any axioms*. NO-VACUITY invariant (added 2026-06-04): the suite also contains *no `True`-typed "believeme" theorems*. A previous pass had eight theorems whose @@ -53,12 +56,17 @@ stale* — `data_terminates` is a complete structural induction. The denotational/operational model (`evalDataExpr`) is over **`Int`** only. The seven number systems are present in `JtvTypes` as the `JtvType` enum plus typing -rules (`addRational` / `addComplex` / `addSymbolic` / …), but their *evaluation* -is not modelled, and `type_preservation` is mechanised **only for `τ = int`**. -So: addition-only Data totality/determinism/algebra and the Echo/reversibility -layer are proved over the integer model; rational/float/complex/hex/binary/ -symbolic semantics are `stated-unproven` at the value level. (This is orthogonal -to v2 — Echo is representation-agnostic.) +rules (`addRational` / `addComplex` / `addSymbolic` / …), but the carrier-distinct +systems' *evaluation* is not modelled. `type_preservation` is mechanised for the +whole **integer-represented family `{int, hex, binary}`** — these three share the +`Int` runtime carrier (hex/binary *are* int-represented), so the generalised +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.) == Believeme remediation (2026-06-04) @@ -101,6 +109,7 @@ to v2 — Echo is representation-agnostic.) | `dataExpr_determinism` | JtvTheorems | `verified` | Data evaluation is a function. | `data_terminates` | JtvOperational | `verified` | Data reduction reaches a literal. | `data_is_pure` | JtvOperational | `verified` | Data steps preserve state (Harvard invariant). +| `type_preservation` | JtvTypes | `verified` | Evaluated value inhabits its type, for the integer-represented family `{int, hex, binary}` (guarded by `isIntRepr`; zero axioms). `type_preservation_int` recovers `τ = int`. | `no_control_to_data_flow` | JtvSecurity | `verified` | Control cannot flow into Data. | `string_not_executable` | JtvSecurity | `verified` | Data is inert — evaluation yields an `Int` value, never a `ControlStmt` (injection impossibility, with `no_control_to_data_flow`). | `strong_normalization` | JtvExtended | `verified` | Data fragment strongly normalizing.