GapCVP proof, part 03, continuation 02

def GapCVP.SourceStructuralDecoder.payloadValidTrace (payload suffix : List Bool) : StateTransition.EvalsToInTime payloadDecoderMachine.step (payloadConfiguration 0 (BinaryEncoding.lengthPrefixedWord payload ++ suffix) [] [] []) (some (Turing.haltList payloadDecoderMachine (true :: payload))) (3 * payload.length + suffix.length + 4)

Decode a valid length-prefixed payload and discard its suffix within a linear time bound.

Equations

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

def GapCVP.SourceTotalStructuralDecoder.payloadFailureTrace (input counter reversed output : List Bool) : StateTransition.EvalsToInTime SourceStructuralDecoder.payloadDecoderMachine.step (SourceStructuralDecoder.payloadConfiguration 4 input counter reversed output) (some (Turing.haltList SourceStructuralDecoder.payloadDecoderMachine (false :: output))) (input.length + counter.length + reversed.length + 1)

Clear the decoder's work stacks and halt with a failure flag.

Equations

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

def GapCVP.SourceTotalStructuralDecoder.payloadMissingPrefixTrace (count : ℕ) (counter reversed output : List Bool) : StateTransition.EvalsToInTime SourceStructuralDecoder.payloadDecoderMachine.step (SourceStructuralDecoder.payloadConfiguration 0 (List.replicate count true) counter reversed output) (some (SourceStructuralDecoder.payloadConfiguration 4 [] (List.replicate count true ++ counter) reversed output)) (count + 1)

Enter the failure state when the unary length prefix has no delimiter.

Equations

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

def GapCVP.SourceTotalStructuralDecoder.payloadMissingTrace (count : ℕ) : StateTransition.EvalsToInTime SourceStructuralDecoder.payloadDecoderMachine.step (SourceStructuralDecoder.payloadConfiguration 0 (List.replicate count true) [] [] []) (some (Turing.haltList SourceStructuralDecoder.payloadDecoderMachine [false])) (2 * count + 2)

Reject an input consisting entirely of a unary length prefix.

Equations

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

def GapCVP.SourceTotalStructuralDecoder.payloadPartialCopyTrace (payload remaining reversed output : List Bool) : StateTransition.EvalsToInTime SourceStructuralDecoder.payloadDecoderMachine.step (SourceStructuralDecoder.payloadConfiguration 1 payload (List.replicate payload.length true ++ remaining) reversed output) (some (SourceStructuralDecoder.payloadConfiguration 1 [] remaining (payload.reverse ++ reversed) output)) payload.length

Copy all available payload bits while retaining any unconsumed length counter.

Equations

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

def GapCVP.SourceTotalStructuralDecoder.payloadTruncatedTrace (payload : List Bool) (extra : ℕ) : StateTransition.EvalsToInTime SourceStructuralDecoder.payloadDecoderMachine.step (SourceStructuralDecoder.payloadConfiguration 0 (List.replicate (payload.length + extra + 1) true ++ false :: payload) [] [] []) (some (Turing.haltList SourceStructuralDecoder.payloadDecoderMachine [false])) (3 * payload.length + 2 * extra + 6)

Reject a payload shorter than its declared length within a linear time bound.

Equations

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

def GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput input = match GapCVP.BinaryEncoding.readLengthPrefixedWord input with | some (payload, snd) => true :: payload | none => [false]

@[simp]

theorem GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput_valid (payload suffix : List Bool) : payloadDecodeOutput (BinaryEncoding.lengthPrefixedWord payload ++ suffix) = true :: payload

@[simp]

theorem GapCVP.SourceTotalStructuralDecoder.readUnaryPrefix_missing (count : ℕ) : BinaryEncoding.readUnaryPrefix (List.replicate count true) = none

structure GapCVP.SourceTotalStructuralDecoder.MissingUnaryInput (input : List Bool) : Type

GapCVP reduction support.

• count : ℕ

  GapCVP reduction support.

• shape : input = List.replicate self.count true

structure GapCVP.SourceTotalStructuralDecoder.DelimitedUnaryInput (input : List Bool) : Type

GapCVP reduction support.

• count : ℕ

  GapCVP reduction support.

• tail : List Bool

  GapCVP reduction support.

• shape : input = List.replicate self.count true ++ false :: self.tail

