When proving row-structured circuits (per-row hypotheses extracted from folds/mapFinRange over vectors of cells), each proof currently needs a hand-tuned interleaving of index normalization (norm_num), simp passes, and targeted rws — and the working order is discovered by trial and error. Two concrete failure shapes:
- rewriting cell equations before
norm_num works when the lemma instance spelling (v[0+1]) matches the raw hypothesis, and breaks after normalization folds the index to v[1] — and vice versa;
rw-by-cell-equation routes can trigger explosive casesOn motive checks that a fused pass avoids.
The fused pass that made the Orchard double-and-add tractable:
simp only [Vector.get, Vector.getElem_ofFn, Fin.val_mk]
<case split on the row index>
norm_num [Vector.getElem_append, Vector.getElem_mapRange]
A dedicated circuit_row_norm-style tactic that collapses vector/index/ite atoms of an extracted per-row hypothesis in one canonical pass would remove a whole class of iteration from row-structured circuit proofs.
(Extracted from the retired doc/circuit-proof-friction.md feedback list. Related, already tracked separately: #407 on the loop combinators' differing contracts.)
🤖 Generated with Claude Code
When proving row-structured circuits (per-row hypotheses extracted from folds/mapFinRange over vectors of cells), each proof currently needs a hand-tuned interleaving of index normalization (
norm_num), simp passes, and targetedrws — and the working order is discovered by trial and error. Two concrete failure shapes:norm_numworks when the lemma instance spelling (v[0+1]) matches the raw hypothesis, and breaks after normalization folds the index tov[1]— and vice versa;rw-by-cell-equation routes can trigger explosivecasesOnmotive checks that a fused pass avoids.The fused pass that made the Orchard double-and-add tractable:
A dedicated
circuit_row_norm-style tactic that collapses vector/index/ite atoms of an extracted per-row hypothesis in one canonical pass would remove a whole class of iteration from row-structured circuit proofs.(Extracted from the retired doc/circuit-proof-friction.md feedback list. Related, already tracked separately: #407 on the loop combinators' differing contracts.)
🤖 Generated with Claude Code