Bitstring-level Barrington code generator

barringtonCompileCode is the exact total function targeted by the remaining uniformity proof. On a canonical postfix formula code it emits the canonical code of barringtonCompile formula barringtonTargetBase; malformed inputs map to the empty string.

This module proves the complete extensional specification independently of a machine implementation: output decoding recovers the executable program, its evaluation matches the source formula, and its instruction count is at most 4 ^ depth. The next layer must realize this particular function in FL.

Main results

• barringtonCompileCode_encode -- exact generated bits.
• decode?_barringtonCompileCode_encode -- generated-code round trip.
• length_barringtonCompileCode_encode_le -- serialized output-size bound.
• barringtonCompileCode_spec -- decoded semantics and Barrington length bound.

theorem Complexity.formula_variable_le_code_length (formula : BoolFormula) (index : ℕ) (hindex : index ∈ formula.vars) : index ≤ (FormulaCode.encode formula).length

Every variable referenced by a formula is at most its canonical code length.

@[simp]

theorem Complexity.barringtonCompileCode_encode (formula : BoolFormula) : barringtonCompileCode (FormulaCode.encode formula) = BPCode.Program.encode (barringtonCompile formula barringtonTargetBase)

On canonical formula input, the generator emits exactly the canonical encoding of the executable Barrington compiler's result.

theorem Complexity.decode?_barringtonCompileCode_encode (formula : BoolFormula) : BPCode.Program.decode? (barringtonCompileCode (FormulaCode.encode formula)) = some (barringtonCompile formula barringtonTargetBase)

Decoding generated code recovers the executable compiler's program.

theorem Complexity.length_barringtonCompileCode_encode (formula : BoolFormula) : (barringtonCompileCode (FormulaCode.encode formula)).length = List.length (barringtonCompile formula barringtonTargetBase) + 1 + (List.map (fun (instruction : BPInstr 5) => instruction.var + 15) (barringtonCompile formula barringtonTargetBase)).sum

Exact generated-code length on canonical formula input.

theorem Complexity.length_barringtonCompileCode_encode_le (formula : BoolFormula) : (barringtonCompileCode (FormulaCode.encode formula)).length ≤ 4 ^ formula.depth + 1 + 4 ^ formula.depth * ((FormulaCode.encode formula).length + 15)

Serialized generated output is bounded by the Barrington instruction bound times the source-code length needed for each terminated-unary variable field.

theorem Complexity.barringtonCompileCode_spec (formula : BoolFormula) : barringtonTargetBase ≠ 1 ∧ (∀ (assignment : ℕ → Bool), BP.eval assignment (barringtonCompile formula barringtonTargetBase) = if BoolFormula.eval assignment formula = true then barringtonTargetBase else 1) ∧ List.length (barringtonCompile formula barringtonTargetBase) ≤ 4 ^ formula.depth ∧ BPCode.Program.decode? (barringtonCompileCode (FormulaCode.encode formula)) = some (barringtonCompile formula barringtonTargetBase)

Bitstring-level constructive Barrington theorem. On the canonical code of a formula, the generated code decodes to the compiled program, which has exact formula semantics through the fixed target barringtonTargetBase (stated here only to be nonidentity; it is a 5-cycle by barringtonTargetBase_spec) and instruction count at most 4 ^ depth.