Documentation

MIPRE.Foundations.SAT.GateFieldEval

Uniform field evaluation of a routed gate #

Field elements are coefficient vectors modulo a supplied binary monic polynomial. Gate indices stay binary, including on malformed inputs.

source
@[reducible, inline]
abbrev MIPRE.SAT.Circuit.zeroBits (p : Cost.BitStr) :
Cost.BitStr

Circuit-facing zero coefficients, implemented by generic quotient arithmetic.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPRE.SAT.Circuit.oneBits :
    Cost.BitStr → Cost.BitStr

    Circuit-facing one coefficients, implemented by generic quotient arithmetic.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.SAT.Circuit.length_zeroBits (p : Cost.BitStr) :
      List.length (zeroBits p) = List.length p
      source
      @[simp]
      theorem MIPRE.SAT.Circuit.length_oneBits (p : Cost.BitStr) :
      List.length (oneBits p) = List.length p
      source
      @[simp]
      theorem MIPRE.SAT.Circuit.evalBits_zeroBits {R : Type u_1} [CommRing R] (z : R) (p : Cost.BitStr) :
      LowDegree.BinaryPolynomial.evalBits z (zeroBits p) = 0
      source
      theorem MIPRE.SAT.Circuit.evalBits_oneBits {R : Type u_1} [CommRing R] (z : R) (p : Cost.BitStr) (hp : p ≠ []) :
      LowDegree.BinaryPolynomial.evalBits z (oneBits p) = 1
      source
      @[reducible, inline]
      noncomputable abbrev MIPRE.SAT.Circuit.zeroBitsProg :
      Cost.PolyTimeFun Cost.BitStr Cost.BitStr
      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev MIPRE.SAT.Circuit.oneBitsProg :
        Cost.PolyTimeFun Cost.BitStr Cost.BitStr
        Equations
        Instances For
          source
          @[simp]
          theorem MIPRE.SAT.Circuit.zeroBitsProg_apply (p : Cost.BitStr) :
          zeroBitsProg.toFun p = zeroBits p
          source
          @[simp]
          theorem MIPRE.SAT.Circuit.oneBitsProg_apply (p : Cost.BitStr) :
          oneBitsProg.toFun p = oneBits p
          source
          def MIPRE.SAT.Circuit.gateBits (p : Cost.BitStr) (x : ℕ → Cost.BitStr) (w : List Cost.BitStr) :
          Gate → Cost.BitStr

          Gate arithmetic on coefficient vectors. The input reader is supplied separately so that the same arithmetic supports the routed copy links.

          Equations
          Instances For
            source
            def MIPRE.SAT.Circuit.gateValue {R : Type u_1} [CommRing R] (x w : ℕ → R) :
            Gate → R

            The corresponding field expression in characteristic two.

            Equations
            Instances For
              source
              theorem MIPRE.SAT.Circuit.length_gateBits (p : Cost.BitStr) (x : ℕ → Cost.BitStr) (w : List Cost.BitStr) (g : Gate) (hx : ∀ (i : ℕ), g = Gate.input i → List.length (x i) = List.length p) (hw : ∀ j ∈ g.refs, List.length (w.getD j []) = List.length p) :
              List.length (gateBits p x w g) = List.length p
              source
              theorem MIPRE.SAT.Circuit.evalBits_gateBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (x : ℕ → Cost.BitStr) (w : List Cost.BitStr) (g : Gate) (hw : ∀ j ∈ g.refs, List.length (w.getD j []) = List.length p) :
              LowDegree.BinaryPolynomial.evalBits z (gateBits p x w g) = gateValue (fun (i : ℕ) => LowDegree.BinaryPolynomial.evalBits z (x i)) (fun (j : ℕ) => LowDegree.BinaryPolynomial.evalBits z (w.getD j [])) g

              Correctness of all five gate operations over every characteristic-two ring containing a root of the supplied modulus.

              source
              theorem MIPRE.SAT.Circuit.gateValue_eq_eval_gateArith {F : Type u_2} [Field F] [CharP F 2] (C : Circuit) (k : ℕ) (g : Gate) (x w : ℕ → F) :
              gateValue (fun (i : ℕ) => Sum.elim x w (C.inputRef k i)) w g = (MvPolynomial.eval (Sum.elim x w)) (C.gateArith k g)
              source
              @[reducible, inline]
              abbrev MIPRE.SAT.Circuit.FieldEnv :
              Type

              Modulus, external coordinates, gate coordinates, and preceding gate/value pairs.

              Equations
              Instances For
                source
                def MIPRE.SAT.Circuit.readInput (e : FieldEnv) (i : ℕ) :
                Cost.BitStr
                Equations
                Instances For
                  source
                  noncomputable def MIPRE.SAT.Circuit.readInputProg :
                  Cost.PolyTimeFun (FieldEnv × ℕ) Cost.BitStr
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem MIPRE.SAT.Circuit.readInputProg_apply (e : FieldEnv) (i : ℕ) :
                    readInputProg.toFun (e, i) = readInput e i
                    source
                    noncomputable def MIPRE.SAT.Circuit.gateBitsProg :
                    Cost.PolyTimeFun (FieldEnv × Gate) Cost.BitStr

                    Uniform polynomial-time field evaluation of one routed gate.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem MIPRE.SAT.Circuit.gateBitsProg_apply (e : FieldEnv) (g : Gate) :
                      gateBitsProg.toFun (e, g) = gateBits e.1 (readInput e) e.2.2.1 g