Canonical fixed-width protocol rows

This file packages the routine construction of a protocol row from its synchronous tracks. The function-indexed constructor is the primitive operation; the list-based wrapper is convenient when an action copies most tracks from an existing row.

def CertifiedRowSystem.Complement.listToFixed {X : Type u_1} (xs : List X) : Fin xs.length → X

Regard a list as a function on its canonical finite index type.

Equations

• CertifiedRowSystem.Complement.listToFixed xs = xs.get

@[simp]

theorem CertifiedRowSystem.Complement.ofFn_listToFixed {X : Type u_1} (xs : List X) : List.ofFn (listToFixed xs) = xs

def CertifiedRowSystem.Complement.listToFixedCast {X : Type u_1} (xs : List X) {width : ℕ} (h : xs.length = width) : Fin width → X

Reindex a list by any propositionally equal width.

Equations

• CertifiedRowSystem.Complement.listToFixedCast xs h i = xs.get (Fin.cast ⋯ i)

@[simp]

theorem CertifiedRowSystem.Complement.ofFn_listToFixedCast {X : Type u_1} (xs : List X) {width : ℕ} (h : xs.length = width) : List.ofFn (listToFixedCast xs h) = xs

def CertifiedRowSystem.Complement.canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : ProtocolRow A

Build a protocol row of fixed width from all nine track functions and replicated found/phase values.

Equations

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

@[simp]

theorem CertifiedRowSystem.Complement.length_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : List.length (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = width

@[simp]

theorem CertifiedRowSystem.Complement.sourceTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : sourceTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn source

@[simp]

theorem CertifiedRowSystem.Complement.depthTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : depthTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn depth

@[simp]

theorem CertifiedRowSystem.Complement.outerTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : outerTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn outer

@[simp]

theorem CertifiedRowSystem.Complement.innerTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : innerTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn inner

@[simp]

theorem CertifiedRowSystem.Complement.pathTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : pathTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn path

@[simp]

theorem CertifiedRowSystem.Complement.fuelTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : fuelTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn fuel

@[simp]

theorem CertifiedRowSystem.Complement.oldCountTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : oldCountTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn oldCount

@[simp]

theorem CertifiedRowSystem.Complement.newCountTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : newCountTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn newCount

@[simp]

theorem CertifiedRowSystem.Complement.seenCountTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : seenCountTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.ofFn seenCount

@[simp]

theorem CertifiedRowSystem.Complement.foundTrack_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : foundTrack (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase) = List.replicate width found

@[simp]

theorem CertifiedRowSystem.Complement.hasFound_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : HasFound found (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase)

@[simp]

theorem CertifiedRowSystem.Complement.hasPhase_canonicalProtocolRow {A : Type u_1} [Fintype A] {width : ℕ} (source depth outer inner path fuel : Fin width → A) (oldCount newCount seenCount : Fin width → CountDigit A) (found : Bool) (phase : ProtocolPhase) : HasPhase phase (canonicalProtocolRow source depth outer inner path fuel oldCount newCount seenCount found phase)

structure CertifiedRowSystem.Complement.ProtocolTrackLists (A : Type u_1) [Fintype A] : Type u_1

Nine concrete track lists sharing the source-list width.

• source : List A
• depth : List A
• outer : List A
• inner : List A
• path : List A
• fuel : List A
• oldCount : List (CountDigit A)
• newCount : List (CountDigit A)
• seenCount : List (CountDigit A)
• depth_length : self.depth.length = self.source.length
• outer_length : self.outer.length = self.source.length
• inner_length : self.inner.length = self.source.length
• path_length : self.path.length = self.source.length
• fuel_length : self.fuel.length = self.source.length
• oldCount_length : self.oldCount.length = self.source.length
• newCount_length : self.newCount.length = self.source.length
• seenCount_length : self.seenCount.length = self.source.length

def CertifiedRowSystem.Complement.protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : ProtocolRow A

Build a canonical row directly from equal-width concrete track lists.

Equations

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

@[simp]

theorem CertifiedRowSystem.Complement.length_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : List.length (protocolRowOfTracks tracks found phase) = tracks.source.length

@[simp]

theorem CertifiedRowSystem.Complement.sourceTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : sourceTrack (protocolRowOfTracks tracks found phase) = tracks.source

@[simp]

theorem CertifiedRowSystem.Complement.depthTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : depthTrack (protocolRowOfTracks tracks found phase) = tracks.depth

@[simp]

theorem CertifiedRowSystem.Complement.outerTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : outerTrack (protocolRowOfTracks tracks found phase) = tracks.outer

@[simp]

theorem CertifiedRowSystem.Complement.innerTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : innerTrack (protocolRowOfTracks tracks found phase) = tracks.inner

@[simp]

theorem CertifiedRowSystem.Complement.pathTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : pathTrack (protocolRowOfTracks tracks found phase) = tracks.path

@[simp]

theorem CertifiedRowSystem.Complement.fuelTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : fuelTrack (protocolRowOfTracks tracks found phase) = tracks.fuel

@[simp]

theorem CertifiedRowSystem.Complement.oldCountTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : oldCountTrack (protocolRowOfTracks tracks found phase) = tracks.oldCount

@[simp]

theorem CertifiedRowSystem.Complement.newCountTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : newCountTrack (protocolRowOfTracks tracks found phase) = tracks.newCount

@[simp]

theorem CertifiedRowSystem.Complement.seenCountTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : seenCountTrack (protocolRowOfTracks tracks found phase) = tracks.seenCount

@[simp]

theorem CertifiedRowSystem.Complement.foundTrack_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : foundTrack (protocolRowOfTracks tracks found phase) = List.replicate tracks.source.length found

@[simp]

theorem CertifiedRowSystem.Complement.hasFound_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : HasFound found (protocolRowOfTracks tracks found phase)

@[simp]

theorem CertifiedRowSystem.Complement.hasPhase_protocolRowOfTracks {A : Type u_1} [Fintype A] (tracks : ProtocolTrackLists A) (found : Bool) (phase : ProtocolPhase) : HasPhase phase (protocolRowOfTracks tracks found phase)