Possible-value abstraction

For a finite concrete carrier, an operation on sets returns every result obtainable by choosing one concrete value from each argument set. This is the standard nonrelational possible-value abstraction. Singleton inputs reproduce concrete circuit evaluation exactly, while arbitrary input sets can safely forget correlations between wires.

noncomputable def Cslib.Circuits.Interpretation.possibleValues {U : Type u_1} {σ : Signature} [Fintype U] (interpretation : Interpretation σ U) : Interpretation σ (Finset U)

Pointwise possible-value lifting of a concrete interpretation.

Equations

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

@[simp]

theorem Cslib.Circuits.Interpretation.mem_possibleValues {U : Type u_1} {σ : Signature} [Fintype U] (interpretation : Interpretation σ U) (op : σ.Op) (input : Fin (σ.Arity op) → Finset U) (output : U) : output ∈ interpretation.possibleValues op input ↔ ∃ (concrete : Fin (σ.Arity op) → U), (∀ (argument : Fin (σ.Arity op)), concrete argument ∈ input argument) ∧ interpretation op concrete = output

noncomputable def Cslib.Circuits.Interpretation.singletonHomomorphism {U : Type u_1} {σ : Signature} [Fintype U] (interpretation : Interpretation σ U) : Homomorphism interpretation interpretation.possibleValues

Sending a value to its singleton set is a homomorphism into the possible-value interpretation.

Equations

• interpretation.singletonHomomorphism = { map := fun (value : U) => {value}, homomorphic := ⋯ }

theorem Cslib.Circuits.Circuit.eval_possibleValues_singleton {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype U] (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → U) : (fun (value : U) => {value}) ∘ circuit.eval interpretation input = circuit.eval interpretation.possibleValues ((fun (value : U) => {value}) ∘ input)

Possible-value evaluation agrees exactly with concrete evaluation on singleton input sets.

theorem Cslib.Circuits.Program.eval_mem_possibleValues {U : Type u_1} {σ : Signature} {n g : ℕ} [Fintype U] (program : Program σ n g) (interpretation : Interpretation σ U) (concreteInput : Fin n → U) (abstractInput : Fin n → Finset U) (contained : ∀ (input : Fin n), concreteInput input ∈ abstractInput input) (gate : Fin g) : program.eval interpretation concreteInput gate ∈ program.eval interpretation.possibleValues abstractInput gate

Every concrete gate value belongs to the possible-value analysis whenever each concrete input belongs to its supplied abstract input set.

theorem Cslib.Circuits.Program.trace_mem_possibleValues {U : Type u_1} {σ : Signature} {n g : ℕ} [Fintype U] (program : Program σ n g) (interpretation : Interpretation σ U) (concreteInput : Fin n → U) (abstractInput : Fin n → Finset U) (contained : ∀ (input : Fin n), concreteInput input ∈ abstractInput input) (wire : Wire n g) : program.trace interpretation concreteInput wire ∈ program.trace interpretation.possibleValues abstractInput wire

Every concrete wire value belongs to its possible-value abstraction.

theorem Cslib.Circuits.Circuit.eval_mem_possibleValues {U : Type u_1} {σ : Signature} {n m : ℕ} [Fintype U] (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (concreteInput : Fin n → U) (abstractInput : Fin n → Finset U) (contained : ∀ (input : Fin n), concreteInput input ∈ abstractInput input) (output : Fin m) : circuit.eval interpretation concreteInput output ∈ circuit.eval interpretation.possibleValues abstractInput output

Every concrete circuit output belongs to the corresponding possible-value output set.

theorem Algebraic.Translation.compile_possibleValues {U : Type u_1} {σ : Signature} {τ : Signature} {n m : ℕ} [Fintype U] (translation : Translation σ τ) (circuit : Circuit σ n m) (interpretation : Interpretation τ U) (input : Fin n → Finset U) : (translation.compile circuit).eval interpretation.possibleValues input = circuit.eval (translation.pull interpretation.possibleValues) input

Translation preserves possible-value propagation exactly at the abstract level.