def lt96

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:75

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

75def lt96(+q: Nat, +r: Nat, +hq: {Nat.is_lt(q, 3n) == True{} : Bool}, +hr: {Nat.is_lt(r, 32n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(q, 32n), r), 96n) == True{} : Bool}:
76  match q:
77    case 0n:
78      N.lt_trans(r, 32n, 96n, hr, {==})
79    case 1n:
80      N.lt_trans(r, 32n, 64n, hr, {==})
81    case 2n:
82      hr
83    case 3n+j:
84      Empty.absurd({Nat.is_lt(Nat.add(Nat.mul(3n+j, 32n), r), 96n) == True{} : Bool}, N.lt_zero_absurd(j, hq))