def small_by

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/reduce.bend:97

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/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

97def small_by(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +c: Nat, +V: Nat, +b: Bool, +hb: {Nat.is_lt(c, one) == b : Bool}, +ha: {Nat.is_lt(a, LM.shn(32n, one)) == True{} : Bool}, +hv: {Nat.add(a, LM.shn(32n, c)) == V : Nat}, +hV: {Nat.is_lt(V, Nat.add(LM.shn(32n, one), WD.sc(27n, one))) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), LM.shn(32n, one)) == True{} : Bool}:
98  match b:
99    case True{}:
100      small_zero(one, h1, a, c, ha, hb)
101    case False{}:
102      small_one(one, h1, a, c, V, hv, hV, N.not_lt_le(c, one, hb))