Realign spec and proofs

[blaxill]

A few admits still left to go.

[samuelgruetter]

I see a lot of proofs here that start with N.bits_inj and then prove that for each bit index, N.testbit at that index returns the same on the left and right of the equality to prove. I have already developed automation for this proof strategy twice (but for Z, not for N):

• A first approach, mostly used in riscv-coq, was getting a bit complex, and ran into performance problems in lia, btauto, and rewriting (though rewrite_strat helped), and still fails to prove some goals I think it should prove, and also runs forever if I add all the rewrite lemmas I think it should use.
• A simpler second approach, which is easier to deal with, but less powerful than the first one.

I don't claim that there's anything ready to use for you there, but depending on how many more bitwise goals you need to prove, maybe you could harvest some reusable snippets from these files. Or if you expect really many bitwise goals, it might be worth considering developing a tactic that's actually good and works for all goals in cava & riscv-coq & bedrock2, but that would be a bit of an investment...

[blaxill]

I see a lot of proofs here that start with N.bits_inj and then prove that for each bit index, N.testbit at that index returns the same on the left and right of the equality to prove. I have already developed automation for this proof strategy twice (but for Z, not for N):

• A first approach, mostly used in riscv-coq, was getting a bit complex, and ran into performance problems in lia, btauto, and rewriting (though rewrite_strat helped), and still fails to prove some goals I think it should prove, and also runs forever if I add all the rewrite lemmas I think it should use.
• A simpler second approach, which is easier to deal with, but less powerful than the first one.

I don't claim that there's anything ready to use for you there, but depending on how many more bitwise goals you need to prove, maybe you could harvest some reusable snippets from these files. Or if you expect really many bitwise goals, it might be worth considering developing a tactic that's actually good and works for all goals in cava & riscv-coq & bedrock2, but that would be a bit of an investment...

Thanks. I had previously approached those proofs with normal rewriting, but it was taking a huge number of rewrites to massage the goal and was taking too long. The bitwise specialised-for-my-specific goal tactics didn't actually take too long, but I'll definitely use your machinery in the future

[jadephilipoom]

I've already got a tactic for bitwise reasoning in N in our repo called push_Ntestbit. Just apply N.bits_inj, then intro, then push_Ntestbit will take you as far as it can go. Might need further destructs to rewrite with lemmas that have arithmetic side conditions (e.g. for N.testbit (N,ones x) i you will need to destruct i <? x), so there's room for more automation there, but should help with the majority of the manual steps.

[blaxill]

The proof is reduced to some admitted lemmas about concat_bytes which all look to be true- I'd like to address them in a follow up PR.

I should have broken down the main proofs further/better but oh well I've learnt my lesson for the future.

@jadephilipoom could you take a look please?