Prove specs over every input: state graphs, symbolic evaluation, a certifying solver - #8

Merged

yogthos merged 9 commits into

mainfrom

proofs-over-every-input

Sep 24, 2026

Commits on Sep 23, 2026

writ.solve: clauses of linear literals, and a certificate checker
Yogthos
committed
465fe56
writ.solve: simplex with Farkas certificates, and DPLL over it
Yogthos
committed
66347c0
writ.solve: check, valid?, verify and eval-formula
Yogthos
committed
5a37696
Merge branch 'worktree-agent-a124a82be48021f79'
Yogthos
committed
a5cb358

Commits on Sep 24, 2026

writ.solve: incremental simplex, and propagation by occurrence
Yogthos
committed
31ffa92
Prove over every input: state graphs, symbolic evaluation, proof namespace
Yogthos
committed
f2d1f70
examples: specs as state graphs, proved end to end
Yogthos
committed
7dc17bd
Document graphs, refinements, the solver and the proof namespace
Yogthos
committed
cac6628
writ.spec: look harder for a rare refinement's values
Yogthos
committed
6af2cd8