def GapCVP.SourceTotalStructuralDecoder.unaryInputSplit (input : List Bool) : MissingUnaryInput input ⊕ DelimitedUnaryInput input

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceTotalStructuralDecoder.validInput_reconstruct (count : ℕ) (tail : List Bool) (hlen : count ≤ tail.length) : List.replicate count true ++ false :: tail = BinaryEncoding.lengthPrefixedWord (List.take count tail) ++ List.drop count tail

def GapCVP.SourceTotalStructuralDecoder.payloadTotalTrace (input : List Bool) : StateTransition.EvalsToInTime SourceStructuralDecoder.payloadDecoderMachine.step (SourceStructuralDecoder.payloadConfiguration 0 input [] [] []) (some (Turing.haltList SourceStructuralDecoder.payloadDecoderMachine (payloadDecodeOutput input))) (3 * input.length + 6)

A time-bounded decoder execution for every input, including malformed encodings.

Equations

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

noncomputable def GapCVP.SourceTotalStructuralDecoder.payloadDecoderComputable : BitTM payloadDecodeOutput

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceFormulaStructuralDecoder.dropHeadMachine : Turing.FinTM2

The single-step machine that removes the first bit of its input.

Equations

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

noncomputable def GapCVP.SourceFormulaStructuralDecoder.dropHeadComputable : BitTM List.tail

GapCVP reduction support.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.firstFieldContents (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceFormulaStructuralDecoder.firstFieldContents input = (GapCVP.SourceTotalStructuralDecoder.payloadDecodeOutput input).tail

noncomputable def GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable : BitTM firstFieldContents

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceFormulaStructuralDecoder.firstFieldContents_valid (payload suffix : List Bool) : firstFieldContents (BinaryEncoding.lengthPrefixedWord payload ++ suffix) = payload

@[reducible, inline]

abbrev GapCVP.SourceFormulaStructuralDecoder.suffixDecoderMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceFormulaStructuralDecoder.suffixConfiguration (phase : Fin 6) (input counter reversed output : List Bool) : suffixDecoderMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.SourceFormulaStructuralDecoder.suffixConfiguration phase input counter reversed output = { l := some phase, var := none, stk := ![input, counter, reversed, output] }

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_prefix_true (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 0 (true :: input) counter reversed output) = some (suffixConfiguration 0 input (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_prefix_delimiter (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 0 (false :: input) counter reversed output) = some (suffixConfiguration 1 input counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_prefix_missing_delimiter (counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 0 [] counter reversed output) = some (suffixConfiguration 5 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_copy_step (bit : Bool) (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 1 (bit :: input) (true :: counter) reversed output) = some (suffixConfiguration 1 input counter (bit :: reversed) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_insufficient (counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 1 [] (true :: counter) reversed output) = some (suffixConfiguration 5 [] (true :: counter) reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_counter_complete (input reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 1 input [] reversed output) = some (suffixConfiguration 2 input [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_discard_step (bit : Bool) (input reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 2 input [] (bit :: reversed) output) = some (suffixConfiguration 2 input [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_discard_complete (input output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 2 input [] [] output) = some (suffixConfiguration 3 input [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_collect_step (bit : Bool) (input reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 3 (bit :: input) [] reversed output) = some (suffixConfiguration 3 input [] (bit :: reversed) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_collect_complete (reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 3 [] [] reversed output) = some (suffixConfiguration 4 [] [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_restore_step (bit : Bool) (reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 4 [] [] (bit :: reversed) output) = some (suffixConfiguration 4 [] [] reversed (bit :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_restore_finish (output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 4 [] [] [] output) = some (Turing.haltList suffixDecoderMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_drop_input (bit : Bool) (input counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 (bit :: input) counter reversed output) = some (suffixConfiguration 5 input counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_drop_counter (bit : Bool) (counter reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 [] (bit :: counter) reversed output) = some (suffixConfiguration 5 [] counter reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_drop_reversed (bit : Bool) (reversed output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 [] [] (bit :: reversed) output) = some (suffixConfiguration 5 [] [] reversed output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceFormulaStructuralDecoder.suffix_failure_finish (output : List Bool) : suffixDecoderMachine.step (suffixConfiguration 5 [] [] [] output) = some (Turing.haltList suffixDecoderMachine output)

Internal support shared across GapCVP continuation modules.