Canonical postfix encoding of Boolean formulas

This module exposes the machine-facing input format for the uniform Barrington generator. Formula nodes become a postfix stream of six three-bit token kinds; variable tokens carry a terminated-unary index, and a terminated-unary token count frames the complete stream.

The stack decoder is iterative, exact decoding is a left inverse, canonical serialization is injective, and the code-length equation records every bit.

Main results

• FormulaCode.run?_tokens -- postfix execution reconstructs a formula on any stack.
• FormulaCode.decode?_encode -- whole-formula round trip.
• FormulaCode.encode_injective -- canonical codes are unambiguous.
• FormulaCode.length_encode -- exact serialized length.

@[simp]

theorem Complexity.FormulaCode.Token.length_encode (token : Token) : token.encode.length = token.codeLength

The declared token cost is its exact encoded length.

@[simp]

theorem Complexity.FormulaCode.Token.decodePrefix?_encode_append (token : Token) (suffix : List Bool) : decodePrefix? (token.encode ++ suffix) = some (token, suffix)

Decoding an encoded token in front of any suffix recovers both.

theorem Complexity.FormulaCode.run?_append (first second : List Token) (stack : List BoolFormula) : run? (first ++ second) stack = (run? first stack).bind (run? second)

Running concatenated token streams is sequential stack execution.

@[simp]

theorem Complexity.FormulaCode.run?_tokens (formula : BoolFormula) (stack : List BoolFormula) : run? (tokens formula) stack = some (formula :: stack)

Running a formula's postfix tokens pushes exactly that formula.

@[simp]

theorem Complexity.FormulaCode.build?_tokens (formula : BoolFormula) : build? (tokens formula) = some formula

Building from a formula's postfix stream recovers the formula.

@[simp]

theorem Complexity.FormulaCode.length_tokens (formula : BoolFormula) : (tokens formula).length = formula.size

The postfix stream has one token per formula node.

@[simp]

theorem Complexity.FormulaCode.decodeTokens?_flatMap_encode_append (stream : List Token) (suffix : List Bool) : decodeTokens? stream.length (List.flatMap Token.encode stream ++ suffix) = some (stream, suffix)

Fixed-count token decoding consumes exactly the supplied encoded stream.

@[simp]

theorem Complexity.FormulaCode.decodePrefix?_encode_append (formula : BoolFormula) (suffix : List Bool) : decodePrefix? (encode formula ++ suffix) = some (formula, suffix)

Prefix decoding preserves a caller-supplied suffix.

@[simp]

theorem Complexity.FormulaCode.decode?_encode (formula : BoolFormula) : decode? (encode formula) = some formula

Exact decoding is a left inverse of canonical serialization.

theorem Complexity.FormulaCode.encode_injective : Function.Injective encode

Canonical formula serialization is injective.

theorem Complexity.FormulaCode.decode?_encode_append_eq_none (formula : BoolFormula) {suffix : List Bool} (hsuffix : suffix ≠ []) : decode? (encode formula ++ suffix) = none

Exact decoding rejects nonempty trailing data.

@[simp]

theorem Complexity.FormulaCode.length_encode (formula : BoolFormula) : (encode formula).length = formula.size + 1 + (List.map Token.codeLength (tokens formula)).sum

Exact formula-code length: one framed token count followed by every token.