~/jendhub

def and_step

bend-collections-laws-math@1.0.0.0 · proofs/math/random/bits.bend:23

import bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend as Bits
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/rand.bend as SR
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WI

23# one bit and the rest: (b + 2a) & (c + 2d) = b c + 2 (a & d)
24def and_step(+p: Nat, +b: Nat, +a: Nat, +c: Nat, +d: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +hc: {Nat.is_le(c, 1n) == True{} : Bool}) -> {SR.and_bits(1n+p, Nat.add(b, Nat.double(a)), Nat.add(c, Nat.double(d))) == Nat.add(Nat.mul(b, c), Nat.double(SR.and_bits(p, a, d))) : Nat}:
25  match b c:
26    case 0n 0n:
27      %Equal.sym(Nat, C.bit(Nat.double(a)), 0n, WI.bit_dbl(0n, a)) : {Nat.add(Nat.mul(_, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, C.half(Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
28      %Equal.sym(Nat, C.half(Nat.double(a)), a, WI.half_dbl(0n, a)) : {Nat.add(Nat.mul(0n, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, _, C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
29      %Equal.sym(Nat, C.half(Nat.double(d)), d, WI.half_dbl(0n, d)) : {Nat.add(Nat.mul(0n, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
30      {==}
31    case 0n 1n:
32      %Equal.sym(Nat, C.bit(Nat.double(a)), 0n, WI.bit_dbl(0n, a)) : {Nat.add(Nat.mul(_, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, C.half(Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
33      %Equal.sym(Nat, C.half(Nat.double(a)), a, WI.half_dbl(0n, a)) : {Nat.add(Nat.mul(0n, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, _, C.half(1n+Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
34      %Equal.sym(Nat, C.half(1n+Nat.double(d)), d, WI.half_dbl(1n, d)) : {Nat.add(Nat.mul(0n, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
35      {==}
36    case 1n 0n:
37      %Equal.sym(Nat, C.bit(1n+Nat.double(a)), 1n, WI.bit_dbl(1n, a)) : {Nat.add(Nat.mul(_, C.bit(Nat.double(d))), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
38      %Equal.sym(Nat, C.bit(Nat.double(d)), 0n, WI.bit_dbl(0n, d)) : {Nat.add(Nat.mul(1n, _), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
39      %Equal.sym(Nat, C.half(1n+Nat.double(a)), a, WI.half_dbl(1n, a)) : {Nat.add(Nat.mul(1n, 0n), Nat.double(SR.and_bits(p, _, C.half(Nat.double(d))))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
40      %Equal.sym(Nat, C.half(Nat.double(d)), d, WI.half_dbl(0n, d)) : {Nat.add(Nat.mul(1n, 0n), Nat.double(SR.and_bits(p, a, _))) == Nat.add(0n, Nat.double(SR.and_bits(p, a, d))) : Nat}
41      {==}
42    case 1n 1n:
43      %Equal.sym(Nat, C.bit(1n+Nat.double(a)), 1n, WI.bit_dbl(1n, a)) : {Nat.add(Nat.mul(_, C.bit(1n+Nat.double(d))), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
44      %Equal.sym(Nat, C.bit(1n+Nat.double(d)), 1n, WI.bit_dbl(1n, d)) : {Nat.add(Nat.mul(1n, _), Nat.double(SR.and_bits(p, C.half(1n+Nat.double(a)), C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
45      %Equal.sym(Nat, C.half(1n+Nat.double(a)), a, WI.half_dbl(1n, a)) : {Nat.add(Nat.mul(1n, 1n), Nat.double(SR.and_bits(p, _, C.half(1n+Nat.double(d))))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
46      %Equal.sym(Nat, C.half(1n+Nat.double(d)), d, WI.half_dbl(1n, d)) : {Nat.add(Nat.mul(1n, 1n), Nat.double(SR.and_bits(p, a, _))) == Nat.add(1n, Nat.double(SR.and_bits(p, a, d))) : Nat}
47      {==}
48    case 2n+q _:
49      Empty.absurd({SR.and_bits(1n+p, Nat.add(2n+q, Nat.double(a)), Nat.add(c, Nat.double(d))) == Nat.add(Nat.mul(2n+q, c), Nat.double(SR.and_bits(p, a, d))) : Nat}, L.false_true(hb))
50    case _ 2n+q:
51      Empty.absurd({SR.and_bits(1n+p, Nat.add(b, Nat.double(a)), Nat.add(2n+q, Nat.double(d))) == Nat.add(Nat.mul(b, 2n+q), Nat.double(SR.and_bits(p, a, d))) : Nat}, L.false_true(hc))

Uses (14)

Used by (1)