def le_go

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/bits.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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

97def le_go(fuel: Nat, +n: Nat, +hf: {Nat.is_le(n, fuel) == True{} : Bool}) -> {Nat.is_le(SC.pow2(M.bit_length_go(fuel, n, 0n)), Nat.max(1n, Nat.double(n))) == True{} : Bool}:
98  match fuel n:
99    case 0n 0n:
100      {==}
101    case 0n 1n+np:
102      Empty.absurd({Nat.is_le(SC.pow2(M.bit_length_go(0n, 1n+np, 0n)), Nat.max(1n, Nat.double(1n+np))) == True{} : Bool}, L.false_true(hf))
103    case 1n+f 0n:
104      {==}
105    case 1n+ +f 1n+ +np:
106      +h = Nat.div(1n+np, 2n)
107      +x = M.bit_length_go(f, h, 0n)
108      +ih = le_go(f, h, half_fuel(np, f, hf))
109      %Equal.sym(Nat, M.bit_length_go(f, h, 1n), 1n+x, go_acc(f, h, 0n)) : {Nat.is_le(SC.pow2(_), Nat.max(1n, Nat.double(1n+np))) == True{} : Bool}
110      N.double_le(SC.pow2(x), 1n+np, le_step(np, h, x, half_eq(1n+np), ih))