Syntactic degree propagation

A degree policy classifies each operation as constant, maximum-like (such as addition), or sum-like (such as multiplication). Inputs start in degree one. The resulting interpretation is a compositional abstract analysis; relating it to semantic polynomial degree only requires a separate soundness proof for the chosen concrete signature.

inductive Algebraic.DegreeMode : Type

Local rule used to propagate a degree bound through an operation.

• constant : DegreeMode
• maximum : DegreeMode
• sum : DegreeMode

@[instance_reducible]

instance Algebraic.instDecidableEqDegreeMode : DecidableEq DegreeMode

Equations

• Algebraic.instDecidableEqDegreeMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Algebraic.DegreeMode.eval (mode : DegreeMode) {arity : ℕ} (input : Fin arity → ℕ) : ℕ

Evaluate a local degree-propagation rule.

Equations

• Algebraic.DegreeMode.constant.eval input = 0
• Algebraic.DegreeMode.maximum.eval input = Fin.foldl arity (fun (degree : ℕ) (argument : Fin arity) => max degree (input argument)) 0
• Algebraic.DegreeMode.sum.eval input = ∑ argument : Fin arity, input argument

def Cslib.Circuits.Signature.degreeInterpretation (σ : Signature) (mode : σ.Op → Algebraic.DegreeMode) : Interpretation σ ℕ

Degree interpretation induced by a local rule for every operation.

Equations

• σ.degreeInterpretation mode op input = (mode op).eval input

def Cslib.Circuits.Circuit.degreeProfile {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (mode : σ.Op → Algebraic.DegreeMode) : Fin m → ℕ

Degree profile of a circuit when every original input has degree one.

Equations

• circuit.degreeProfile mode = circuit.eval (σ.degreeInterpretation mode) fun (x : Fin n) => 1

theorem Algebraic.Translation.compile_degreeProfile {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) (targetMode : τ.Op → DegreeMode) : (translation.compile circuit).degreeProfile targetMode = circuit.eval (translation.pull (τ.degreeInterpretation targetMode)) fun (x : Fin n) => 1

Translation gives exact degree propagation using the derived source operation rules implemented by the target gadgets.