Pure Barrington code-generator internals

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

Internal bound placing every referenced variable below the formula-code length.

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

Internal exact action of the code generator on a canonical formula code.

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

Internal decoding theorem for generated program code.

theorem Complexity.length_barringtonCompileCode_encode_internal (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

Internal exact output-code length on canonical formula input.

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

Internal serialized-output bound in terms of formula-code length and depth. The extra factor comes from the terminated-unary variable field in each instruction.

theorem Complexity.barringtonCompileCode_spec_internal (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)

Internal combined semantic and program-length specification of generated code on canonical formula input.