cert: one plan grammar built from MIR instead of plan families - #1412

Merged

jasisz merged 96 commits into

mainfrom

cert/one-grammar

Sep 25, 2026

Commits on Sep 22, 2026

Emit every function through the MIR body emitter

jasisz
and
claude
committed
98e6dc0
cert wall: add i64.ne, i32.eqz, i32.ne and i32.or to the interpreter

jasisz
and
claude
committed
dfb99c6
cert wall: add the one-grammar plan, its lowering and the simulation theorem

jasisz
and
claude
committed
3d7ffca
cert wall: rotate the wall id for the interpreter additions

jasisz
and
claude
committed
8e78c9e
cert wall: add Match and Construct to the one-grammar plan

jasisz
and
claude
committed
39c23b3
cert wall: pin the constructor struct finality the exact ref.test needs

jasisz
and
claude
committed
c043e3f
cert wall: add String, Float, Vector, List and tuple nodes to the one-grammar plan

jasisz
and
claude
committed
e3c94f8
cert wall: pin string literal bytes to their data segments

jasisz
and
claude
committed
220b7c0

Commits on Sep 23, 2026

cert wall: add totality (L3) for the one-grammar plan

jasisz
and
claude
committed
d57d21a
cert wall: admit literal multipliers in the one-grammar totality check

jasisz
and
claude
committed
47715f0
cert wall: rebuild the acceptance on the one grammar (statement schema 9)

jasisz
and
claude
committed
3c4ff02
cert: embed the schema-9 wall and rotate the wall id

jasisz
and
claude
committed
15a2fbd
cert wall: pin the Int equality helper by its template only

jasisz
and
claude
committed
8a42ace
cert: produce schema-9 packages from the printed MIR plans

jasisz
and
claude
committed
d65e1dc
cert: delete the family producer

jasisz
and
claude
committed
182c8d2
cert: name the intrinsic and the newtype record in printer declines

jasisz
and
claude
committed
d94f2f1
cert: prove the whole-module facts one by one in the package

jasisz
and
claude
committed
ebf2834
cert lint: bind the plan only through its code-entry equality

jasisz
and
claude
committed
7004f41
cert wall: decline declarations that make an obligation vacuous

jasisz
and
claude
committed
09c5d23
cert docs: disclose the helper model, the unpinned sub-routines and L3 limits

jasisz
and
claude
committed
cd7999e
Lean proof export: decline the lift of a generic-oracle effect instead of panicking

jasisz
and
claude
committed
35fcda4
cert wall: add GrammarBridge, the plan-equals-source statement kinds and proof engines

jasisz
and
claude
committed
f709d7b
Lean certificate model: keep the native recursion equations

jasisz
and
claude
committed
cc6d579
cert: plan-equals-source bridges and law-claims on schema 9

jasisz
and
claude
committed
e660783
cert: close hypothesis-side branches in bridge step proofs

jasisz
and
claude
committed
f67fbe1
cert: one lexical gate for the producer and the checker

jasisz
and
claude
committed
999d246
cert model: take the refused prelude pieces from the wall, keep safe deriving

jasisz
and
claude
committed
6dbd2ed
cert: ship the model nested, isolate each theorem, self-check before shipping

jasisz
and
claude
committed
b8653a2
cert model: a when-guarded law over Bool connectives exports universally

jasisz
and
claude
committed
7c1b74e
cert: admit a keyword-escape prime anywhere after a segment's first letter

jasisz
and
claude
committed
a75c8b1
cert: build the bridge proofs apart from the byte-level proof

jasisz
and
claude
committed
c4bf53d
cert: admit Euclidean Int.div and Int.mod through a pinned divmod helper

jasisz
and
claude
committed
de12964
cert: give String, Float, List and Vector their default fillers

jasisz
and
claude
committed
1899f8d
cert: give a record or sum one type id under every spelling of its name

jasisz
and
claude
committed
8bbdd77
cert: find the sub and mul helpers past a raw-i64 user function

jasisz
and
claude
committed
0d030e7
Lean certificate model: hand law statements over with constructor applications

jasisz
and
claude
committed
82efc03
cert: check the plans of a package in chunks

jasisz
and
claude
committed
fc53078
cert: attempt no source bridge for a plan of more than 100 nodes

jasisz
and
claude
committed
354d126
cert: build the bridge step lemmas in parallel slices

jasisz
and
claude
committed
1b2fe26
cert: rewrite bridge step proofs with one image lemma per function

jasisz
and
claude
committed
93ab5a2
Revert "cert: attempt no source bridge for a plan of more than 100 nodes"

jasisz
and
claude
committed
b2f9716
cert: attempt no source bridge for a plan of more than 100 nodes

jasisz
and
claude
committed
9275b7e
build: optimise sha2 in debug builds

jasisz
and
claude
committed
fdffcfc
cert: report Lean step times on request

jasisz
and
claude
committed
475bdc2
cert: render artifact bytes as chunked numerals

jasisz
and
claude
committed
56e7e69
cert: prove agreement by induction on the term size

