Imports
/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module
public import Geb.Prototypes.Computability.BitTree.Encoding -- shake: keepset_option doc.verso trueBoundary cases of the binary-tree encoding
These calculations exercise tree tags, both payload bit values, string terminators, incomplete input and trailing input.
Main statements
-
The empty string is a valid leaf payload, while an empty input is invalid.
-
Forks may have empty or nonempty leaf payloads.
-
Truncated escapes, unfinished forks and trailing trees are rejected.
Tags
binary tree, encoding, recognizer, boundary cases
public sectionnamespace Geb.BitTreeexample : encode (leaf []) = [false, false] := rflexample : encode (leaf [false, true]) = [false, true, false, true, true, false] := rflexample : encode (fork (leaf []) (leaf [])) = [true, false, false, false, false] := rflexample : validBool [] = false := rflexample : validBool [false, false] = true := rflexample : validBool [false, true, false, true, true, false] = true := rflexample : validBool [true, false, false, false, false] = true := rflexample : validBool [false, true] = false := rflexample : validBool [false, true, false] = false := rflexample : validBool [true, false, false] = false := rflexample : validBool [false, false, false, false] = false := rflend Geb.BitTree