Documentation

Sparkle.Core.MulOracle

source
@[reducible, inline]
abbrev MulOracle.S :
Type
Equations
Instances For
    source
    def MulOracle.step (s : S) :
    S
    Equations
    Instances For
      source
      def MulOracle.extract (s : S) :
      BitVec 64
      Equations
      Instances For
        source
        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
        source
        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
        source
        @[implicit_reducible]
        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.