try working on combining shift register, we morally are on the right track but need to finetune the indexing and make sure the boundary cases don't break stuff)

seems to work, i think we should write the shift register so we can do the proof against the golden model (which uses a nonsynthesizable RAM)

we can make this read-only because the only write that happens is for the parse tree and there's no read/write, it can be done with a straightforward gearbox, i believe.

make it work in general case with non-unitary bit widths. also k-induction doesn't require more than 1 step!

remove superfluous asserts. at least i think they're superfluous, we still need to check with different upstream/downstream widths.

with it

different

ready