Pair-encoding validator — definitions

This file defines a finite-state scanner for the image of the library's self-delimiting binary pair codec. Unlike pairSplitCoreTM, the validator has total semantics: it writes 1 exactly when unpair? succeeds and writes 0 on every malformed encoding.

def Complexity.validPairEncoding : Language

The language of strings on which the canonical pair decoder succeeds.

Equations

• Complexity.validPairEncoding = {z : List Bool | (Complexity.unpair? z).isSome = true}

inductive Complexity.TM.PairValidateState : Type

Finite control for recognizing the doubled prefix and 01 separator of a pair encoding. Once the separator has been seen, every remaining bit belongs to the unrestricted right component.

• next : PairValidateState

  Expect the first copy of the next doubled bit.

• afterZero : PairValidateState

  The first copy was 0; 0 continues the prefix and 1 is the separator.

• afterOne : PairValidateState

  The first copy was 1; only a second 1 is valid.

• suffix : PairValidateState

  The separator has been seen; the remaining suffix is unrestricted.

• invalid : PairValidateState

  A mismatched doubled bit was seen.

@[implicit_reducible]

instance Complexity.TM.instDecidableEqPairValidateState : DecidableEq PairValidateState

Equations

• Complexity.TM.instDecidableEqPairValidateState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypePairValidateState : Fintype PairValidateState

Equations

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

def Complexity.TM.pairValidateStep : PairValidateState → Bool → PairValidateState

One automaton step for the pair-encoding validator.

Equations

• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.next false = Complexity.TM.PairValidateState.afterZero
• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.next true = Complexity.TM.PairValidateState.afterOne
• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.afterZero false = Complexity.TM.PairValidateState.next
• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.afterZero true = Complexity.TM.PairValidateState.suffix
• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.afterOne false = Complexity.TM.PairValidateState.invalid
• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.afterOne true = Complexity.TM.PairValidateState.next
• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.suffix x✝ = Complexity.TM.PairValidateState.suffix
• Complexity.TM.pairValidateStep Complexity.TM.PairValidateState.invalid x✝ = Complexity.TM.PairValidateState.invalid

def Complexity.TM.pairValidateAccept : PairValidateState → Bool

The scanner accepts exactly after it has seen the pair separator.

Equations

• Complexity.TM.pairValidateAccept Complexity.TM.PairValidateState.suffix = true
• Complexity.TM.pairValidateAccept x✝ = false

def Complexity.TM.pairValidateTM : TM 0

A total, zero-work-tape validator for the image of pair.

The generic scanner consumes the whole input, folds pairValidateStep in finite control, and writes the final Boolean verdict to output cell 1.

Equations

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