cert: one plan grammar built from MIR instead of plan families - #1412
Merged
Merged
Conversation
Plan-shaped functions in modules with the Int carrier were lowered through the certification plan lowerer instead of the MIR emitter. That path is removed, so the wasm-gc backend has one body emitter. The producer still receives its MIR-derived plans as certificate input; a plan whose lowering no longer matches the emitted bytes declines. Across the certkit fixtures, the json and hello examples, the projects and btc-listener, 7 of 8139 code entries change (+125 bytes); four fixture exports (letnamed x3, cell_at) now decline. The PlanEmittedCanonicalCodegen decision is replaced by MirEmitterIsTheOnlyEmitter. The plan-path engagement test is dropped; the carrier on/off agreement test stays. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The MIR emitter lowers `!=` against an Int literal with `i64.ne`, `!=` over `__aint_eq` and `Bool.not` with `i32.eqz`, Bool `!=` with `i32.ne` and `Bool.or` with `i32.or`. The one-grammar lowering needs all four. `i64.ne`, `i32.eqz` and `i32.ne` follow the value convention of the existing `i64.eq` / `i32.eq` cases. `i32.or` is exact on 0/1 operands and stuck on anything else, so it never yields a value the bitwise wasm instruction would not. CertPreludeSanity gains edge-value examples for each, including the stuck cases. This changes the embedded wall sources, so the wall id no longer matches CURRENT_WALL_ID; the rotation is deferred to the end of the branch. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…theorem Grammar.lean mirrors the admitted subset of MirExpr (literals, locals, named lets, calls to user functions and to Bool.and/or/not, tail calls, Int and Bool binary operators, Int negation, if/else, record create in declared order and field projection) with its typing and source semantics, including fuel-indexed group models for SCCs. GrammarLower ports the wasm-gc MIR emitter for exactly these nodes and makes the same choices from the same tree: the literal compare looks for the literal on the left first and flips the operator, re-emits a bare local and stashes anything else in the const-compare scratch local, and single-use let copies stay locals. One lowering yields both the instructions the interpreter runs and the code-entry bytes. GrammarSound proves `agreement` by structural induction over the grammar and `fn_certified_group`, which certifies every member of one group by fuel induction, with callees outside the group as FnCertified hypotheses. Axioms: propext, Classical.choice, Quot.sound. The files are built by the development lakefile only; they are not yet in the verifier's source set. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The plan grammar mirrors MirExpr::Match and MirExpr::Construct: Int literal cascades with a catch-all last, the two-arm Bool match the if-rewrite keeps, the Option and Result tag dispatch with payload binders, and the user-variant ref.test cascade whose last arm is untested. Option.withDefault and Result.withDefault are admitted as lazy builtins, evaluated as the emitter lowers them. Source values gain variants and instantiation-carrying Option and Result values. The lowering ports the emitter for these nodes, including the subject scratch, the dead binder extraction and the default fillers; scratch positions are a function of the declared locals. The typing admits exactly the arm shapes whose emitted code has first-match meaning, and requires a variant cascade to cover every constructor and a sum to keep its constructor structs distinct. The agreement theorem and the group theorem extend to the new nodes with the same axioms. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The audited interpreter compares type indices in ref.test while wasm GC tests subtyping. The variant cascade is sound only when no represented value has a struct type that is a strict subtype of another constructor's struct. S3Pin states the byte fact that rules this out: every constructor struct of a sum sits in the rec group that opens the type section and is declared sub final under the sum's root. ctor_refTest_exact shows that, under this pin and the two wasm GC subtyping facts it relies on, the exact test is the wasm test on every pair of constructors of one sum. The acceptance must check the pin against the type section bytes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-grammar plan The plan grammar now covers every construct the old families certify: String literals (by data segment), concatenation (binary and interpolation), equality and literal matches; Float literals and comparisons (no arithmetic); the fused Option.withDefault over Vector.get with a literal default; the empty list and List.prepend; the flat tuple destructure; opaque pass-through fields; and one-field records represented as their field's value. The lowering ports the MIR emitter for these nodes, and the agreement theorem and the group theorem extend to them. The new helpers (concatenation, string equality, index conversion) are taken with the contracts the schema already assumes of them. Scratch locals no longer have to exist: every stash is read back at once, so a carrier-free function with no declared locals is certified too. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A string literal lowers to array.new_data over a data segment, while the interpreter carries the literal's bytes. DataPin states the check the acceptance must make against the data section: every literal of a plan names a segment that holds exactly its bytes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
GrammarTotal computes the termination check from the plan alone: every member of a group has Int parameters, an `n <= 0` guard over parameter 0, a call-free base arm, and a step arm of Int arithmetic whose member calls all pass `n - 1` first. The group role is `.mul` exactly when a member multiplies, and a literal multiplier keeps a plan at L1. fn_certified_total proves main's L3 promise for a checked group: at fuel `n.natAbs + 1` the run returns and the plan's model at that fuel is defined and represented by the result, under the partial contracts plus box, add and sub totality (and mul for the `.mul` role). Not yet wired into acceptance, so the wall id is unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A `*` with a literal operand is as total as any other Int product, and the L3 group theorem covers it without change, so `k * f(n-1)` now reaches L3 at role `.mul` like `n * f(n-1)`. A literal outside the i64 band is still declined, by the typing. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…a 9) The statement, the acceptance root and the soundness assembly are rewritten over the one plan grammar, and every family file is deleted. - SchemaBase: the registries, identities, subject, policy axes, carrier specification and the Int helper contracts, split out so the grammar can build on them. - SchemaCore: schema 9. The manifest carries the subject, a declared type table, one list of planned functions (the MIR bodies printed 1:1) and the obligations. An obligation is stated over the grammar: the model is the plan's fuel-indexed meaning and the face is the plan's signature read through the byte-pinned layout. L3 is the partial statement plus return at the checked fuel. - TypeTable: the lowering context of a manifest, and the declare-and-confirm pins of the type table against the rec group that opens the type section (field storage of every struct, constructor structs `sub final` under their root with S3Pin and sumOk, carrier and magnitude array, strings, vectors, lists, Option and Result instantiations, newtypes) and of every string literal against its data segment. - AcceptedArtifactCore: the obligations are derived by the wall (`obligationsOf`); every planned function is bound to its code entry by export name or function index, with its declared function type; calls go only to planned functions of the same or an earlier group; role and planned indices are distinct; present helpers have their role's function type. The helper-body pins and the whole-module accounting are kept. - ClaimAxes: contracts from the helper calls of the lowered code, one report class `source-plan-v1` with facets derived from the plans. - AcceptanceSoundness: `fn_claim_discharges` (one fuel induction over all plans, plus the group totality theorem for L3 groups) and `accept_sound`, axioms within [propext, Classical.choice, Quot.sound]; an S-3 corollary for accepted artifacts. - The Int negation role is declined: it has no wall template yet, so a plan with `neg` does not encode. - CertPreludeSanity uses `decide +kernel` instead of `native_decide`; SchemaSanity gains typing negatives and a contract witness. The wall goes from 47 files and 29497 lines to 22 files and 11492 lines. The Rust producer still emits schema-8 packages, which do not verify against this wall until the producer is rewritten. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
- wall.rs: the embedded source set is the 19 files of the rebuilt wall, and the pristine roots are every module but the two artifact-dependent ones. - The wall id is rotated in format.rs, the format specification and the two package snapshots; the specification states the new source count. - The capability-registry test reads the registries from SchemaBase. - Byte-binding lint: a binder named with a `?` suffix is typed from its match scrutinee; under `xs.all (f a ...)` each element of a producer list counts as passed to `f`; a producer value equal to a wall function of other producer values is derived (rule D), which is how the obligations are now pinned. The source type id of a record is a declared-only name over a byte-confirmed layout. The historical index-helper regression still flags. - Trust inventory: the two wasm GC facts the exact `ref.test` relies on are stated as hypotheses of the S-3 argument, not axioms. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The emitter exports `__aint_eq` only when a user code path marks it live, while an Int literal match calls it regardless, so the export-name pin declined every module whose only equality use is such a match. The role is now pinned like add, sub and mul: a declared index must hold the equality template, and an undeclared role lowers to an index no code entry encodes. `cmp` keeps its name pin, so the two comparison helpers stay apart. The wall id is rotated in format.rs and the format specification. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The compiler now prints every emitted function's optimized MIR body 1:1 into the one plan grammar, from the same compile the wasm-gc emitter consumed: `plan_from_mir.rs` maps each admitted MIR node to the grammar node of the same name and declines any other node, pattern or type by name. Types, struct indices, helper and data-segment indices come from the emitter's own registry through `wasm_gc/cert_layout.rs`, into one module-wide type table. The producer (`aver-cert/src/engine`) checks each plan against the exact module bytes before rendering: Rust twins of the wall's typing, lowering, type-table confirmation and totality check decline a plan whose lowering is not its code entry per function, instead of failing the whole package in Lean. The offered functions are grouped into call SCCs, callees first, and rendered as `Plans.lean`, `Manifest.lean` (obligations are the ones the wall derives), `Artifact.lean`, `Final.lean` and `ArtifactCertificate.lean`. The manifest moves to schema 9: every certified export reports the one class `source-plan-v1` with facets, which the checker witness pins against `ClaimAxes.reportEntries` and `ClaimAxes.reportFacets`. Law-claims and source bridges are not carried yet; the checker refuses a package declaring either, and the Lean model emission is no longer run. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The byte classifiers, the per-family plan definitions and renderers, the family-keyed rederivation, the sym/expression-fragment plan IR with its byte lowering, the model evaluator and the record-compute bridge producer are unreachable now that every certified function is its printed MIR plan. The MIR-to-fragment adapter in `src/codegen/cert` goes with them, and `aver-cert` no longer needs `wasm-encoder`. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A decline now says which intrinsic a call is, and that a record create or projection is over a one-field record the emitter erases, instead of leaving those to the generic typing decline. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A large module (payment_ops, workflow_engine) ran the whole-module conjunction out of the default elaboration budget in one `decide`. Each of the five facts is now its own theorem, and `Artifact.lean` states the same explicit heartbeat allowance the family packages carried. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The byte-binding lint counted `planTyped M e.plan` and `callsOrdered fns e` as binding every plan field and the call group, because both conjuncts sit in a definition whose `match` reads the bytes. With the code-entry equality removed the lint stayed green. Rule A1 now needs the callee to read the bytes itself, or the conjunct to meet them on its own. A new rule C2 recognises the real pin: a value lowered by a wall function and then compared for equality with the module bytes (`codeEntryBytes M e.plan` into `exactFuncBindingForExport`). The call scanner also finds calls nested in another call's arguments, so the function type pin `sigPinned` binds the signature. Rule D is now checked on the parsed application: every argument must be producer-free or a whole producer value that is not the value, an ancestor or a part of it, cannot contain its type, and has every leaf bound by the other rules or a standing allowance. `m.subject = subjectOfManifest m` no longer binds `Subject`. Only `obligationsDerived` fires D on the current wall. `FnEntry.group` becomes a declared-only allowance: partial correctness is one fuel induction over all plans, and the L3 check admits recursive calls only to members of the declared group, so a wrong grouping can only lose L3. Both counterexamples are regression tests. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
An obligation quantifies over well-typed arguments. A declared type with no finite value made that hypothesis unsatisfiable and the obligation true of any code: a self-referential newtype `R = [record R]` (whose struct pin then reads as a tautology) used as a parameter or field, `eqref` in a signature, or a record `R = [int, record R]` over a self-referential struct. Such a package was accepted. `plansAccepted` now also requires `TypeTable.declsWellFormed`: - `eqref` only as the subject-scratch local, never in a signature, a record or constructor field, or an Option / Result / List / Vector element; - no newtype cycle; - every declared record and sum, and every parameter and result type of every plan, inhabited, by a least fixpoint over the type table. `inhabTy_sound` turns a passing check into a value, and the new theorem `AcceptanceSoundness.accepted_nonvacuous` states that every certified export of an accepted artifact has well-typed arguments and an inhabited result type. Opaque heap types join the struct indices that must be unique. The producer mirrors the check and declines per function. The local P4 variants probe gains the review's certificate and the other routes as negatives; each keeps every byte pin passing and is declined by the declaration check alone. The wall identity rotates. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…3 limits The trust inventory now states three assumptions the statement makes: - runtime helpers are modelled as pure functions of their argument values, so the theorem assumes they mutate nothing the caller can reach; the mutability of the carrier's fields and of `$string` is not pinned; - the bignum sub-routines the add, sub, mul and cmp templates call are not pinned, so the truth of those contracts for a given artifact rests on code the certificate does not look at (this predates schema 9); - "returns" at L3 is about the wall's interpreter: stack exhaustion and allocation failure in a real engine are not covered. The architecture document's trust boundary lists these and the two wasm GC facts behind the exact `ref.test`. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d of panicking An effectful function using Wait.poll, whose oracle is generic over its key type, lifted to a signature with an unresolved type variable, and the Lean type renderer panicked on it, aborting the whole export (btc-listener's model emission). The lift now declines with GenericOracle and proof export drops that one function, as it already does for any function it cannot lift. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…and proof engines The wall now defines what a schema-9 bridge says about an export's obligation (exportObligation, ArgsTyped, the exact and adequate kinds) and what an adequate bridge means for the bytes (adequate_transfer). Two engines assemble a bridge from one step lemma per function: bridge_of_step (adequacy at every fuel by one fuel induction over a call closure, through evaluation monotonicity, so recursion and mutual recursion need no per-function induction) and exact_of_step (exact answers above a declared call depth for a closure without recursion). String values get their byte encoding strBytes, its injectivity and the choice decoder decodeStr. The wall id rotates. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The certificate model converted well-founded Int recursion to explicit fuel for the retired recursion wall. A plan-equals-source bridge unfolds a source function one step through its equation lemma instead, which a fuel wrapper does not offer, so the model now keeps the same recursion shapes as proof export. The entry and dependency Lean namespaces are exposed so the certificate producer can name a transpiled function by its wasm export. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The producer emits the Lean source model again at --certify (a panic in that emission costs the package its bridges and law-claims, never the byte certificate) and bridges every certified export whose source definition, encoders and callees resolve. Encoders cover Int, Bool, Float, String, records, user sums, Option, Result, tuples, lists and vectors; a parameter must also decode (Float, List and Vector parameters and recursive types decline). Bridge.lean proves one step lemma per function and assembles each export's bridge with GrammarBridge.exact_of_step for a call closure without recursion and GrammarBridge.bridge_of_step otherwise. Every proof is first | script | sorry under a heartbeat cap, so a proof that does not close costs exactly the bridges whose closure uses it. The manifest entry gains the statement kind, and the encoder specs their schema-9 forms; the checker renders the statement from that structure with the one renderer both sides share, pins and audits each bridge and each bridged law as before, and no longer refuses either surface. Nested model files are admitted through Bridge.lean and Laws.lean imports. The k5 law and bridge tamper tests are ported to the new surface. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A step whose plan and source branch in different orders left an if inside a hypothesis; the script now splits those too before the final arithmetic. Adds renderer tests for the String literal and constructor split helpers. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The checker's token scan, file-name rule and law-claim identifier rule move into lean_gate.rs, which the producer can call too. Where the two sides had their own copies they disagreed, and one disagreement was enough for the checker to refuse a whole package over a single bridge or law. - A model name escaped with a trailing prime (none') now passes the bridge gate, which uses the same identifier rule as the producer. A law theorem may carry the same escape; labels and corollaries may not. - The producer's law gate calls the checker's functions, with the checker's statement length cap instead of a stricter local copy. - The token scan admits exactly one form of deriving: the classes BEq, DecidableEq and Inhabited on a type, or ReflBEq and LawfulBEq in a deriving instance line, with nothing else on the line and no continuation after it. A package cannot register a derive handler, so this runs only the pinned toolchain's handlers for those classes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…deriving Two defects made aver-cert check refuse a whole package: - A model that uses Bits or whose law proofs close with aver_int_order shipped the AverBits prelude (with @[simp] lemmas) and the aver_int_order syntax/macro_rules pair in AverCommon.lean, and the token gate refuses both. They now live in a new wall source, ModelPrelude.lean, which the checker owns and pins by the wall id; a certificate model imports it instead of carrying the text. The macro is recursive, so expanding it into the proofs was not an option. A compiler test pins the wall text to the proof-export prelude constants byte for byte. - The producer stripped every deriving line, so == on a record had no BEq instance and the model failed to build. The certificate model now keeps the derived BEq, DecidableEq where the type reflects equality, and the ReflBEq/LawfulBEq line, and drops Repr and Inhabited (the explicit Inhabited instance stays). The hand-written BEq for enums is gone: it shadowed the derived instance the LawfulBEq line is about. The wall gains one source, so the wall id rotates. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…shipping Three more ways one law or bridge could cost the whole package: - A user module named Laws (or Bridge, Manifest, Grammar, Schema, ...) shadowed a package or wall file, so the producer left out the whole model and declined every bridge and law. Model files now ship under the reserved directory AverModel/, with model-to-model imports rewritten; the Lean namespaces, and so every name a claim cites, do not change. - A deterministic maxHeartbeats timeout in one law proof escaped the first | ... | sorry ladder (Lean re-throws resource-limit exceptions past every tactic combinator) and failed the build. Every theorem of the model, Bridge.lean and Laws.lean is now prefixed with #guard_msgs (drop error) in. Lean's error recovery already closes a failed goal with sorryAx; only the error message failed the build. The axiom audit then declines exactly the claims that rest on the failed proof. - The producer runs the checker's file-name rule, case-collision rule and token scan over every model file, keeping only the deriving classes the gate admits. A model that would still fail is declined with a reason, costing its bridges and laws and never the byte certificate. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The certificate model exports a when-guarded holds law as a universal claim only when its unfold cone is transparent arithmetic. Bool.and, Bool.or and Bool.not counted as opaque builtins, so a law like the k5 Table 3 rows (a window Bool.and(a <= x, x <= b) under a when) kept its bounded sampled-domain statement and was left out entirely. These three are written inline as &&, || and ! in the Lean model, so there is nothing to unfold; the cone walker now admits them and the proof's simp set gains the lemmas that turn them into propositions for omega. The proof still ends in sorry when it does not close, and the axiom audit decides credit. On k5_fdiv this adds 16 law-claims, all credited. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…etter A law of a function named after a Lean keyword (btc-listener's Rules.at) lives in a theorem like at'_law_rulesOnlyTurnOn, with the transpiler's prime in the middle of the name. The shared identifier rule only allowed trailing primes, so the producer left three such laws out. Lean lexes a prime after a letter as part of the identifier, so admitting it anywhere after the first character cannot open a character literal. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…branch Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Conflicts kept the docs branch's structure and carried the newer facts from the checker hardening and the layout rounds: the audit program and the pure witness, the tokenized package text gate, bridge statements as applications of GrammarBridge.Exact/Adequate, the law bridge-list rule, the divmod type pin, the declared layout and fast readings, the per-module data cache, the 22-file wall and its current identity. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The produce unit tests read three wasm-gc modules from an untracked notes directory, so they failed on a clean checkout. The modules are committed byte for byte under aver-cert/tests/fixtures/one-grammar, because the tests' plans name their exact function and helper indices. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Every certified theorem reads an Int through CanonRepr, so it assumes each Int input is a canonical carrier word. explain printed that per export for the retired record face and then not at all; it now states it once under Certified domain, and the k5 explain test asserts the line. The same test now looks for the bridge statement in its pinned GrammarBridge.Exact form, and the token tripwire for the tokenized gate's reason. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
No allowance has used it since the schema-9 wall, and clippy fails the aver-cert test build on the dead variant. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # docs/language.md # tools/website/playground/index.html
…e shape - Refresh the add_one certificate snapshot for the current wall identity. - Add the divmod role to the phase-timeout fixture's host-role table. - Pin the aver-cert plans feature as dependency-free in the release test. - Fix clippy findings in the certificate engine and the plan printer: collapse nested ifs, use then_some and the question-mark operator, name the complex tuple types, and pass the rendered surfaces to the manifest renderer instead of four of their fields. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…pin shapes The wall's Schema imported the package's Module.lean, and Lean resolves a dotted name in the innermost namespace first. A package could therefore declare AverCert.AcceptedArtifact.AverCert.ClaimAxes.checked and have the wall's own accepted predicate use it, so a certificate with its runtime contracts dropped verified. The verifier now renders Module.lean from the hash of the bytes it read and ignores a package file of that name, the wall qualifies its cross-namespace references from the root, and the audit program declines any package constant under a wall or checker namespace. The witness now elaborates every law and bridge statement alone, as a checker definition, and conjoins the definitions, so a statement cannot re-associate a pin's conjunction. The statement gate counts delimiters the way Lean reads them, skipping string and char literals and quoted identifiers, and refuses what it cannot lex exactly. The wall id changes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…Module A configured data or prelude cache is trusted local state. verify now ignores both variables with a notice and builds from the staged sources, so its verdict never rests on a cache; check keeps using them. The format and architecture documents describe the checker-rendered Module.lean, how the witness pins the artifact hash, the namespace audit, and the pins that conjoin statement definitions. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
cert_hardening_spec had no certification lane, and in ci.yml it compiled to no tests without the wasm feature, so its tampers never ran with Lean. It now has a lane with the features it needs. The decide job fails when a tests/cert_*.rs suite has no lane, the certification lanes set AVER_CERT_REQUIRE_LEAN=1 so a certificate test that finds no lake fails instead of skipping, and pull requests run the hardening and guard isolation lanes beside the existing smoke lanes. The workspace job also runs the aver-cert unit tests with every feature, which covers the producer's. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…asses The token gate read the rest of a file as code after any s! string, so a doc comment reading "payment-scoped" in the payment_ops model tripped the refused word `scoped`. The model was then not shipped, and the project's one law-claim silently left the manifest. The gate now lexes s! strings exactly: their text is inert and their interpolated terms are code. Anything it cannot read exactly still makes the rest of the file code. With the model shipped, the audit declined the map prelude's AverKeyOrder instances: isClass reads extension state the audit's imported environment does not rebuild, so every package class looked undeclared. The audit now reads the class from the declaring module's own entries. The hardening baseline reads a Map so its clean certificate covers these instances. The nested-module test expects the single-parameter binder the bridge renderer writes (x, not x0). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
tools/cert_ratchet.py compiles the certificate corpus (certkit fixtures, the JSON example, k5_fdiv and payment_ops) with --certify, which writes the package without Lean, and compares the certified exports, source bridges and law-claims per program with tools/cert-baseline.json. A loss fails and is named; a gain fails until the baseline is updated in the same commit. The checks lane runs it on every pull request. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ecker-owned Module The guard isolation tests cut conjuncts out of arithTableCheck by their text, which now spells CertDecode as _root_.CertDecode. The claim-free hash rebind is now refused while the package data builds, because the checker renders Module.lean with the hash of the bytes it was handed; the test accepts that stage and still requires the artifact-hash face to be the one named. The JSON example carries eleven law-claims. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A certificate is for the bytes that ship, so --certify no longer turns the buffer builder, chars fusion and byte sink off. Instead every wasm-gc and wasip2 build leaves unfused each function the certificate plan printer could print in its source form (ir::cert_shape). The predicate is a syntactic superset of printer admission, read once before the first fabricating pass; the printer refuses any builtin outside the same PRINTED_BUILTINS list, so the two cannot drift. A kept classifier still grows its __code variant from a rewritten copy, and an indexed worker starts from that copy too, so loops keep reading one codepoint while the classifier keeps its source body. tests/cert_one_build_spec.rs compiles the certificate corpus plain and with --certify and requires identical modules, and checks on the corpus that every function the printer admits unfused is one the predicate keeps. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A wasm-gc module with job kinds imports submit, take, task and complete from aver:work/v1, and the certificate refused it on the first of them. The four pairs join the wasm-gc capability registry in the wall and in its Rust mirror; like every import they are accounted and never claimed, since no certified closure may reach an import. A decide theorem pins them to wasm-gc only, work_abi::IMPORTS feeds both the emitter and the compiler/verifier parity test, and the wall identity rotates. The new cert_work_job fixture certifies its job body, declares the four imports in import order with their exact types, and joins the ratchet corpus. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A large program's type table did not elaborate: btc-listener's string segments (151 entries, the longest 570 bytes) made one list literal deeper than maxRecDepth, and the whole table one declaration past maxHeartbeats. The subject's exports and declared-uncertified lists hit the same limit in Manifest.lean. A list field that exceeds 64 entries or 4096 characters is now written as its own declarations (Plans.types_<field>_<k>, subject.<field>_<k>), each within both bounds, joined with ++ in the table or the subject; a byte list longer than 64 is written as ++-joined literals. The value is the same list, so the wall's decide and the checker's rfl pins see what they saw before. Small tables render as one declaration, unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
btc-listener's model did not reach the checker, or did not build: - the Random.int oracle lemma carried @[simp], which the token gate refuses; the certificate model now states it without the attribute; - a record with a field that has no default (a capability handle) got an Inhabited instance that could not elaborate; it now gets none. A field of the standard Bytes type is written as the empty octet list, since the audit refuses an instance at the Subtype Bytes is; - the synthesized BranchPath parameter was named path even when the body bound path itself, so effect calls under that binding received a String; the name now avoids body bindings and pattern binders too; - a user function named sizeOf captured the bare sizeOf of a termination measure in its namespace; measures then use SizeOf.sizeOf. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Brings in #1422 to #1425: proof export fixes, the removal of the Dafny backend, and the process layer fixes. The certificate model prelude in the wall (ModelPrelude) takes main's new AverBits mask lemmas byte for byte, so the wall identity rotates. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The wall's decoders read a section as one numeral and a length, a byte at a time, and every byte read shifts the rest of the section. The kernel keeps each of those numerals until the declaration is checked, so a section of S bytes costs memory quadratic in S: the export accounting of btc-listener (740 KB, 3701 exports) ran past a 16 GB heap, and the String helper roles ran for over fifty minutes. A package now declares the byte length of every entry of the type, export and code sections. ByteWindow cuts a section at those lengths and decodes each entry on its own window; Ext lemmas show every entry reader returns on its window what it returns inside the section. One declaration per section checks that every window decodes and fills its window exactly, and proves the section's decoder equal to a lazy reading of the windows, which decodes an entry only when a check reads it. A wrong length declines the package. SortedKeys decides the export accounting and the closure isolation with merge sorts and walks over sorted numeric keys instead of balanced trees, whose insertions cost the kernel thousands of steps each, and proves that what it decides implies the tree-based checks. The export names' distinctness is read from the accounting instead of decided again. The checker's report pins over every plan (facets, policies, termination witnesses) are decided by the kernel under a raised elaboration budget. What is accepted is unchanged: the acceptance statement still reads the decoders. Two hardening tests move one byte between two export entries and between two code entries, and the package is declined. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The certificate's source model emitted verify blocks in source order, so a law whose `using` citation sat lower in the same file had no theorem to cite and fell to its sorry floor. `aver proof` already orders the blocks with `order_verify_blocks_for_citation`; the certify path now runs the same pass. On btc-listener this credits 39 more law-claims (70 to 109 of 119). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A step lemma used to run one search under a 1M-heartbeat cap: the default simp set over the whole plan with every String literal of the package, then `repeat' split` and `simp_all`. A miss cost the full budget (250 s for one 13-arm Int match on btc-listener, 466 s for one slice on payment_ops), and a timeout escaped `first` and dropped the lemma. The step script is now fixed by the plan. `BridgeDefs.lean` carries a small block of lemmas: a match taken arm by arm per pattern kind, a plan `if` and `withDefault` as Lean functions of their subject, `ite_eq_of` to split an `if` without naming its condition, and the normal forms the source spells (`==`, `!=`, String `+` and interpolation). Each step evaluates its plan with `simp only` over an exact list (its own String literals read back whole), splits the plan's ifs, and closes each leaf against the source unfolded once, with the nullary constants its body names; a self-recursive source unfolds on the right only. The cap is 400k. Export theorems split every argument in every goal (`<;>` instead of `;`) and close the image by `rfl` per conjunct after `simp`. btc-listener: source-bridges 416 to 494 of 494, bridged laws 8 to 16 of 17, step slices about 650 s to 87 s. payment_ops: bridges 51 to 59 of 59, proof build 718 s to 145 s. k5 unchanged at 11 of 11 laws and 12 of 12 bridges. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…names Lean resolves a dotted identifier to the longest prefix that is a declared constant, so a report pin written as `_root_.AverCert.manifest.subject.contracts` meant a package constant `AverCert.manifest.subject` (or the whole path) when the package declared one. A package could then print a false L3 level, hide runtime contracts, or tie laws and bridges to a manifest of its choosing through `AverCert.Artifact.data.manifest`, with the accepted bytes unchanged. The witness now names only the package constants `AverCert.manifest` and `AverCert.Artifact.data` in full and reads every field through the wall structures' projection functions, which live in wall namespaces the audit closes to packages. The audit also admits under `AverCert` only the exact producer shapes (`manifest`, `subject`, and names inside `Plans`, `Artifact`, `Final`, `Bridge`, `Laws`), and refuses a package constant there whose name extends another declared constant, Lean's own auxiliaries excepted. The producer writes the pieces of long subject lists as `AverCert.Plans.subject_<field>_<k>` so none extends `AverCert.subject`. The token gate now also refuses `open _root_.Lean`. New hardening tests forge the report behind shadowed constants (refused by the pins) or declare them with an honest report (refused by the audit), lie in the declared layout (type cut, code offset and length, type index, function type, export position), hide a closure helper, widen the divmod helper's type to a supertype, rename the work import, and make a certified closure reach a work import. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… chose The witness elaborated each law statement inside `namespace <prefix>`, where the prefix is the manifest's `theorem` minus its last segment. Lean resolves a name in the innermost enclosing namespace first, so a package constant `Evil.Tiny.addTwo` (theorem `Evil.law`) or `Tiny.Tiny.addTwo` made the statement text `Tiny.addTwo` mean the slipped-in function. A law-claim was then credited, and bridged through the real function's bridge, for a property the real function need not have. - The witness and the package's `Laws.lean` read every law statement at the root. The producer rewrites each statement the emitter wrote for its theorem's namespace so every model name is `_root_.`-qualified (`root_qualify_statement`), resolving names against the model's declarations the way Lean does inside that namespace. - A law that lists bridges must name each bridged model exactly as `_root_.<model>`; the bridge list is matched on that spelling only. - The audit refuses a package constant `Q.M` for any namespace prefix `Q` of a law's namespace and any model `M` a law names, and a bridged law whose elaborated statement does not use every bridged model constant. - The audit exempts a reserved name only beside a constant the package does not declare; beside a package constant only internal, numbered and unfolding auxiliaries are exempt, since a package can declare `V.h.eq_1` before `V.h`. - The text gate refuses `namespace Lean` and `namespace Lake`, as it refuses `open` of them. The Tiny laws now also carry bridged corollaries, because their bare function names become `_root_.Tiny.*` mentions. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…en in statements The witness reads every law statement at the root, and a bridged model must be spelled `_root_.M`, which resolves to exactly the root constant. A package constant where a law's namespace would resolve a mentioned model is therefore harmless, and the audit rule that refused one (`lawShadows`) is removed. It was also too broad: it refused the whole package for any program with modules `Foo.Tiny` and `Tiny` once a law in `Foo` existed and a law named `_root_.Tiny.addTwo`. The check that each bridged law's elaborated statement uses every bridged model stays. - The statement gate refuses `set_option` and `open` as a segment of any identifier token outside literals. A term-level `set_option ... in` bypassed the package gate's option whitelist; the producer writes neither word. - The shadow tests now show the shadow is harmless: beside the honest statement the law is credited, and a statement only the shadow makes true does not bind. A new test accepts an honest program with `Foo.Tiny.addTwo` beside `Tiny.addTwo`. - The docs describe the audit's law step and the gate as they are now, and list the free values of model `BEq`/`Inhabited` instances as an open item. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
jasisz
marked this pull request as ready for review
September 25, 2026 16:02
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Work in progress. Not ready for review.
The certificate wall used to admit a function only if the whole function fit one of eleven plan families. This branch replaces the families with one plan grammar: the plan is the optimized MIR function the wasm-gc emitter consumed, printed one to one. The wall lowers it the way the emitter does and pins the result against the module bytes, as before. One simulation theorem covers every node, and one fuel induction covers self and mutual calls.
Decisions on this branch:
Numbers so far (local runs,
aver-cert check):wildnow proved total).Still to do before this can merge:
Int.div/Int.mod,Result<_, String>and a few smaller constructs (in progress).--certifymust not change a single byte of the build.aver:work/v1.submitimport.