def word_from_unsigned

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:40

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA

40# Every word is recovered from its unsigned interpretation (reconstruct at 0).
41def word_from_unsigned(+w: Word(32n)) -> {S.from_nat(32n, S.unsigned(32n, w)) == w : Word(32n)}:
42  %N.add_zero(S.unsigned(32n, w)) : {S.from_nat(32n, _) == w : Word(32n)}
43  MA.reconstruct(32n, w, 0n)