cert: one plan grammar built from MIR instead of plan families

.github/cert-lanes.json

@@ -96,26 +96,36 @@
     "mode": "cargo",
     "smoke": true
   },
+  {
+    "suite": "cert_hardening_spec",
+    "lane": "",
+    "mode": "cargo",
+    "features": "wasm,wasip2",
+    "smoke": true
+  },
   {
     "suite": "cert_whole_module_guard_iso",
     "lane": "guard-iso-1/3",
     "mode": "nextest",
     "filter": "all()",
-    "partition": "1/3"
+    "partition": "1/3",
+    "smoke": true
   },
   {
     "suite": "cert_whole_module_guard_iso",
     "lane": "guard-iso-2/3",
     "mode": "nextest",
     "filter": "all()",
-    "partition": "2/3"
+    "partition": "2/3",
+    "smoke": true
   },
   {
     "suite": "cert_whole_module_guard_iso",
     "lane": "guard-iso-3/3",
     "mode": "nextest",
     "filter": "all()",
-    "partition": "3/3"
+    "partition": "3/3",
+    "smoke": true
   },
   {
     "suite": "cert_verify_spec",

.github/workflows/cert.yml

@@ -63,6 +63,17 @@ jobs:
                   bad.append(f"{suite} {family}: expected 1..{n}, got {sorted(seen)}")
           if not any(lane.get('smoke') for lane in lanes):
               bad.append("no lane is marked smoke — every pull request would run nothing")
+          # Every certificate suite runs here, where Lean is installed. A suite
+          # without a lane would run only in ci.yml, whose runners have no
+          # `lake`, and its Lean-backed tests would skip there without a word.
+          # The one exception carries no Lean test.
+          import glob, os
+          no_lean = {'cert_delegate_spec', 'cert_one_build_spec'}  # no Lean: byte identity runs in ci.yml's wasm-gc lane
+          laned = {lane['suite'] for lane in lanes}
+          for path in sorted(glob.glob('tests/cert_*.rs')):
+              suite = os.path.splitext(os.path.basename(path))[0]
+              if suite not in laned and suite not in no_lean:
+                  bad.append(f"{suite} has no lane in .github/cert-lanes.json")
           if bad:
               print("\n".join(bad)); sys.exit(1)
           print(f"{len(lanes)} lanes, {len(groups)} partitioned families, all complete")
@@ -75,8 +86,9 @@ jobs:
         run: |
           set -euo pipefail
 
-          # A pull request runs the smoke lanes only: the five cheapest that
-          # still reach all four suites, about five minutes of wall clock. They
+          # A pull request runs the smoke lanes only: the cheap ones that
+          # still reach every suite, plus the hardening tampers and the
+          # guard-isolation lanes, whose failures are soundness regressions. They
           # are marked in .github/cert-lanes.json rather than listed here, so
           # the full set stays the single source and a lane cannot be dropped
           # from one place and kept in the other.
@@ -146,6 +158,9 @@ jobs:
       CARGO_BUILD_JOBS: '2'
       CARGO_INCREMENTAL: '0'
       RUSTFLAGS: -C debuginfo=0
+      # Lean is installed on these runners, so a certificate test that finds
+      # no `lake` fails instead of skipping.
+      AVER_CERT_REQUIRE_LEAN: '1'
     steps:
       - uses: actions/checkout@v5
 
@@ -233,7 +248,7 @@ jobs:
 
       - name: Run certification suite
         if: matrix.mode == 'cargo'
-        run: cargo test -p aver-lang --features wasm --test ${{ matrix.suite }}
+        run: cargo test -p aver-lang --features ${{ matrix.features || 'wasm' }} --test ${{ matrix.suite }}
 
       - name: Run certification suite lane
         # Filtering happens before slice partitioning. Each family filter (one
@@ -248,6 +263,6 @@ jobs:
         env:
           AVER_CERT_PHASE_TIMEOUT_SECS: ${{ matrix.phase_timeout_secs || 900 }}
         run: >-
-          cargo nextest run -p aver-lang --features wasm --test ${{ matrix.suite }}
+          cargo nextest run -p aver-lang --features ${{ matrix.features || 'wasm' }} --test ${{ matrix.suite }}
           -E '${{ matrix.filter }}'
           --partition slice:${{ matrix.partition }}

.github/workflows/ci.yml

@@ -105,7 +105,9 @@ jobs:
           - name: aver-lang unit and docs
             command: cargo test -p aver-lang --lib --bins && cargo test -p aver-lang --doc
           - name: workspace crates
-            command: cargo test --workspace --exclude aver-lang
+            # The workspace test builds aver-cert with its default `verify`
+            # feature only; the producer's unit tests need `engine` as well.
+            command: cargo test --workspace --exclude aver-lang && cargo test -p aver-cert --lib --all-features
           - name: integrations 1/4
             command: python3 tools/ci_test_shard.py 0 4
           - name: integrations 2/4
@@ -263,6 +265,20 @@ jobs:
         if: matrix.lane == 'checks'
         run: cargo test -p aver-lang --features wasm,wasip2 --test provider_spec --test capability_grammar_spec --test capability_target_manifest_spec
 
+      - name: Certificate coupling ratchet
+        if: matrix.lane == 'checks'
+        # An emitter or MIR change that makes a certified function decline must
+        # fail the PR that makes it, not the next Lean run. `--certify` writes
+        # the package without building it, so this needs no Lean: it compiles
+        # the certificate corpus and compares the certified exports, bridges
+        # and law-claims per program with tools/cert-baseline.json. A gain is
+        # recorded in the same commit with `python3 tools/cert_ratchet.py
+        # --update`. The binary is the one the canaries above just linked.
+        timeout-minutes: 10
+        run: |
+          cargo build -p aver-lang --bin aver --features wasm,wasip2
+          python3 tools/cert_ratchet.py --aver target/debug/aver
+
       - name: Install Node for the JavaScript Work host
         if: matrix.lane == 'wasm-gc'
         uses: actions/setup-node@v4
@@ -303,6 +319,7 @@ jobs:
             bigint_literals_differential \
             cert_certify_spec \
             cert_decode_spec \
+            cert_one_build_spec \
             cert_verify_spec \
             cross_backend_proptest \
             cross_backend_stress \

AGENTS.md

@@ -46,7 +46,7 @@ Below: implementation details relevant to development only.
 - **Opaque types** (`exposes opaque [T]`): module-level access control for types. An opaque type is visible in signatures (can be passed, returned, stored) but cannot be constructed, have its fields accessed, or be pattern-matched from outside the defining module. Enforced at compile time in the typechecker; `load_module_sigs` registers a dummy sig (type resolves) but omits field types, constructors, and variant info. Parser recognizes `exposes opaque` after the `Exposes` token by checking for `Ident("opaque")`.
 - **Provider-backed standard capabilities** (`stdlib/capabilities/`): `Args`, `Console`, `Disk`, `Env`, `Http`, `Process`, `Random`, `Tcp`, `Terminal`, and `Time` own their operation signatures, Oracle/replay declarations, hostile profiles, and represented boundary types in Aver source. VM and generated Rust bind exact-contract native providers through `src/provider/standard.rs`; their native adapters live in `aver-rt/src/provider/`. `Process.stopRequested` is a monotonic cooperative SIGINT/SIGTERM flag; wasm-gc supplies it as a host import and wasip2 rejects it because WASI 0.2 has no signal binding. Disk includes byte-exact whole-file, positional, write, and append methods plus metadata `size`; `readBytesAt` returns at most the requested length and treats EOF as a successful short read, and `sync` forces one path's bytes and metadata to stable storage — a file or a directory, because a file's own fsync does not make its directory entry durable. `Http.Response` and `Terminal.Size` are represented capability-owned records; `Tcp.Connection` is a provider-owned capability resource, not a surface record or an `exposes opaque` type. wasm-gc and wasip2 register supported host/WASI lowerings as bindings of the same contracts, with operation-level target availability where only part of a capability is supported. Standard capability operations are not legacy service builtins.
 - **WASM-GC backend** (`src/codegen/wasm_gc/`, feature-gated behind `--features wasm`): compiles Aver to wasm modules using the WebAssembly GC + tail-call proposals (typed structs/arrays, no linear-memory heap for first-class values). Two emission modes share the lowering pipeline: (a) `--target wasm-gc` for browsers / Workers / JS hosts via the `aver/*` standard host ABI plus contract-derived `aver:user/cap-…` imports for program-defined capabilities; (b) `--target wasip2` (and `aver run --wasip2`) for the WASI 0.2 / Component Model story — the same backend emits canonical-ABI WIT imports (`wasi:cli/stdout`, `wasi:filesystem/preopens`, `wasi:io/streams`, ...) and `src/codegen/wasip2/wrap.rs` wraps the core module via `wit-component`, no preview-1 adapter. Custom raw wasm-gc imports use native GC values, `externref` resources, full `Int = ℤ`, and generated `__cap_abi_*` factory/accessor exports; see [docs/wasm-gc-custom-capabilities.md](docs/wasm-gc-custom-capabilities.md). Effect set on wasip2: Console, Time, Random, Args, Env (read), all Disk, all `Http.*` verbs, the connected half of `Tcp` (`connect`, `close`, `writeLine`, `writeBytes`, `writeNow`, `readLine`, `readBytes`, `readSome`, `readNow`, `poll`, `send`, `sendBytes`, `ping`), and the reserved job contracts `Wait.poll` and `Work.cancel`; `Terminal.*`, `Env.set`, `Process.*`, and the seven `Tcp` dial/listener operations are compile-rejected. Job kinds on wasm-gc use the versioned `aver:work/v1` ABI: the native runner and Wasmtime packs schedule isolated worker instances over shared compiled code, and `tools/wasm-work` supplies a JavaScript Worker adapter. Task/result transport uses owned values and generated capability helpers; generated coordinators expose a post-wait step so JS can receive worker messages between turns. WASI 0.2 retains inline `begin`. See [docs/wasm-work.md](docs/wasm-work.md); lowering is in `src/codegen/wasm_gc/jobs.rs`, native scheduling in `src/runtime/wasm_gc/host_work/`. Incoming HTTP is an explicit `--handler <fn>` export in fetch/proxy worlds, while native programs use the Aver `HttpServer` module over `Tcp` (see [docs/wasip2.md](docs/wasip2.md)). The legacy linear-memory `--target wasm` backend was deleted in 0.18 Phase 1.8, and its `abi.rs` import table with it. Standard host imports are enumerated by `EffectName` in `src/codegen/wasm_gc/effects.rs` and mirrored in `aver-cert/src/format.rs`; custom imports are admitted by the exact hashed namespace grammar in both Rust and the Lean wall.
-- **Artifact certificates** (`aver-cert/`): `aver-cert` 0.1.x is an independently versioned verifier/process; `aver cert` is an exact subprocess shortcut. Public package version is `1` (`FORMAT_VERSION`) and manifest schema version is `8` (`CERT_SCHEMA_VERSION`): schema 2 made the subject `hostRoleTable` optional — `null` for modules without the Int box helper, pinned against a byte-derived proof of the helper's absence; schema 3 added the required `toIndex` key to the object form; schema 4 added the required `cmp` and `eq` keys; schema 5 added the required top-level `target` field; schema 6 added the wasip2 component-envelope byte binding; schema 7 added the required top-level `laws` array — the law-claims surface whose `Laws.lean` corollaries the checker-owned witness re-elaborates and axiom-audits; schema 8 added the required top-level `sourceBridges` array and the `bridges` key on every law entry — the plan-equals-source surface, one kernel-checked theorem per compute-face export identifying the plan its obligation evaluates with the transpiled source function. A bridge entry transports STRUCTURE (export, model, and one closed-form encoder per parameter and result); the checker renders the pinned statement from it with `aver-cert/src/bridge_statement.rs`, the same renderer the producer writes `Bridge.lean` with, so no statement text the package writes is ever read as a claim. A law-claim listing bridges carries a second `_bridged` corollary conjoining them, pinned and audited apart from the law's own. `Plans.lean` is the sole authoritative plan data, while the verifier supplies the actual artifact bytes, Lean 4.34 wall, build, and witness. See [docs/certification.md](docs/certification.md) and [docs/certification-architecture.md](docs/certification-architecture.md).
+- **Artifact certificates** (`aver-cert/`): `aver-cert` 0.1.x is an independently versioned verifier/process; `aver cert` is an exact subprocess shortcut. Public package version is `1` (`FORMAT_VERSION`) and manifest schema version is `9` (`CERT_SCHEMA_VERSION`): schema 2 made the subject `hostRoleTable` optional — `null` for modules without the Int box helper, pinned against a byte-derived proof of the helper's absence; schema 3 added the required `toIndex` key to the object form; schema 4 added the required `cmp` and `eq` keys; schema 5 added the required top-level `target` field; schema 6 added the wasip2 component-envelope byte binding; schema 7 added the required top-level `laws` array — the law-claims surface whose `Laws.lean` corollaries the checker-owned witness re-elaborates and axiom-audits; schema 8 added the required top-level `sourceBridges` array and the `bridges` key on every law entry — the plan-equals-source surface, one kernel-checked theorem per compute-face export identifying the plan its obligation evaluates with the transpiled source function. A bridge entry transports STRUCTURE (export, model, and one closed-form encoder per parameter and result); the checker renders the pinned statement from it with `aver-cert/src/bridge_statement.rs`, the same renderer the producer writes `Bridge.lean` with, so no statement text the package writes is ever read as a claim. A law-claim listing bridges carries a second `_bridged` corollary conjoining them, pinned and audited apart from the law's own; the list must be exactly the bridges of the functions its statement names. Schema 9 states every obligation over one plan grammar (the optimized MIR printed 1:1), and a bridge statement is an application of the wall's `GrammarBridge.Exact`/`Adequate` with `nat_lit` numerals. The checker's witness is pure `_root_`-qualified pins; a separate checker-authored audit program, elaborated without the package, audits axioms, package instances, parser extensions and bridge encoder shapes; the final `leanchecker --fresh` replays the witness and its whole import closure; the package text gate (`aver-cert/src/lean_gate.rs`) is token-based and admits only listed `set_option`s. `Plans.lean` is the sole authoritative plan data, while the verifier supplies the actual artifact bytes, Lean 4.34 wall, build, and witness. See [docs/certification.md](docs/certification.md) and [docs/certification-architecture.md](docs/certification-architecture.md).
 - **Independent products** (`?!` / `!`): a tuple followed by `!` is a product of independent computations; `?!` adds Result unwrapping. `Expr::IndependentProduct(Vec<Spanned<Expr>>, bool)` in AST. Parser detects `?` + `!` or bare `!` after tuple in `parse_postfix`. Typechecker: `?!` verifies all elements are `Result<T, E>` with compatible error types and that elements are function calls; `!` infers as regular tuple. Interpreter: sequential evaluation with replay groups. Codegen: `std::thread::scope` with real parallelism. VM: `CALL_PAR` dispatches callable values plus per-branch arity, so aliases like `f = foo; (f(x), f(y))!` work. Replay: effects within a product share `group_id`, matched by `branch_path + effect_occurrence + effect_type + effect_args`, not execution order. See [docs/independence.md](docs/independence.md).
 
 ### Design omissions

CHANGELOG.md

@@ -104,6 +104,10 @@ The generated loop is now written from the program's source alone, and the manif
 - **A call inside a `!` or `?!` branch is numbered from zero, whatever the surrounding body has already charged.** A branch is its own numbering scope in a run: every operation gets a fresh slot each time the branch is entered. A body threading the `Process.stopRequested` base used to carry that base into its branches, so a poll inside an independent product was exported at the loop's turn count while the run charged it 0 on every turn, and from the second turn on the exported model computed a different function from the one the run computes. The branch now numbers its own calls and a law over such a loop keeps a theorem about the run.
 
 ### Changed
+- **`aver-cert check` scales to large modules.** The checker used to decode the type, export and code sections one byte at a time, and the kernel kept a copy of the rest of the section for every byte, so a 740 KB module ran out of memory at the export accounting and spent over fifty minutes on the String helper roles. A package now declares the byte length of every entry of those three sections; the checker decodes each entry on its own and requires it to fill its declared length exactly, so a wrong length declines the package. The export accounting and the certified-closure check sort their keys instead of indexing them in balanced trees. What a certificate proves is unchanged, and certificates produced by earlier versions name a different wall and must be produced again.
+
+- **`aver-cert verify` builds without caches, and the verifier writes `Module.lean` itself.** `verify` now ignores `AVER_CERT_DATA_CACHE` and `AVER_CERT_PRELUDE_CACHE` and prints a notice; only `check` uses them. A certificate package no longer carries `Module.lean`: the verifier renders the artifact hash into it from the bytes it reads, and ignores a package file of that name. Packages declaring names inside the verifier's own Lean namespaces are declined. Certificates produced by earlier versions name a different wall and must be produced again.
+
 - **Five kinds of law that used to stay open, or break the Lean build, now prove.** A law whose `given` ranges over a refinement record no longer fails the exported project, which used to cost every other law in the file its tier: each sample is substituted into the proof instead of case-split, a sample carries its type where it meets a `when`, the sampled-domain proof sits under a `sorry` floor, and a module called `Min` or `Max` no longer clashes with a core Lean name in the lakefile. A law over a sum type whose variant carries a payload is split by constructor before the closers run. A law that divides by a variable, such as `n * quot(a, n) + rem(a, n) => a` or `0 <= rem(a, n) < n` under `n >= 1`, now cites the quotient-remainder facts of Lean's `Int` division, which is Euclidean like Aver's `Int.div` and `Int.mod`. A list induction whose step needs the subject's own `if` split before anything else is simplified (`count(y, insert(x, xs))`) keeps its induction hypothesis. A cited law about a non-recursive helper (`ok(push(x, xs))` under `ok(xs)`) is applied before that helper is unfolded. Each new step is tried after the ones that were there before, so a law that already proved keeps its proof.
 
 - **A law whose claim reveals a helper that matches on a name closes again.** The alternative that reveals every outer helper at once and then lets the solver saturate was also offered when a revealed body still held a match the goal had not resolved, and on a large corpus that is a deterministic timeout, which stops the whole export rather than falling through to the alternatives that open one computation at a time. It is no longer offered on that shape. Measured on an external corpus of a hundred and twenty laws: all of them close, where one of them had stopped closing.

Cargo.toml

@@ -154,3 +154,9 @@ required-features = ["wasm"]
 [profile.release]
 lto = true
 codegen-units = 1
+
+# The certificate checker hashes its build caches (hundreds of MiB of `.olean`
+# files) with SHA-256; unoptimised, that hashing alone costs seconds per check
+# in the debug builds the developer loop and the test suites use.
+[profile.dev.package.sha2]
+opt-level = 3