def ws.g1a

bend-osdev-word64@0.1.1.0 · proof_shift.bend:376

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

376def ws.g1a(+n: Nat, +k: Nat, +w: Word(n), +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {Word.to_nat(n, ws.shl(n, k, w)) == U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))) : Nat}:
377  +er = UL.nat_le_witness(U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), Word.to_nat(n, w), ws.shr_le(n, Nat.sub(n, k), w))
378  +h1 = P.wn.lt_rw(Word.to_nat(n, w), Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), Equal.sym(Nat, Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Word.to_nat(n, w), er), ws.shr_lt(n, Nat.sub(n, k), w))
379  +h2 = P.wn.lt_rw2(Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n+Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), Nat.add(U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), UL.dbl_add(Nat.sub(n, k), 1n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))), h1)
380  +hr = Equal.trans(Bool, Nat.is_lt(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), Nat.is_lt(Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Nat.add(U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), Nat.add(U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), Nat.is_lt(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), P.wn.lt_add_r(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), h2)
381  +hrk = P.wn.lt_rw2(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n)), U.U32Nat.dbl(n, 1n), ns.dkm(n, k, 1n, hk), Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(k, U.U32Nat.dbl(Nat.sub(n, k), 1n))), Nat.is_lt(Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), True{}, UL.dbl_lt(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), U.U32Nat.dbl(Nat.sub(n, k), 1n)), hr))
382  ws.uniq(n, ws.ov(n, k, w), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)), Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, ws.shl(n, k, w)), U.U32Nat.dbl(n, ws.ov(n, k, w))), U.U32Nat.dbl(k, Word.to_nat(n, w)), Nat.add(U.U32Nat.dbl(k, Nat.sub(Word.to_nat(n, w), U.U32Nat.dbl(Nat.sub(n, k), Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w))))), U.U32Nat.dbl(n, Word.to_nat(n, ws.shr(n, Nat.sub(n, k), w)))), ws.shlk(n, k, w), ws.g1w(n, k, w, hk)), UL.word_value_lt(n, ws.shl(n, k, w)), hrk)