@[reducible, inline]

abbrev MulOracle.S : Type

Equations

• MulOracle.S = (BitVec 64 × BitVec 64 × BitVec 64 × BitVec 64)

def MulOracle.step (s : S) : S

Equations

• MulOracle.step s = Sparkle.Verification.MulProps.carrySaveStep s.fst s.snd.fst s.snd.snd.fst s.snd.snd.snd

def MulOracle.extract (s : S) : BitVec 64

Equations

• MulOracle.extract s = s.fst + s.snd.fst

theorem MulOracle.csa64_main (a b : BitVec 64) : match Sparkle.Verification.MulProps.carrySaveN 64 0 0 a b with | (rd, rdx, fst, snd) => rd + rdx = a * b

theorem MulOracle.equiv (input : BitVec 64 × BitVec 64) : extract (Sparkle.Core.OracleSpec.iterateN step 64 (0, 0, input.fst, input.snd)) = input.fst * input.snd

instance instOracleReductionSProdBitVecOfNatNat : Sparkle.Core.OracleSpec.OracleReduction "pcpi_mul" MulOracle.S (BitVec 64 × BitVec 64) (BitVec 64)

Equations

• One or more equations did not get rendered due to their size.