Table of Contents
The preceding sections converge on five properties that the pipeline tool must track per step and propagate through the chain:
- Invertibility class: bijection, injection, surjection, or general map. Derived from the mathematical properties of the transform function.
- Key dependency: does the inverse require an external value (decryption key, initialization vector, salt) not present in the forward output? AES-encrypt is bijective given the key, but the key is not carried in the ciphertext by default.
- Domain restriction: is the inverse defined on all outputs of the forward function, or only on a subset? gzip decompress is defined only on valid compressed data.
- State dependency: does the operation depend on mutable external state (a counter, a timestamp, a random nonce)? If so, the inverse requires reconstructing that state.
- Chain reversibility: the chain is reversible if and only if every step is bijective and none introduce external dependencies that are not threaded through the pipeline.
The visual representation should propagate a traffic-light model: green for bijective steps, amber for injective or key-dependent steps, red for surjective or hash steps. The chain's overall indicator is the minimum (most pessimistic) of its step indicators. A single MD5 in a chain of otherwise bijective operations makes the whole chain irreversible.
1. Enforcement Spectrum: Who Guarantees the Inverse?
The encode tool's :inverse? true flag is a claim, not a proof. The
question is where in the stack the guarantee lives. Languages differ in how
strongly they enforce that decode ∘ encode = id:
| Language | Mechanism | Enforcement |
|---|---|---|
| Uiua | ° (un) operator (??, ????) |
Compiler derives the inverse from language semantics |
| Janus | Every statement has a defined inverse (??, a) | Syntax enforces reversibility – if it compiles, it's invertible |
| Haskell | Iso type in lens libraries (??, a) |
Type-level – Iso s t a b is a pair the type checker verifies |
| Lean 4 | Dependent types (Equiv) |
Proven for all inputs – spec/codecproofs/ (two-sided Equiv) |
| Dafny | Auto-active ensures + SMT (Z3) |
Proven for all inputs – involution/round-trip as one ensures Z3 closes |
| Racket | Contracts (??, a) | Runtime-checked pre/post conditions with blame |
| Clojure | PBT (test.check) (??, a) | Empirical – 100 random inputs, not a proof |
At the top of this spectrum (Uiua, Janus), the language knows the inverse and can derive it mechanically. At the bottom (Clojure, JavaScript), the programmer asserts it and PBT searches for counterexamples.
Three of these points are now built, not hypothetical, for the same codecs:
Lean (spec/codecproofs/, a two-sided Equiv), Dafny
(the transducer lab, auto-active ensures Z3 discharges), and Racket
(transform-tool-racket, contracts with Findler–Felleisen blame) – the same
decode ∘ encode = id claim guaranteed at three different points in the stack.
The Lean/Dafny split is itself the Dafny 2026 question: interactive dependent
types vs. auto-active SMT, same theorem.
The encode tool operates at the Clojure level: the :inverse? flag is a manual
annotation, and the property-based tests verify it empirically. The green
indicator means "annotated as bijective and PBT hasn't found a counterexample" –
not "proven bijective." This is the same epistemological status as any
PBT-verified property: high confidence, not certainty.
The practical consequence: some inputs might work even when the codec is
marked irreversible. upper/decode (lowercase) applied to an already-lowercase
string is a perfect round-trip. sort/decode on a string that was already
sorted is the identity. The irreversibility flag is about the worst case over
the entire input domain, not about any specific input. A codec that fails for
even one input is not a bijection – but it may be bijective on a subdomain, and
the tool does not yet track domain restrictions (property 3 above).
CyberChef is the closest deployed tool. The improvement is the explicit reversibility annotation at every step, derived from the operation's mathematical classification, not from the user's knowledge. The intellectual lineage – from Forth to group theory to Janus to quantum gates – all points toward the same abstraction: a pipeline step is a morphism, and the pipeline's reversibility is a property of the morphism's category.
Formal verification of these properties is tractable. TLA+ specifications can model the state machine of encode/decode transitions with invariants about information preservation. Alloy can enforce structural constraints on stage composition. See PLDI 2026 (PAgE workshop on agentic engineering foundations) and BugBash 2026 (Nada Amin on dependent types, Gabriela Moreira on Quint/TLA+) for venues where this work connects to active research.