LanglibCorrectness and uniqueness of the boot transition #
The boot scanner has no certificate choices: on a nonempty encoded input row it accepts exactly the canonical initialized protocol row.
theorem
CertifiedRowSystem.Complement.isBoot_phases_length
{A : Type u_1}
[Fintype A]
[Nonempty A]
[DecidableEq A]
{old new : ProtocolRow A}
(hboot : IsBoot old new)
:
HasPhase ProtocolPhase.input old ∧ HasPhase ProtocolPhase.roundStart new ∧ List.length old = List.length new
Any successful boot scan starts in the replicated input phase, ends in the replicated round-start phase, and preserves row width.
@[simp]
theorem
CertifiedRowSystem.Complement.isBoot_input_iff_eq_initialized
{I : Type u_1}
{A : Type u_2}
[Fintype A]
[Nonempty A]
[DecidableEq A]
(sourceCell : I → A)
{input : List I}
(hne : input ≠ [])
(new : ProtocolRow A)
:
IsBoot (List.map (inputProtocolCell sourceCell) input) new ↔ new = initializedProtocolRow (List.map sourceCell input)
On a nonempty encoded input row, boot acceptance uniquely determines the canonical initialized row.
theorem
CertifiedRowSystem.Complement.isInitialized_of_isBoot_input
{I : Type u_1}
{A : Type u_2}
[Fintype A]
[Nonempty A]
[DecidableEq A]
(sourceCell : I → A)
{input : List I}
(hne : input ≠ [])
{new : ProtocolRow A}
(hboot : IsBoot (List.map (inputProtocolCell sourceCell) input) new)
:
IsInitialized (List.map sourceCell input) new
A successful boot from an encoded input establishes the full initialization invariant.
theorem
CertifiedRowSystem.Complement.isBoot_input_phases_length
{I : Type u_1}
{A : Type u_2}
[Fintype A]
[Nonempty A]
[DecidableEq A]
(sourceCell : I → A)
{input : List I}
(hne : input ≠ [])
{new : ProtocolRow A}
(hboot : IsBoot (List.map (inputProtocolCell sourceCell) input) new)
:
HasPhase ProtocolPhase.input (List.map (inputProtocolCell sourceCell) input) ∧ HasPhase ProtocolPhase.roundStart new ∧ (List.map (inputProtocolCell sourceCell) input).length = List.length new
Phase and width projections of a successful boot from an encoded input.