def xorv

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

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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

300def xorv(+h: U32, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {v(U32.xor(h, c)) == Nat.add(C.low(31n, v(h)), C.shift(31n, Nat.sub(1n, C.high(31n, v(h))))) : Nat}:
301  L.subst(U32, z => {v(U32.xor(h, z)) == Nat.add(C.low(31n, v(h)), C.shift(31n, Nat.sub(1n, C.high(31n, v(h))))) : Nat}, U32{WD.pw(32n, 31n)}, c, Equal.sym(U32, c, U32{WD.pw(32n, 31n)}, hc), xorv0(h))