Description
Review items: R1, R2
Each decode lemma repeats ~20 lines of boilerplate. Write a generic decode_at_offset lemma that takes offset and byte list, returning the decode result. Each instruction decode becomes a one-liner.
This is the single biggest barrier to scaling to real s2n-bignum routines (50-200 instructions).
Files affected
Bignum/Arm/Machine/Decode.lean (add generic lemma)Bignum/Arm/Tutorial/Simple.lean (simplify decode lemmas)Bignum/Arm/Tutorial/Sequence.lean (simplify decode lemmas)
Description
Review items: R1, R2
Each decode lemma repeats ~20 lines of boilerplate. Write a generic
decode_at_offsetlemma that takes offset and byte list, returning the decode result. Each instruction decode becomes a one-liner.This is the single biggest barrier to scaling to real s2n-bignum routines (50-200 instructions).
Files affected
Bignum/Arm/Machine/Decode.lean(add generic lemma)Bignum/Arm/Tutorial/Simple.lean(simplify decode lemmas)Bignum/Arm/Tutorial/Sequence.lean(simplify decode lemmas)