def from_nat_step

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/word_value.bend:93

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/lemmas/proofs/nat_algebra.bend as A

93def from_nat_step(+p: Nat, +v: Nat, parts: {v == Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)) : Nat} & {Nat.is_le(Nat.mod(v, 2n), 1n) == True{} : Bool}, bound: {Nat.is_lt(v, Nat.mul(2n, Nat.pow(2n, p))) == True{} : Bool}, ih: @+q: Nat -> @hq: {Nat.is_lt(q, Nat.pow(2n, p)) == True{} : Bool} -> {S.unsigned(p, S.from_nat(p, q)) == q : Nat}) -> {S.unsigned(1n+p, S.from_nat(1n+p, v)) == v : Nat}:
94  (+eq, le) = parts
95  %Equal.sym(Nat, S.unsigned(p, S.from_nat(p, Nat.div(v, 2n))), Nat.div(v, 2n), ih(Nat.div(v, 2n), lt_double(Nat.div(v, 2n), Nat.pow(2n, p), Nat.mod(v, 2n), rescale(p, v, eq, bound)))) : {Nat.add(S.bit_value(Nat.is_eq(Nat.mod(v, 2n), 1n)), Nat.double(_)) == v : Nat}
96  %Equal.sym(Nat, S.bit_value(Nat.is_eq(Nat.mod(v, 2n), 1n)), Nat.mod(v, 2n), remainder_bit(Nat.mod(v, 2n), le)) : {Nat.add(_, Nat.double(Nat.div(v, 2n))) == v : Nat}
97  %Equal.sym(Nat, v, Nat.add(Nat.mul(Nat.div(v, 2n), 2n), Nat.mod(v, 2n)), eq) : {Nat.add(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n))) == _ : Nat}
98  %Equal.sym(Nat, Nat.mul(Nat.div(v, 2n), 2n), Nat.double(Nat.div(v, 2n)), two_times(Nat.div(v, 2n))) : {Nat.add(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n))) == Nat.add(_, Nat.mod(v, 2n)) : Nat}
99  A.add_comm(Nat.mod(v, 2n), Nat.double(Nat.div(v, 2n)))