def xstep

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/f64bits.bend:63

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

63# flipping the top bit
64def xstep(+q: Nat, +b: Bool, +t: Word(1n+q), +ih: {S.unsigned(1n+q, Word.xor(1n+q, t, WD.pw(1n+q, q))) == Nat.add(C.low(q, S.unsigned(1n+q, t)), C.shift(q, Nat.sub(1n, C.high(q, S.unsigned(1n+q, t))))) : Nat}) -> {S.unsigned(2n+q, Word.xor(2n+q, WCon{b, t}, WD.pw(2n+q, 1n+q))) == Nat.add(C.low(1n+q, S.unsigned(2n+q, WCon{b, t})), C.shift(1n+q, Nat.sub(1n, C.high(1n+q, S.unsigned(2n+q, WCon{b, t}))))) : Nat}:
65  match b:
66    case True{}:
67      +T = S.unsigned(1n+q, t)
68      +X0 = S.unsigned(1n+q, Word.xor(1n+q, t, WD.pw(1n+q, q)))
69      +lq = C.low(q, T)
70      +sq = C.shift(q, Nat.sub(1n, C.high(q, T)))
71      +U0 = Nat.add(1n, Nat.double(T))
72      +e1 = Equal.cong(Nat, Nat, z => 1n+Nat.double(z), X0, Nat.add(lq, sq), ih)
73      +e2 = Equal.cong(Nat, Nat, z => 1n+z, Nat.double(Nat.add(lq, sq)), Nat.add(Nat.double(lq), Nat.double(sq)), NA.double_add(lq, sq))
74      +r1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), C.bit(U0), 1n, WW.bit_dbl(1n, T))
75      +r2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1n, Nat.double(C.low(q, z))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, z))))), C.half(U0), T, WW.half_dbl(1n, T))
76      +r = Equal.trans(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(1n, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(1n, Nat.double(lq)), Nat.double(sq)), r1, r2)
77      Equal.trans(Nat, 1n+Nat.double(X0), 1n+Nat.double(Nat.add(lq, sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e1, Equal.trans(Nat, 1n+Nat.double(Nat.add(lq, sq)), Nat.add(Nat.add(1n, Nat.double(lq)), Nat.double(sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e2, Equal.sym(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(1n, Nat.double(lq)), Nat.double(sq)), r)))
78    case False{}:
79      +T = S.unsigned(1n+q, t)
80      +X0 = S.unsigned(1n+q, Word.xor(1n+q, t, WD.pw(1n+q, q)))
81      +lq = C.low(q, T)
82      +sq = C.shift(q, Nat.sub(1n, C.high(q, T)))
83      +U0 = Nat.add(0n, Nat.double(T))
84      +e1 = Equal.cong(Nat, Nat, z => Nat.double(z), X0, Nat.add(lq, sq), ih)
85      +e2 = NA.double_add(lq, sq)
86      +r1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), C.bit(U0), 0n, WW.bit_dbl(0n, T))
87      +r2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(0n, Nat.double(C.low(q, z))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, z))))), C.half(U0), T, WW.half_dbl(0n, T))
88      +r = Equal.trans(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(0n, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.double(lq), Nat.double(sq)), r1, r2)
89      Equal.trans(Nat, Nat.double(X0), Nat.double(Nat.add(lq, sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e1, Equal.trans(Nat, Nat.double(Nat.add(lq, sq)), Nat.add(Nat.double(lq), Nat.double(sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e2, Equal.sym(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.double(lq), Nat.double(sq)), r)))