def inv_140

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:240

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
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/math/natural/arith.bend as NR

240# fuel 140 against the reference fuel m, for m < 2^k, 2k+1 <= 140
241def inv_140(+k: Nat, +mp: Nat, +a: Nat, +hk: {Nat.is_le(1n+Nat.double(k), 140n) == True{} : Bool}, +hm: {Nat.is_lt(1n+mp, C.pow2(k)) == True{} : Bool}) -> {M.inv_go(140n, 1n+mp, 1n+mp, 0n, Nat.mod(a, 1n+mp), 1n) == M.inv_go(1n+mp, 1n+mp, 1n+mp, 0n, Nat.mod(a, 1n+mp), 1n) : M.Bezout}:
242  +hb = N.lt_trans(Nat.mod(a, 1n+mp), 1n+mp, C.pow2(k), NR.dm_lt(mp, a), hm)
243  inv_fuel(140n, 1n+mp, 1n+mp, 1n+mp, 0n, Nat.mod(a, 1n+mp), 1n, halve(k, 140n, 1n+mp, Nat.mod(a, 1n+mp), Nat.mod(1n+mp, Nat.mod(a, 1n+mp)), {==}, hb, hk), ends_self(1n+mp, 1n+mp, Nat.mod(a, 1n+mp), N.lt_le(Nat.mod(a, 1n+mp), 1n+mp, NR.dm_lt(mp, a))))