def inv

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:34

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

34# the long-division invariant of a partial result r for the prefix a
35def inv(+m: Nat, +a: Word(m), +bn: Nat, r: Word(m) & U32) -> Type:
36  {Nat.add(Nat.mul(S.unsigned(m, dq(m, r)), bn), v(dr(m, r))) == S.unsigned(m, a) : Nat} & {Nat.is_lt(v(dr(m, r)), bn) == True{} : Bool}