WIP: Jcb/formalization2 - #4

Open

johnchandlerburnham wants to merge 23 commits into

devfrom

jcb/formalization2

Commits on Aug 9, 2026

verify: drop spurious noncomputable markers on singleton replay rows
johnchandlerburnham
committed
c0b04d7
inductive: compute of_run by replaying the transparent decomposition
johnchandlerburnham
committed
48b9980
verify: compute staged ofRun packagers by replaying their builders
johnchandlerburnham
committed
731d0f9
verify: drop noncomputable markers freed by computable staged owners
johnchandlerburnham
committed
ff5ffc7
verify: add trExprS?, the deterministic shadow of strict translation
johnchandlerburnham
committed
ffe2cd4
verify: compute the generation packages through the deterministic translator
johnchandlerburnham
committed
ea73301

Commits on Aug 10, 2026

Commits on Aug 11, 2026