def mul_exact

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:63

import Base
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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as WM
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as NM

63# multiplication below 2^n is exact
64def mul_exact(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +a: Word(n), +b: Word(n), +h: {Nat.is_lt(Nat.mul(uw(n, a), uw(n, b)), sc(n, one)) == True{} : Bool}) -> {uw(n, Word.mul(n, a, b)) == Nat.mul(uw(n, a), uw(n, b)) : Nat}:
65  +p = Nat.mul(uw(n, a), uw(n, b))
66  %Equal.sym(Word(n), Word.mul(n, a, b), S.from_nat(n, p), WM.refines(n, a, b)) : {S.unsigned(n, _) == p : Nat}
67  WV.from_nat_value(n, p, L.subst(Nat, z => {Nat.is_lt(p, z) == True{} : Bool}, S.scale_binary(n, 1n), Nat.pow(2n, n), NM.scale_power(n), lt1(n, one, h1, p, h)))