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