jasisz
and
claude
committed
da1a106
cert: select a bridge's obligation without deciding String equality

jasisz
and
claude
committed
9ac921c
cert: account exports on numeric name keys

jasisz
and
claude
committed
7d0edcd
cert: keep byte numerals out of the compiler; check 32 plans per declaration

jasisz
and
claude
committed
18ff69e
cert: prove the witness's report pins by reduction first

jasisz
and
claude
committed
5354972
cert: spread a large package's byte facts over modules

jasisz
and
claude
committed
159ee0f

Commits on Sep 24, 2026

cert: read plan facts from a declared module layout

jasisz
and
claude
committed
ac7e9d6
cert: classify String helper roles through a signature-shape bitmap

jasisz
and
claude
committed
5efe5f5
cert: reuse unchanged modules from the data cache

jasisz
and
claude
committed
ef4e925
Fix two stale sentences in the language guide and the playground

jasisz
and
claude
committed
048f36f
cert docs: rewrite the format specification for statement schema 9

jasisz
and
claude
committed
4180141
cert docs: describe the schema-9 architecture

jasisz
and
claude
committed
a318b43
cert docs: update the user guide for statement schema 9

jasisz
and
claude
committed
0f8b071
cert: read declared capability and helper names as characters

jasisz
and
claude
committed
9e938fb
cert tests: port the decoder differential to the one plan grammar

jasisz
and
claude
committed
d9a4fb7
cert tests: rebuild the guard-isolation suite on the one-grammar wall

jasisz
and
claude
committed
d6d433d
cert: tokenize the package text gate and admit only listed options

jasisz
and
claude
committed
9619d57
cert: pin witness names from the root and audit the package outside it

jasisz
and
claude
committed
34c8c8f
cert: tamper tests for the package trust boundary

jasisz
and
claude
committed
fb2c38a
Merge the certificate checker hardening into the one-grammar branch

jasisz
and
claude
committed
9f31cc1
cert wall: pin the divmod helper type in the layout reading as well

jasisz
and
claude
committed
133ba74
cert tests: port the verify suite's tampers to the one-grammar package

jasisz
and
claude
committed
5c734c6
cert tests: port the certify suite to schema 9 and the one plan class

jasisz
and
claude
committed
87c0d0d
Merge the ported certificate integration suites into the one-grammar branch

jasisz
and
claude
committed
5ad97cd
Merge the rewritten certification docs into the one-grammar branch

jasisz
and
claude
committed
41f43aa
cert: keep the producer test modules under the crate's own fixtures

jasisz
and
claude
committed
1f4b89b
cert: state the canonical Int input domain in explain

jasisz
and
claude
committed
bfdc822
cert: drop the unused wall-owned lint category

jasisz
and
claude
committed
594ede1
Merge remote-tracking branch 'origin/main' into cert/one-grammar
jasisz
committed
b953575
cert: bring tests, fixtures and lints in line with the current package shape

jasisz
and
claude
committed
5aa4a88
cert: keep package modules out of the wall and statement text out of pin shapes

jasisz
and
claude
committed
4f17f67
cert: make verify ignore build caches and document the checker-owned Module

jasisz
and
claude
committed
4f5df00
ci: run every Lean-backed certificate suite where Lean is installed

jasisz
and
claude
committed
6c6db98
cert: ship the source model of payment_ops again and admit its own classes

jasisz
and
claude
committed
003580b
ci: hold certified exports, bridges and law-claims with a ratchet

jasisz
and
claude
committed
2494561
cert: refit the Lean-backed tests to the rooted wall names and the checker-owned Module

jasisz
and
claude
committed
45d9c9b
compile: make --certify write the same module as a plain build

jasisz
and
claude
committed
ca90cb6
cert: admit the aver:work/v1 job imports on wasm-gc

jasisz
and
claude
committed
2c62f18
ci: exempt the one-build suite from cert lanes; it runs no Lean

jasisz
and
claude
committed
922b43e
cert: write big type tables and subject lists in pieces

jasisz
and
claude
committed
d04d451
lean: fix four ways the certificate model of an effectful project fails

jasisz
and
claude
committed
c83a056

Commits on Sep 25, 2026

Merge origin/main into cert/one-grammar

jasisz
and
claude
committed
06546cc
cert: decode the big sections one declared entry at a time

jasisz
and
claude
committed
6fd0771
Merge origin/main into cert/one-grammar
jasisz
committed
3f94dda
cert: order the model's laws for citation as aver proof does

jasisz
and
claude
committed
1c547f5
cert: prove bridge step lemmas by construction

jasisz
and
claude
committed
655ef42
tests: refresh the certificate package snapshots for the current wall

jasisz
and
claude
committed
d155318
Merge remote-tracking branch 'origin/main' into tmp-certmain
jasisz
committed
14546d4
cert: read report pins through wall projections and refuse extending names

jasisz
and
claude
committed
dd37b59
cert: read law statements at the root, not in a namespace the package chose

jasisz
and
claude
committed
6591800
cert: drop the law-namespace shadow rule and refuse set_option and open in statements

jasisz
and
claude
committed
bfe70f4