def and_low_step

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:232

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

232def and_low_step(+m: Nat, +d: Nat, +xb: Bool, +xt: Word(m), +yb: Bool, +yt: Word(m), +hy: {Nat.add(S.bit_value(yb), Nat.double(S.unsigned(m, yt))) == Nat.sub(SC.pow2(d), 1n) : Nat}, +hx: {Nat.is_lt(Nat.add(S.bit_value(xb), Nat.double(S.unsigned(m, xt))), SC.pow2(d)) == True{} : Bool}, +ih: {Word.and(m, xt, yt) == xt : Word(m)}) -> {WCon{Bool.and(xb, yb), Word.and(m, xt, yt)} == WCon{xb, xt} : Word(1n+m)}:
233  match d:
234    case 0n:
235      %Equal.sym(Word(m), Word.and(m, xt, yt), xt, ih) : {WCon{Bool.and(xb, yb), _} == WCon{xb, xt} : Word(1n+m)}
236      %Equal.sym(Bool, yb, False{}, and_low_hyb(m, 0n, yb, yt, hy)) : {WCon{Bool.and(xb, _), xt} == WCon{xb, xt} : Word(1n+m)}
237      %Equal.sym(Bool, xb, False{}, and_low_hxb(m, xb, xt, hx)) : {WCon{Bool.and(_, False{}), xt} == WCon{_, xt} : Word(1n+m)}
238      {==}
239    case 1n+k:
240      %Equal.sym(Word(m), Word.and(m, xt, yt), xt, ih) : {WCon{Bool.and(xb, yb), _} == WCon{xb, xt} : Word(1n+m)}
241      %Equal.sym(Bool, yb, True{}, and_low_hyb(m, 1n+k, yb, yt, hy)) : {WCon{Bool.and(xb, _), xt} == WCon{xb, xt} : Word(1n+m)}
242      %Equal.sym(Bool, Bool.and(xb, True{}), xb, and_true(xb)) : {WCon{_, xt} == WCon{xb, xt} : Word(1n+m)}
243      {==}