Bit-blasting circuits over a finite carrier

Let enc : F ≃ BitString w encode the elements of a carrier F by w bits. A circuit over the full binary basis of F (fullInterpretation (k := 2), where every constant and every operation with at most two arguments is a gate) is simulated by a De Morgan circuit on the encodings: each gate is replaced by w circuits, one for each bit of its value, each a function of the 2 * w bits of the gate's arguments and so computable with 2 ^ (2 * w) * (4 * w + 2) + 1 gates by its disjunctive normal form (Cslib.Circuits.Synthesis.selected). A gate of the full basis therefore costs at most bitBlastCost w = w * (2 ^ (2 * w) * (4 * w + 2) + 1) De Morgan gates. For a field F with q = 2 ^ w elements this is O(w ^ 2 * q ^ 2) gates per field operation, a polynomial in q, which suffices for reconstruction arguments whose circuits are polynomial in q anyway.

The simulation is stated as a synthesis bound (Cslib.Circuits.Synthesis.bitBlast): if the bits of the F-valued functions feeding the circuit's inputs are available, then the bits of all its outputs can be made available with size * bitBlastCost w further gates.

Main definitions

• Cslib.Circuits.bitsOf: the bits of an F-valued function under an encoding.
• Cslib.Circuits.bitBlastCost: the De Morgan cost of one gate of the full binary basis.

Main results

• Cslib.Circuits.Synthesis.bitBlast_program: the bits of every wire of a program over the full binary basis.
• Cslib.Circuits.Synthesis.bitBlast: the bits of every output of a circuit over the full binary basis.
• Cslib.Circuits.Synthesis.bitBlast_synthesis: the same for a synthesis bound over the full binary basis.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers
• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]

def Cslib.Circuits.bitsOf {F : Type u_1} {w n : ℕ} (enc : F ≃ BitString w) (φ : (Fin n → Bool) → F) (j : Fin w) : BooleanFunction n

The j-th bit, under the encoding enc, of an F-valued function φ of the inputs.

def Cslib.Circuits.bitBlastCost (w : ℕ) : ℕ

The number of De Morgan gates that simulate one gate of the full binary basis on w-bit symbols: each of the w bits of the value is a function of the 2 * w bits of the arguments.

theorem Cslib.Circuits.Synthesis.bitBlast_program {F : Type u_1} {w n : ℕ} (enc : F ≃ BitString w) {s : Set (BooleanFunction n)} {N g : ℕ} (p : Program (fullSignature 2 F) N g) (φ : Fin N → (Fin n → Bool) → F) (hφ : ∀ (i : Fin N) (j : Fin w), bitsOf enc (φ i) j ∈ s) : Synthesis Boolean.interpretation s (Set.range fun (wj : Wire N g × Fin w) => bitsOf enc (fun (x : Fin n → Bool) => p.trace fullInterpretation (fun (i : Fin N) => φ i x) wj.1) wj.2) (g * bitBlastCost w)

Bit-blasting a program. If the bits of the functions φ i feeding the inputs of a program over the full binary basis of F are available, then the bits of the values of all its wires can be made available with bitBlastCost w De Morgan gates for each of its gates.

theorem Cslib.Circuits.Synthesis.bitBlast {F : Type u_1} {w n : ℕ} (enc : F ≃ BitString w) {s : Set (BooleanFunction n)} {N M : ℕ} (c : Circuit (fullSignature 2 F) N M) (φ : Fin N → (Fin n → Bool) → F) (hφ : ∀ (i : Fin N) (j : Fin w), bitsOf enc (φ i) j ∈ s) : Synthesis Boolean.interpretation s (Set.range fun (oj : Fin M × Fin w) => bitsOf enc (fun (x : Fin n → Bool) => c.eval fullInterpretation (fun (i : Fin N) => φ i x) oj.1) oj.2) (c.size * bitBlastCost w)

Bit-blasting a circuit. If the bits of the functions φ i feeding the inputs of a circuit over the full binary basis of F are available, then the bits of all its outputs can be made available with c.size * bitBlastCost w De Morgan gates.

theorem Cslib.Circuits.Synthesis.bitBlast_synthesis {F : Type u_1} {w n : ℕ} (enc : F ≃ BitString w) {N : ℕ} {ι : Type u_2} [Finite ι] (Ψ : ι → (Fin N → F) → F) {cost : ℕ} (h : Synthesis fullInterpretation (inputs N) (Set.range Ψ) cost) {s : Set (BooleanFunction n)} (φ : Fin N → (Fin n → Bool) → F) (hφ : ∀ (i : Fin N) (j : Fin w), bitsOf enc (φ i) j ∈ s) : Synthesis Boolean.interpretation s (Set.range fun (oj : ι × Fin w) => bitsOf enc (fun (x : Fin n → Bool) => Ψ oj.1 fun (i : Fin N) => φ i x) oj.2) (cost * bitBlastCost w)

Bit-blasting a synthesis bound. If a family Ψ of functions of N field inputs is synthesized over the full binary basis from the input projections with cost gates, and the bits of the functions φ i feeding the inputs are available, then the bits of all Ψ o (φ ·) can be made available with cost * bitBlastCost w De Morgan gates.