def inc_exact

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

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_value.bend as WV
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as NM
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA

345# an increment below 2^n is exact
346def inc_exact(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +w: Word(n), +h: {Nat.is_lt(1n+uw(n, w), sc(n, one)) == True{} : Bool}) -> {uw(n, Word.inc(n, w)) == 1n+uw(n, w) : Nat}:
347  %Equal.sym(Word(n), Word.inc(n, w), S.from_nat(n, 1n+uw(n, w)), MA.increment_refines(n, w)) : {S.unsigned(n, _) == 1n+uw(n, w) : Nat}
348  WV.from_nat_value(n, 1n+uw(n, w), L.subst(Nat, z => {Nat.is_lt(1n+uw(n, w), z) == True{} : Bool}, S.scale_binary(n, 1n), Nat.pow(2n, n), NM.scale_power(n), lt1(n, one, h1, 1n+uw(n, w), h)))