def Hex.PermGroup.Program.encodeNode : Node → Lean.Json

Wire format: identity [0], generator [1,i], inverse [2,i], and product [3,i,j]. Indices are exact natural numbers.

Equations

• Hex.PermGroup.Program.encodeNode Hex.PermGroup.Node.id = Lean.toJson #[0]
• Hex.PermGroup.Program.encodeNode (Hex.PermGroup.Node.generator i) = Lean.toJson #[1, i]
• Hex.PermGroup.Program.encodeNode (Hex.PermGroup.Node.inv i) = Lean.toJson #[2, i]
• Hex.PermGroup.Program.encodeNode (Hex.PermGroup.Node.comp i j) = Lean.toJson #[3, i, j]

def Hex.PermGroup.Program.encode (program : Program) : String

Encode the raw program as a versioned JSON object.

Equations

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

def Hex.PermGroup.Program.decodeNode (generatorCount earlier : Nat) (json : Lean.Json) : Except String Node

Decode a node, rejecting references outside the already decoded prefix.

Equations

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

def Hex.PermGroup.Program.decode (maxBytes maxNodes generatorCount : Nat) (input : String) : Except String Program

Decode within explicit byte and node limits. The byte limit is checked before JSON parsing, and the node limit before constructing program nodes. All references are validated, including nodes unreachable from the root.

Equations

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