def step_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/xor.bend:41

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/random/pcg.bend as SP
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH

41# one step of xor_bits on two values written bit + 2 rest
42def step_eq(+p: Nat, +ba: Bool, +ua: Nat, +bb: Bool, +ub: Nat) -> {SP.xor_bits(1n+p, Nat.add(S.bit_value(ba), Nat.double(ua)), Nat.add(S.bit_value(bb), Nat.double(ub))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}:
43  +A = Nat.add(S.bit_value(ba), Nat.double(ua))
44  +B = Nat.add(S.bit_value(bb), Nat.double(ub))
45  %Equal.sym(Nat, C.bit(A), S.bit_value(ba), bit_bvd(ba, ua)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(_, C.bit(B)))), Nat.double(SP.xor_bits(p, C.half(A), C.half(B)))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
46  %Equal.sym(Nat, C.bit(B), S.bit_value(bb), bit_bvd(bb, ub)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), _))), Nat.double(SP.xor_bits(p, C.half(A), C.half(B)))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
47  %Equal.sym(Nat, C.half(A), ua, SH.half_bv(ba, ua)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, _, C.half(B)))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
48  %Equal.sym(Nat, C.half(B), ub, SH.half_bv(bb, ub)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, _))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
49  {==}