From 034fd369d0fa3549013ddc1b2f3ac538ca50d8e5 Mon Sep 17 00:00:00 2001 From: Alexander Flom Date: Sun, 18 Oct 2026 03:54:39 -0600 Subject: [PATCH] Complete #167 release follow-ups: generation bounds, env audit, text, and coverage (#187) --- CHANGELOG.md | 11 +- CONFORMANCE.md | 2 +- SPEC.md | 158 +++++++++++------- VERIFICATION.md | 58 +++++-- crates/conformance/src/cases/cli_api.rs | 82 +++++++++ crates/conformance/src/cases/models.rs | 33 +++- .../src/cases/semantic_ir/widen.rs | 56 +++++++ crates/conformance/src/lean_literals.rs | 7 +- .../src/production/certificate/data_a.rs | 14 +- features/suites/preservation.feature | 2 +- model/ids.toml | 2 +- 11 files changed, 328 insertions(+), 97 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 644070152..0b265b77d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -56,8 +56,13 @@ versions, and the entries below say what each tag does and does not claim. state. Certificates A and B are kernel data in which a repeated type is one node, so the chain verifies (it did not fit under `max_file_bytes` as text) and the lower bound counts no type node; what a small source still makes - large is the pairs of arms of a match, which the fixture now uses. The - fixture is refused with `LLS8002` in lowering, as before. + large is the pairs of arms of a match, which the fixture now uses. With + certificate A as kernel data, a pair of arms costs about 5.7 times its text + cost (`1018` against `180` sixteenths of a byte), so the widest match that + fits the default `max_file_bytes` falls from about `420` to `240` + constructors (`SP-02`, SPEC.md §17.17; a project with a wider match raises + `max_file_bytes`). The fixture is refused with `LLS8002` in lowering, as + before. - The preservation library's statement of `LexLeanTarget.TargetSemantics.fromOrdering.eq_1` is the one the elaborator makes for the generated module under the explicit byte-literal spelling @@ -77,7 +82,7 @@ versions, and the entries below say what each tag does and does not claim. `Bytes` forms) to `(sign, mantissa, exponent)` over `nat` and `int`, rejecting out-of-width patterns and the non-finite biased exponents, and derives `round(a * b / c * 2^32)` scale ratios (ties to even) by exact - integer division; 43 theorems (39 in `Models.Recognizer`, 4 in `Models.Main`) are closed by `decide`. The change is to the + integer division; 47 theorems (43 in `Models.Recognizer`, 4 in `Models.Main`) are closed by `decide`. The change is to the `models` example and the register only: no compiler source moves. - Widening conversions (#114, SPEC.md §17.12 *Widening conversions*, `SM-32`, diff --git a/CONFORMANCE.md b/CONFORMANCE.md index 05982c757..eaab0ba9c 100644 --- a/CONFORMANCE.md +++ b/CONFORMANCE.md @@ -353,7 +353,7 @@ the error registry does not sanction (R5, `ERRORS.md`). | ID | Level | Statement | | --- | --- | --- | | `SP-01` | `build` | Every production root of the committed examples lowers to a valid realization program in first-binding order, byte-identical across two lowerings, with an origin for every function and document type and exactly the root's eligibility closure; the lowering and certificate sources match no construct by default; a planted closure disagreement fails with LLI9001 and a planted default arm is refused. | -| `SP-02` | `build` | Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it, and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; and in every case by generating each certificate under the limit, which stops it at the limit; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. | +| `SP-02` | `build` | Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it (and a mixed shape that fits at its full scale of 256 is checked to fit and not edge-checked), and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; during certificate B's derivation at 12 bytes a kernel node; and for every certificate by weighing the finished module in the authoring notation it is recorded in against max_file_bytes before any file is staged; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. | | `SP-03` | `build` | On seeded inputs to every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning, the calculus interpreter's outcome on the lowered program equals the certificate's observation evaluated by Lean, and a planted disagreement is detected. | | `SP-04` | `build` | Every declaration of the preservation library is a row of a native module that pins its axioms exactly and depends on exactly them under the pinned Lean, the statement vocabulary SPEC.md quotes equals what the pinned Lean prints of the generated library, the shipped calculus modules are byte-equal to the compiler project's golden modules, and a library module or certificate with a forbidden token, a disallowed option, or a foreign import is refused. | | `SP-05` | `build` | Verification checks certificate A for every production root after named-root extraction and publishes each certificate, its audit output and process records, and a preservation.json valid against its schema whose digest the attestation binds; the lowered program and each target's crate the certificates are about are published and bound by that record, which also states the function each crate is invoked through and agrees with certificate E and the crate; a certificate the pinned Lean rejects fails with LLV7013 and a drifted preservation environment with LLV7014, before publication; and a pinned Lean that gives up on a certificate by heartbeats or recursion depth is reported as that rejection unless the module is at least a quarter of max_file_bytes, in which case, as when it is killed or out of memory, it is an exhausted resource, LLS8002. | diff --git a/SPEC.md b/SPEC.md index 031dba153..b9df5658b 100644 --- a/SPEC.md +++ b/SPEC.md @@ -2774,7 +2774,10 @@ either backend runs; they do not defer to what Lean would accept. `Type`, `UInt8`..`UInt64`, `Unit`, `and_congr`, `and_true`, `beq_iff_eq`, `congr`, `decide`, `decide_eq_false_iff_not`, `decide_eq_true_eq`, `false`, `id`, `reduceIte`, `rfl`, `true`, `true_and`), and to every imported declaration through - the project's module prefix, all without qualification. In a + the project's module prefix, all without qualification (a byte literal + instead qualifies `_root_.ByteArray.mk` and `_root_.UInt8.ofNat (nat_lit n)` + from the root and binds literal-local `let __byteN` variables whose `__` + prefix no source binder can spell). In a `lexlean/semantic-module/2` module no binder (a type parameter, a value parameter, or a pattern, `let`, quantifier, lambda, or proof binder) is spelled like a declaration of the module, one of those built-in names, or @@ -3807,15 +3810,19 @@ counter by counter by Lean's kernel. result `Nat`. Any other operand type, result type, or argument count is rejected in linking (`LLT4001`) before either backend runs. 2. **Elaboration.** A widening conversion is a total, exact conversion of its - operand's value. Linking elaborates each application into an ordinary - language-1.2 term before Lean rendering, production eligibility, or - production lowering runs: the operand is bound once to a generated local - `__widen` (`n` counted in evaluation order within each declaration), - each bit $k$ of the width is tested with `bit_and` and `equal` against the - fixed-width mask $2^k$, and the bit weights are summed in a balanced tree - over `Int` (`subtract` and `negate`, with the sign bit of a signed width - weighted by $-2^{w-1}$ and bit 63 of `UInt64` expressed as $2^{62} + 2^{62}$ - so every literal lies within 64-bit signed range) or over `Nat` (`add`). + operand's value in Lean (`Int` and `Nat` are unbounded). Linking elaborates + each application into an ordinary language-1.2 term before Lean rendering, + production eligibility, or production lowering runs: the operand is bound + once to a generated local `__widen` (`n` counted in evaluation order + within each declaration), each bit $k$ of the width is tested with `bit_and` + and `equal` against the fixed-width mask $2^k$, and the bit weights are + summed in a balanced tree over `Int` (`subtract` and `negate`, with the sign + bit of a signed width weighted by $-2^{w-1}$ and bit 63 of `UInt64` expressed + as $2^{62} + 2^{62}$ so every literal lies within 64-bit signed range; in the + production calculus `Int` is 64-bit signed, so `to_int` on a `UInt64` at or + above $2^{63}$ overflows the calculus's `Int64` range at the sum of those two + $2^{62}$ terms, while `to_nat` on `UInt64` is total in both, `conformance_sm_32`) + or over `Nat` (`add`). Generated Lean, production eligibility, production lowering, and the preservation certificates read the elaborated declaration, so a root that indexes a `Bytes` value and widens the resulting `UInt8` lowers to bit @@ -4920,8 +4927,12 @@ large for different reasons, and the sum of what they have in common is no bound on the largest (a match on 200 constructors returned with a string of 330 000 characters has a certificate A of 1.1 MB, from the match, and a certificate B of 1.0 MB, from the string; no certificate is the sum). Each -cost of certificates B and E is half of the greatest for which its bound stays -below its certificate, found by linear programming over every root of the three example corpora and of +cost of certificate B is a quarter of the text-era cost (half of the greatest +for which the text bound stayed below the text certificate, halved again +because the authoring notation certificate B is recorded in and weighed by takes +about a quarter of the bytes of its Lean text), and each cost of certificate E is +half of the greatest for which its bound stays below its certificate, found by +linear programming over every root of the three example corpora and of families of programs that grow one dimension at a time (let chains, call chains, many parameters, enumerations of many constructors, matches nested under one another, wide structures, record copies, long literals, a generic @@ -4932,9 +4943,11 @@ random shapes, the wide matches, and the four example corpora has a certificate A smaller than its bound, with five percent to spare. `conformance_sp_02` requires that each bound is never above its certificate (for B and E, the smaller of the targets') on any of them, and on random combinations of five dimensions, none of which the costs -were fitted to, and requires that the largest scaling of each of nine mixed -shapes whose certificates are all under the default limit, a program at the -edge of what fits, is not refused. The early refusal refuses, and only +were fitted to, and requires that for each of nine mixed shapes the largest +scaling at most 256 whose certificates are all under the default limit is not +refused (when a shape fits only below its full scale of 256, that largest +scaling sits within forty percent of the limit; a shape that fits at its full +scale of 256 is checked to fit and not edge-checked). The early refusal refuses, and only refuses early: a root whose certificates fit under `max_file_bytes` is not refused by it (a match on 240 constructors, whose certificate A is 3.9 MB in the notation it is recorded in; a string literal of 450 000 characters, whose certificate B is 1.4 MB; a match @@ -4955,23 +4968,41 @@ floor, not a measured least), would take more than `max_file_bytes` of certificate B: the crate is built after this, so a program that large is never rendered. -The guarantee is the byte budget. Every certificate is generated under -`max_file_bytes`: the proof of each term of certificate A, each match arm, -the encoders, each function, and the boundary, the terms and derivations of -certificate B, and certificate E are counted as they are built, and generation stops with -`LLS8002` as soon as a part is beyond the limit, so that no program makes the -generator produce, or the stage after it hold, much more than the limit (one -part past it: a function's derivation, or a term's proof). Certificates are -generated, for every root, right after lowering and before the toolchain is -touched, so every refusal is `LLS8002` before any Lean work. A derivation is -built, written, and dropped without recursion in the number of a match's arms, -so a limit that allows thousands of arms cannot overflow the stack -(`conformance_sp_08` derives 9000 on a 2 MiB stack). Certificates A and B are -kernel data in which a repeated subterm is one node, so the types of a program -cost its certificates nothing beyond their first occurrence, and the chain -above verifies 16 deep (its 2^16 type nodes are charged to `max_ir_nodes`); -what the generation stops and the early bound does not see is a part of one -certificate past the limit, a function's derivation or a term's proof. +The guarantee is the byte budget. Every certificate is weighed against +`max_file_bytes` before any file is staged or the toolchain is touched, so no +oversized certificate is ever accepted and every refusal is `LLS8002` before +any Lean work. Certificates A, B, and E are built as native core modules +(`lexlean/core-module/2`, kernel-term DAGs in which a repeated subterm is one +node, so the types of a program cost its certificates nothing beyond their +first occurrence, and the chain above verifies 16 deep while its 2^16 type nodes +are charged to `max_ir_nodes`) and weighed in the authoring notation they are +recorded in (`record_source`): +- **Before generation**, lowering's lower bound (`COSTS_A`, `COSTS_B`, + `COSTS_E`) and certificate B's field-read floor (`8` bytes per pattern entry) + refuse any root whose Linear-Program lower bound or field-read floor already + exceeds `max_file_bytes`. +- **During generation**, certificate B's aligner counts each new kernel node of + a function's derivation at `12` bytes (`NODE_BYTES`, the shortest row of the + authoring notation) and stops with `LLS8002` at the end of a step once that + floor passes `max_file_bytes`. Because a record-read node takes about `35` + bytes in the recorded notation (and the corpora's nodes `14` to `18`), a + derivation can hold about three times `max_file_bytes` of recorded notation + before that per-node floor stops it (`conformance_sp_02` checks that a quarter + of the recorded size of `record copy 100` stops B during derivation). + Certificates A and E have no per-node counter during construction; each builds + its `CoreModule` in memory for a root that passed lowering's lower bound. +- **When a certificate is finished**, its recorded notation (`record_source` for + A and B, `lean_text_legacy` and `record_source` for E) is weighed once against + `max_file_bytes` (`certificate.rs`, `data_b.rs`) and refused with `LLS8002` + if it exceeds the limit (fixture `certificate-generation-limit`: the sum of + 500 fields of a record passes lowering's floor and B's 12-byte-per-node + derivation floor and is refused at its exact notation weight of `8 513 069` + bytes against `4 194 304`, holding about `2.03` times the limit in memory + before refusal). + +A derivation of certificate B is built without recursion in the number of a +match's arms, so a limit that allows thousands of arms cannot overflow the +stack (`conformance_sp_08` derives 9000 on a 2 MiB stack). The roots of a project are bounded together, in two places. A closure member of the eligibility report (§17.13, a build artifact) records its shortest call @@ -4999,31 +5030,38 @@ functions from one root is accepted and one of 2360 refused, and a chain of 243 roots is accepted (a report of 66 508 069 bytes, 4.5 seconds and 75 MB to check, 14 seconds and 675 MB to build) and one of 244 refused in the same time and memory. The certificates of the roots repeat their closures too, so their -texts grow with the square of the number of chained roots (1.1 KB of -certificate A and 2.4 KB of each certificate B for every function of a closure; -243 roots would take about 110 MB), each of them under `max_file_bytes`. The +recorded modules grow with the square of the number of chained roots (about 1.9 KB of +certificate A and 0.6 KB of each certificate B in the recorded notation for every +function of a closure, where the text certificates took 1.1 KB and 2.4 KB; +243 roots would take about 75 MB), each of them under `max_file_bytes`. The lowered programs, the Rust crates, and the certificates of all the roots therefore also count toward `max_total_source_bytes`, as each root generates them, and a project that passes the limit is `LLS8002` before the toolchain is touched (fixture `certificates-total-limit`, a chain of 40 roots under a limit of 2 000 000; a chain of 170 roots under the default). -Lean's own budgets are the fourth bound, and they are not the compiler's. The -pinned Lean checks certificate B at a time that grows faster than the fourth -power of the arms of the widest match it derives (the certificate B of a match -on 130 constructors takes 17 seconds, on 200 constructors 42, on 300 -constructors 200, and one on 440 constructors does not finish in 15 minutes), -and a certificate A of 23 bytes for each pair of arms takes 59 seconds at 200 -constructors. Its default budgets are exhausted well before: 100 constructors -are checked within `maxHeartbeats` 200 000 and `synthInstance.maxHeartbeats` -20 000, 160 exhaust the second, 200 the first, a function returning a -large literal (a program carrying its parameters as data) costs `isDefEq` as -much again, and exhausting either in the middle of a proof ends as -`Application type mismatch`, an error that blames a valid certificate. Every -certificate therefore sets both budgets to 0, and certificate B declares its -program and crate terms `noncomputable`, since they are the statement's data, -unfolded by the proofs and run by nothing, and compiling a large crate term -alone exhausted the code generator's budget. The limit that remains is the +Lean's own budgets are the fourth bound, and they are not the compiler's. On +the text-era certificates, the pinned Lean checked certificate B at a time that +grew faster than the fourth power of the arms of the widest match it derived +(the text certificate B of a match on 130 constructors took 17 seconds, on 200 +constructors 42, on 300 constructors 200, and one on 440 constructors did not +finish in 15 minutes), and a text certificate A of 23 bytes for each pair of +arms took 59 seconds at 200 constructors (as kernel data, a pair of arms is at +least `63.6` bytes of certificate A, so the kernel checks fewer constructors per +megabyte). Lean's default budgets are exhausted well before on the staged +decoder and any elaborator work: 100 constructors were checked within +`maxHeartbeats` 200 000 and `synthInstance.maxHeartbeats` 20 000, 160 exhausted +the second, 200 the first, a function returning a large literal (a program +carrying its parameters as data) cost `isDefEq` as much again, and exhausting +either in the middle of a proof ended as `Application type mismatch`, an error +that blamed a valid certificate. Every certificate therefore sets both budgets +to 0, and in certificate B's native core module the `program`, `krate`, and +`flags` definition rows have `compiled: false` ( as `__prog` and the encoders do +in certificate A, where only `denote` and what it calls set `compiled: true`), +so the native decoder adds them to the kernel environment without invoking the +code generator on them (they are the statement's data, unfolded by the kernel +and run by nothing, and compiling a large crate term alone exhausted the code +generator's budget). The limit that remains is the wall clock: `child_timeout_ms` (300 seconds by default) bounds every Lean process, and its exhaustion is `LLS8002`. Each child process (`lake`, which starts `lean`, and the PDF provider: every child of `verify` is started the @@ -5569,9 +5607,12 @@ The well-typedness theorems of a recursive group are the group's recursor (`T.rec` for each of its document types and `T.rec_j` of the block's first type for the `j`-th container the kernel nests, in the order it nests them), an induction hypothesis standing where the text recursed. The one core -backend renders the module to the Lean verification compiles, with `import` -lines and no `module` header while the staged certificates import one -another as such (a `module` cannot import them), and the verify record holds the module in the +backend renders the module (`lean_text_legacy`) to the Lean verification +compiles, scoped in `namespace ` with `import` lines and no `module` +header so each certificate's inline core-v2 decoder stays inside its own +namespace and because certificates A, B, and E and the staged audit module +import one another outside Lean's `module` system (Lean refuses a `module` that +imports a non-`module` file), and the verify record holds the module in the authoring notation (§17.21.8), at the module's path with the extension `.lex.tex`, which reads back to the data byte for byte; `preservation.json` binds those bytes. A certificate held as data is audited row by row and @@ -5661,9 +5702,10 @@ literal, an added axiom, and a row whose policy lies, each refused. is an auxiliary module of typed commands (`#print axioms`, `#print "marker"`, `#print name`, `#check @name`) that the Lean backend renders. It is rendered without the `module` header, because Lean refuses a `module` that imports a -file that is not one and the certificates are rendered outside the module -system (the user modules they import are not exposed to a `module` -certificate). No other string literal under `crates/lexlean/src/production/`, +file that is not one and the certificates it imports are rendered outside the +module system via `lean_text_legacy` (scoped in `namespace ` without a +`module` header so each certificate's inline decoder stays local and can be +imported by certificate E and the audit module). No other string literal under `crates/lexlean/src/production/`, and none in the probe and audit module part of `backend/lean.rs` beyond the renderer of those commands and the quote of a name, is Lean syntax: a lexer-level scan of the sources, which drops test code and reads every string @@ -9734,7 +9776,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `GC-10` | `gnaf-certification` | The certification model, certificate fixtures, certificate module, and schemas are generated, deterministic, and content-addressed: they equal their generators, the compiler project reaches them from its entrypoint, certificate identities are recomputed from content, and a planted change to a premise, a bound, or a route changes the verdict or the identity. | §17.18 | | `GC-11` | `gnaf-certification` | The certification library is LexLean source: every module of its registry is one language-1.2 native core module of the library's own project, which holds no file of Lean source, no Lean file anywhere in the release tree declares the library's namespace or lies under its module root, and the registry lists only the modules; the declarations and their exact axiom policies are read from the native data, a module that imports anything but `Init`, an earlier module, the preservation core, or the generated and calculus modules it is stated against, or that does not pin its axioms exactly, is refused, and the Lean the compiler generates from the sources is, byte for byte, the Lean the certification library's kernel check compiles, so that neither a stale nor an edited generated module can stand in for the source and a planted drift of the source is visible in what is generated. The one Lean text a generated library module carries beside its data is the decoder of core module 2, which loads native modules. | §17.18 | | `SP-01` | `preservation` | Every production root of the committed examples lowers to a valid realization program in first-binding order, byte-identical across two lowerings, with an origin for every function and document type and exactly the root's eligibility closure; the lowering and certificate sources match no construct by default; a planted closure disagreement fails with LLI9001 and a planted default arm is refused. | §17.17 | -| `SP-02` | `preservation` | Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it, and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; and in every case by generating each certificate under the limit, which stops it at the limit; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. | §17.17 | +| `SP-02` | `preservation` | Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it (and a mixed shape that fits at its full scale of 256 is checked to fit and not edge-checked), and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; during certificate B's derivation at 12 bytes a kernel node; and for every certificate by weighing the finished module in the authoring notation it is recorded in against max_file_bytes before any file is staged; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. | §17.17 | | `SP-03` | `preservation` | On seeded inputs to every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning, the calculus interpreter's outcome on the lowered program equals the certificate's observation evaluated by Lean, and a planted disagreement is detected. | §17.17 | | `SP-04` | `preservation` | Every declaration of the preservation library is a row of a native module that pins its axioms exactly and depends on exactly them under the pinned Lean, the statement vocabulary SPEC.md quotes equals what the pinned Lean prints of the generated library, the shipped calculus modules are byte-equal to the compiler project's golden modules, and a library module or certificate with a forbidden token, a disallowed option, or a foreign import is refused. | §17.17 | | `SP-05` | `preservation` | Verification checks certificate A for every production root after named-root extraction and publishes each certificate, its audit output and process records, and a preservation.json valid against its schema whose digest the attestation binds; the lowered program and each target's crate the certificates are about are published and bound by that record, which also states the function each crate is invoked through and agrees with certificate E and the crate; a certificate the pinned Lean rejects fails with LLV7013 and a drifted preservation environment with LLV7014, before publication; and a pinned Lean that gives up on a certificate by heartbeats or recursion depth is reported as that rejection unless the module is at least a quarter of max_file_bytes, in which case, as when it is killed or out of memory, it is an exhausted resource, LLS8002. | §17.17, §22.8, §22.9 | diff --git a/VERIFICATION.md b/VERIFICATION.md index ced8928a8..82759aa72 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -289,13 +289,16 @@ seeded-random byte literal in which all 256 values occur. | 65536 | 100000 | 37.1 s, heartbeats (`isDefEq`) | 49.2 s, heartbeats (`LCNF compiler`) | | 65536 | default | 33.3 s, heartbeats (`isDefEq`) | 42.7 s, recursion depth | -Bisection at the default `maxRecDepth` (no `set_option`), by 16-byte steps -between 1024 and 16384 bytes, one run per size, seeded-random bytes with all 256 -values present: the largest literal that elaborates is 6394 bytes under both -renderings, and 6409 bytes fails under both (`maximum recursion depth has been -reached`). Elaboration time at 4096 bytes is 2.0 s under both; at 6394 bytes it -is 4.4 s for the `main` rendering and 3.3 s for the explicit one. The lowering -does not move the largest elaborable literal. +Bisection on a standalone scratch Lean file at Lean's default `maxRecDepth` (no +`set_option`; generated semantic modules instead emit `set_option maxRecDepth +100000`, `backend/semantic.rs`, which corresponds to the `100000` rows in the +table above), by 16-byte steps between 1024 and 16384 bytes, one run per size, +seeded-random bytes with all 256 values present: the largest literal that +elaborates at the default depth is 6394 bytes under both renderings, and 6409 +bytes fails under both (`maximum recursion depth has been reached`). Elaboration +time at 4096 bytes is 2.0 s under both; at 6394 bytes it is 4.4 s for the `main` +rendering and 3.3 s for the explicit one. The lowering does not move the largest +elaborable literal. No size succeeds under one rendering and fails under the other. Both fail at 16384 bytes at the default depth and at 65536 bytes at either depth; the @@ -5331,7 +5334,7 @@ Planted, one at a time in a focused copy of `examples/models/src/Recognizer.lex. ```text error[LLV7002]: Lean rejected `Models.Recognizer` (error): Tactic `decide` proved that the proposition - ... + scaleRatioRound32 1047092574 969894013 1000834620 = some 75739599 is false ``` @@ -8989,5 +8992,40 @@ error[LLS8002]: root `Production.Main.wide`: max_file_bytes exceeded in phase lo This is a finding about the fixture's premise, not a planted defect: the planted-defect evidence of the early refusal's bound is `conformance_sp_02`'s, -which was not completed on any host before the train's CI run (the certificate -A session's runs were killed twice by host restarts). +which passed on the train's CI run and records both the early bound and the +post-generation notation check (`SPEC.md` §17.17, #187): + +- **a root whose certificate passes lowering's lower bound and certificate B's + 12-byte-per-node derivation floor (`NODE_BYTES` in `data_b/align.rs`) is + refused by the finished-certificate notation check (`record_source` against + `max_file_bytes`).** `tests/negative/certificate-generation-limit` sums 500 + fields of a record: its 500 field reads take 250,000 pattern entries (`2,000,000` + bytes at lowering's 8-byte-per-slot floor, under the default `4,194,304`), and + its derivation's kernel nodes at `12` bytes each also stay under `4,194,304` + while record-read nodes average about `35` bytes in the recorded notation. + When `data_b::render` weighs the finished notation (`8,513,069` bytes, `2.03` + times `max_file_bytes`), it refuses with `LLS8002` before any file is staged + or Lean is started: + + ```text + error[LLS8002]: root `Production.Main.sum500` (target `rust-core`): max_file_bytes exceeded in phase certificate-b: the certificate is 8513069 bytes, beyond the 4194304 bytes of max_file_bytes + ``` + + In `conformance_sp_02`, `record copy 100` regenerated under a quarter of its + recorded size is refused *during* derivation (`the derivation of a function is + at least … bytes, beyond the … bytes of max_file_bytes`), and certificates A + and E of every stress family regenerated under half their recorded size are + refused with `LLS8002` by the finished-certificate weight check. + +### undeclared environment variables in the compiler crate can fail (`CL-17`, #180 / #187) + +`conformance_cl_17` scans every `.rs` source under `crates/lexlean/src` (with +comments and `#[cfg(test)]` items blanked) for `env::var`, `env::var_os`, +`env::vars`, and `env::vars_os` and refuses any read outside §23.1's four +operational variables (`WIDTH_VARIABLE`, `TELEMETRY_VARIABLE`, `HINTS_VARIABLE`, +and `MEMORY_VARIABLE` in `verify/operational.rs`), `cli.rs`'s `"NO_COLOR"` +presentation check, and the toolchain/process locators `"HOME"`, `"PATH"`, and +`"ELAN_HOME"` in `verify/child.rs` and `verify/toolchain.rs`. On every run it +plants `let _ = std::env::var("LEXLEAN_AXDBG");` on a copy of +`production/certificate/data_a.rs` and requires the scan to report +`production/certificate/data_a.rs`. diff --git a/crates/conformance/src/cases/cli_api.rs b/crates/conformance/src/cases/cli_api.rs index f601348c5..07fe62402 100644 --- a/crates/conformance/src/cases/cli_api.rs +++ b/crates/conformance/src/cases/cli_api.rs @@ -934,6 +934,88 @@ pub(crate) fn run(id: &str) { assert!(stderr.is_empty()); }, ); + + // §23.1: no source in `crates/lexlean/src` reads an environment + // variable beyond the four operational variables of §23.1 + // (`LEXLEAN_VERIFY_WIDTH`, `LEXLEAN_VERIFY_HINTS`, + // `LEXLEAN_VERIFY_MEMORY_KIB`, `LEXLEAN_CI_TELEMETRY`, in + // `verify/operational.rs`) and the toolchain locator's ambient + // `HOME`, `PATH`, and `ELAN_HOME` (`verify/child.rs` and + // `verify/toolchain.rs`). + fn undeclared_env_reads(sources: &[(String, String)]) -> Vec { + const ALLOWED: &[(&str, &str)] = &[ + ("verify/operational.rs", "WIDTH_VARIABLE"), + ("verify/operational.rs", "TELEMETRY_VARIABLE"), + ("verify/operational.rs", "HINTS_VARIABLE"), + ("verify/operational.rs", "MEMORY_VARIABLE"), + ("cli.rs", "\"NO_COLOR\""), + ("verify/child.rs", "\"HOME\""), + ("verify/child.rs", "\"PATH\""), + ("verify/child.rs", "\"ELAN_HOME\""), + ("verify/toolchain.rs", "\"ELAN_HOME\""), + ("verify/toolchain.rs", "\"HOME\""), + ]; + let mut offenders = Vec::new(); + for (path, source) in sources { + for (line_no, line) in source.lines().enumerate() { + let code = line.split("//").next().unwrap_or(""); + for call in ["env::var_os(", "env::var(", "env::vars_os(", "env::vars("] { + let mut rest = code; + while let Some(at) = rest.find(call) { + let after = &rest[at + call.len()..]; + let arg = after.split(')').next().unwrap_or("").trim(); + let allowed = (call == "env::var_os(" || call == "env::var(") + && ALLOWED + .iter() + .any(|(file, want)| path == *file && arg == *want); + if !allowed { + offenders + .push(format!("{path}:{}: `{call}{arg})`", line_no + 1)); + } + rest = after; + } + } + } + } + offenders + } + + let mut sources = Vec::new(); + library_sources( + support::repo_root() + .join("crates/lexlean/src") + .as_std_path(), + &mut sources, + ); + assert!( + sources.len() > 50, + "the scan reads the library, found {} files", + sources.len() + ); + let offenders = undeclared_env_reads(&sources); + assert!( + offenders.is_empty(), + "§23.1: undeclared environment variable reads in crates/lexlean/src: {offenders:?}" + ); + let mut planted = sources.clone(); + let target_file = planted + .iter_mut() + .find(|(path, _)| path == "production/certificate/data_a.rs") + .expect("data_a.rs is scanned"); + target_file + .1 + .push_str("\nfn _planted() { let _ = std::env::var(\"LEXLEAN_AXDBG\"); }\n"); + let caught = undeclared_env_reads(&planted); + assert_eq!( + caught.len(), + 1, + "planted std::env::var outside §23.1 is caught: {caught:?}" + ); + assert!( + caught[0].contains("production/certificate/data_a.rs") + && caught[0].contains("LEXLEAN_AXDBG"), + "{caught:?}" + ); } // §30.3: the exact version report. "CL-18" => { diff --git a/crates/conformance/src/cases/models.rs b/crates/conformance/src/cases/models.rs index 8e186eb56..17f035b6c 100644 --- a/crates/conformance/src/cases/models.rs +++ b/crates/conformance/src/cases/models.rs @@ -660,9 +660,33 @@ fn md_02() { // proved to be their decoding. let build = support::rendered(&project); let lean = support::lean_text(&build, "Recognizer"); - let banner = std::fs::read(project.root.join("artifacts/banner.bin").as_std_path()) - .expect("banner bytes"); - assert_eq!(embedded_artifact_octets(&lean, "banner"), banner); + for (module, name, path) in [ + ("Recognizer", "banner", "artifacts/banner.bin"), + ( + "Recognizer", + "hiddenWeights", + "artifacts/hidden-weights.bin", + ), + ("Recognizer", "hiddenBias", "artifacts/hidden-bias.bin"), + ( + "Recognizer", + "outputWeights", + "artifacts/output-weights.bin", + ), + ("Recognizer", "outputBias", "artifacts/output-bias.bin"), + ("Recognizer", "digitNames", "artifacts/digit-names.txt"), + ("Triage", "triageWeights", "artifacts/triage-weights.bin"), + ("Triage", "triageBias", "artifacts/triage-bias.bin"), + ] { + let module_lean = support::lean_text(&build, module); + let expected_bytes = + std::fs::read(project.root.join(path).as_std_path()).expect("artifact bytes"); + assert_eq!( + embedded_artifact_octets(&module_lean, name), + expected_bytes, + "{module}.{name}.bytes matches {path}" + ); + } assert!(lean.contains("public theorem banner.decoded : banner = banner.bytes := rfl")); let weights = std::fs::read( project @@ -676,7 +700,6 @@ fn md_02() { .map(u8::to_string) .collect::>() .join(", "); - assert_eq!(embedded_artifact_octets(&lean, "hiddenWeights"), weights); assert!(lean.contains( "public theorem hiddenWeights.decoded : (LexLeanModels.tensorMatches 1 true hiddenWeights.flatten hiddenWeights.bytes && (hiddenWeights.length == 12) && (hiddenWeights.map List.length == List.replicate 12 7)) = true := by decide" )); @@ -3531,6 +3554,8 @@ fn md_13() { let raw = (exp << 52) | frac; let bits = if index % 3 == 0 && raw > 0 { i128::from(raw) - (1_i128 << 63) + } else if index % 3 == 1 && raw > 0 { + i128::from(raw) + (1_i128 << 63) } else { i128::from(raw) }; diff --git a/crates/conformance/src/cases/semantic_ir/widen.rs b/crates/conformance/src/cases/semantic_ir/widen.rs index 23f64f5bd..f13ee3100 100644 --- a/crates/conformance/src/cases/semantic_ir/widen.rs +++ b/crates/conformance/src/cases/semantic_ir/widen.rs @@ -166,6 +166,62 @@ pub(super) fn run() { ); } + // A production root over `UInt64` and `Int64` reaches `to_int`'s overflow + // at or above 2^63 (§17.12 *Widening conversions* rule 2), while inputs + // below 2^63 evaluate to their exact integer values. + { + use lexlean::calculus::{interp, Outcome, Value}; + let wide = P::copy_example("production"); + let wide_src = "\\begin{lexlean}{Main}\n\\useglossary{lexlean.std.nat@1.2.0}\n\\title{Natural number addition}\n\\begin{semanticmodule}\ndefinition{\n name: widenWide,\n parameters: [u64 : UInt64, i64 : Int64],\n result: (Int * Nat),\n body: ((prim subtract (prim to_int u64 : Int) (prim to_int i64 : Int) : Int), (prim to_nat u64 : Nat)),\n axioms: [Quot.sound, propext],\n executable: true,\n production: {effects: [overflow], targets: [rust-core, rust-std]}\n}\n\\end{semanticmodule}\n\\end{lexlean}\n"; + wide.write("src/Main.lex.tex", wide_src); + wide.check_ok(); + let certified = crate::preservation::certificates(&wide); + assert_eq!(certified.len(), 1, "one production root"); + let program = &certified[0].program; + let run = |u: u64, i: i64| -> Outcome { + interp::run( + program, + 100_000, + 0, + &[ + Value::U64 { + value: u.to_string(), + }, + Value::I64 { + value: i.to_string(), + }, + ], + ) + }; + match run((1_u64 << 63) - 1, 0) { + Outcome::Value { + value: Value::Pair { left, right }, + .. + } => { + assert_eq!( + *left, + Value::Int { + value: i64::MAX.to_string() + } + ); + assert_eq!( + *right, + Value::Nat { + value: ((1_u64 << 63) - 1).to_string() + } + ); + } + other => panic!("expected Value at 2^63 - 1, got {other:?}"), + } + for u in [1_u64 << 63, u64::MAX] { + let outcome = run(u, 0); + assert!( + matches!(outcome, Outcome::Overflow { .. }), + "`to_int` on UInt64 {u} (>= 2^63) must overflow Int64 in the calculus: got {outcome:?}" + ); + } + } + // The kernel decides every width at its bounds. let bounds = P::language_1_2_example(); bounds.write("src/Main.lex.tex", &bounds_module()); diff --git a/crates/conformance/src/lean_literals.rs b/crates/conformance/src/lean_literals.rs index dadc8904d..ef09af27a 100644 --- a/crates/conformance/src/lean_literals.rs +++ b/crates/conformance/src/lean_literals.rs @@ -46,7 +46,7 @@ pub struct Finding { /// The literals that are Lean syntax and are not templates: the file they are /// in (a suffix of its path), the beginning of the literal, and why. -pub const ALLOWED: [(&str, &str, &str); 10] = [ +pub const ALLOWED: [(&str, &str, &str); 9] = [ ( "production/certificate.rs", "«{segment}»", @@ -67,11 +67,6 @@ pub const ALLOWED: [(&str, &str, &str); 10] = [ "(let {n} : {ty}", "the printout of a kernel let, read by developers in diagnostics", ), - ( - "production/certificate/data_a.rs", - "{full} : {}", - "a developer's printout of a row under LEXLEAN_SHOW, never written to a module", - ), ( "backend/lean.rs", "set_option autoImplicit false", diff --git a/crates/lexlean/src/production/certificate/data_a.rs b/crates/lexlean/src/production/certificate/data_a.rs index 5718fcb80..0964b2465 100644 --- a/crates/lexlean/src/production/certificate/data_a.rs +++ b/crates/lexlean/src/production/certificate/data_a.rs @@ -362,11 +362,7 @@ impl<'g, 'a> Writer<'g, 'a> { } } for name in names { - let found = self.constant_axioms(&name)?; - if std::env::var("LEXLEAN_AXDBG").is_ok() && !found.is_empty() { - eprintln!("AXDBG {name} {found:?}"); - } - out.extend(found); + out.extend(self.constant_axioms(&name)?); } Ok(out) } @@ -380,14 +376,6 @@ impl<'g, 'a> Writer<'g, 'a> { value: Term, ) -> Result<(), String> { let full = format!("{}.{name}", self.name); - if std::env::var("LEXLEAN_SHOW").is_ok_and(|wanted| full.ends_with(&wanted)) { - let text = format!("{full} : {}\n:= {}\n", self.b.show(ty), self.b.show(value)); - if let Ok(path) = std::env::var("LEXLEAN_SHOW_FILE") { - let _ = std::fs::write(path, text); - } else { - eprintln!("{text}"); - } - } if self.b.has_placeholder(ty) || self.b.has_placeholder(value) { return Err(format!( "the row `{full}` of certificate A has a free variable or placeholder left" diff --git a/features/suites/preservation.feature b/features/suites/preservation.feature index 9ccf1281d..fde9cad47 100644 --- a/features/suites/preservation.feature +++ b/features/suites/preservation.feature @@ -10,7 +10,7 @@ Feature: preservation And a report whose closure omits a member fails with LLI9001, and a default arm planted in a preservation source is refused @SP-02 @build - Scenario: Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it, and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; and in every case by generating each certificate under the limit, which stops it at the limit; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. + Scenario: Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it (and a mixed shape that fits at its full scale of 256 is checked to fit and not edge-checked), and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; during certificate B's derivation at 12 bytes a kernel node; and for every certificate by weighing the finished module in the authoring notation it is recorded in against max_file_bytes before any file is staged; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline. Given every production root of examples/production and of examples/production-coverage When each certificate is compiled with the pinned Lean beside the library and the generated modules, replayed, and its axioms audited Then every certificate is accepted and its root theorem depends on exactly the three classical axioms diff --git a/model/ids.toml b/model/ids.toml index 4fd434ef6..7afcb1fcf 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -1878,7 +1878,7 @@ statement = "Every production root of the committed examples lowers to a valid r id = "SP-02" level = "build" suite = "preservation" -statement = "Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it, and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; and in every case by generating each certificate under the limit, which stops it at the limit; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline." +statement = "Every production root of examples/production, examples/production-coverage, examples/models, and examples/reasoning has a certificate whose root theorem, that the lowered program converges on the encoded arguments to the encoded source value or to overflow exactly where the width predicate fails, compiles under the pinned Lean, replays through leanchecker, and depends on exactly Classical.choice, Quot.sound, and propext; a certificate generated against a program with a planted branch, arithmetic, constructor, recursion, or literal mutation is rejected, and each such rejection lies in the declaration of the function mutated; and a root whose lowered program or certificates would exceed max_ir_nodes or max_file_bytes is refused with LLS8002 before the toolchain is touched: early, by a lower bound on each certificate from what the program states, the greatest of which is compared with the limit and none of which is above its certificate on the corpora, on families of programs that grow one dimension at a time, and on programs that grow several at once, so that a program whose certificates fit, a match on 240 constructors, a string of 450 000 characters, or both a wide match and a long string, is not refused by it (and a mixed shape that fits at its full scale of 256 is checked to fit and not edge-checked), and by a floor on certificate B from the entries its field reads print, which the lowering refuses before the Rust crate is built; during certificate B's derivation at 12 bytes a kernel node; and for every certificate by weighing the finished module in the authoring notation it is recorded in against max_file_bytes before any file is staged; the programs, crates, and certificates of all the roots of a project count together toward max_total_source_bytes, which a chain of roots calling one another passes before memory is exhausted; and a match on 180 constructors verifies through the whole pipeline." [[id]] id = "SP-03"