The actual transcript of a pair of advice-bit executions

The transcript records both input states, all four first look-ahead outputs, both refreshed states, and all four second look-ahead outputs. The two advice bits are arbitrary. Both final outputs are right-only maps once these messages are fixed. The tampered final output is not included in this transcript: before advice first differs, it may equal the honest output.

The factors condition the original sources through two successive instances of the common look-ahead transcript. No source is resampled. These are the actual messages in Chattopadhyay--Goyal--Li Algorithm 1, used in the advice induction of Lemma 6.9: https://arxiv.org/pdf/1505.00107.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.FlipFlopFirstTranscript (Z : Type u_1) (L : ℕ) : Type u_1

Both initial states and all first-pass look-ahead outputs.

Equations

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

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.FlipFlopTranscript (Z : Type u_1) (L : ℕ) : Type u_1

Both complete look-ahead histories, before observing either final output.

Equations

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

def Algebraic.Cutwidth.Extractor.flipFlopHonestRefresh {Z : Type u_1} {B : Type u_3} (m L e : ℕ) (y : Z → B → Fin m → Bool) (b : Bool) (t : FlipFlopFirstTranscript Z L) (u : B) : Fin (matchedBlockOutputBits 64 L) → Bool

The honest first refresh is right-only after fixing the first transcript.

Equations

• Algebraic.Cutwidth.Extractor.flipFlopHonestRefresh m L e y b t u = Algebraic.Cutwidth.Extractor.matchedBlockExtractor m 64 L e (y t.1.1 u) (if b = true then t.2.1.2 else t.2.1.1)

def Algebraic.Cutwidth.Extractor.flipFlopTamperedRefresh {Z : Type u_1} {B : Type u_3} (m L e : ℕ) (y' : Z → B → Fin m → Bool) (b' : Bool) (t : FlipFlopFirstTranscript Z L) (u : B) : Fin (matchedBlockOutputBits 64 L) → Bool

The tampered first refresh uses its own advice bit and the original right source.

Equations

• Algebraic.Cutwidth.Extractor.flipFlopTamperedRefresh m L e y' b' t u = Algebraic.Cutwidth.Extractor.matchedBlockExtractor m 64 L e (y' t.1.1 u) (if b' = true then t.2.2.2 else t.2.2.1)

def Algebraic.Cutwidth.Extractor.flipFlopTranscript {Z : Type u_1} {A : Type u_2} {B : Type u_3} (n m L e : ℕ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) (p : (Z × B) × A) : FlipFlopTranscript Z L

The actual two-pass transcript of arbitrary honest and tampered advice bits.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopFirstWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} (n L e : ℕ) [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) : FlipFlopFirstTranscript Z L → ℝ

The exact first transcript weight from the original factors.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopFirstLeft {Z : Type u_1} {A : Type u_2} (n L e : ℕ) [Fintype A] (l : Z → A → ℝ) (x x' : Z → A → Fin n → Bool) : FlipFlopFirstTranscript Z L → A → ℝ

The original left-source kernel conditioned on the first transcript.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopFirstRight {Z : Type u_1} {B : Type u_3} (L : ℕ) [Fintype B] (r : Z → B → ℝ) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) : FlipFlopFirstTranscript Z L → B → ℝ

The original right-source kernel conditioned on the first input pair.

Equations

• Algebraic.Cutwidth.Extractor.flipFlopFirstRight L r q q' = Algebraic.Cutwidth.Extractor.lookAheadBaseRight r q q'

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopTranscriptWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} (n m L e : ℕ) [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) : FlipFlopTranscript Z L → ℝ

The actual two-pass transcript weight for arbitrary advice bits.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopTranscriptLeft {Z : Type u_1} {A : Type u_2} (n L e : ℕ) [Fintype A] (l : Z → A → ℝ) (x x' : Z → A → Fin n → Bool) : FlipFlopTranscript Z L → A → ℝ

The original left-source kernel conditioned on both look-ahead histories.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopTranscriptRight {Z : Type u_1} {B : Type u_3} (m L e : ℕ) [Fintype B] (r : Z → B → ℝ) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) : FlipFlopTranscript Z L → B → ℝ

The original right-source kernel conditioned on both pairs of right states.

Equations

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

def Algebraic.Cutwidth.Extractor.flipFlopHonestOutput {Z : Type u_1} {B : Type u_3} (m L e : ℕ) (y : Z → B → Fin m → Bool) (b : Bool) (t : FlipFlopTranscript Z L) (u : B) : Fin (matchedBlockOutputBits 64 L) → Bool

The honest final output is right-only once its final seed is recorded.

Equations

• Algebraic.Cutwidth.Extractor.flipFlopHonestOutput m L e y b t u = Algebraic.Cutwidth.Extractor.matchedBlockExtractor m 64 L e (y t.1.1.1.1 u) (if b = true then t.2.1.1 else t.2.1.2)

def Algebraic.Cutwidth.Extractor.flipFlopTamperedOutput {Z : Type u_1} {B : Type u_3} (m L e : ℕ) (y' : Z → B → Fin m → Bool) (b' : Bool) (t : FlipFlopTranscript Z L) (u : B) : Fin (matchedBlockOutputBits 64 L) → Bool

The tampered final output is right-only once its final seed is recorded.

Equations

• Algebraic.Cutwidth.Extractor.flipFlopTamperedOutput m L e y' b' t u = Algebraic.Cutwidth.Extractor.matchedBlockExtractor m 64 L e (y' t.1.1.1.1 u) (if b' = true then t.2.2.1 else t.2.2.2)

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopTranscriptLeftEnvelope {Z : Type u_1} {B : Type u_3} (m L e : ℕ) [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : Bool) : FlipFlopTranscript Z L → ℝ

The original left envelope updated by the two exact common transcripts.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.flipFlopTranscriptRightEnvelope {Z : Type u_1} {A : Type u_2} (n L e : ℕ) [Fintype A] (ν : Z → ℝ) (l : Z → A → ℝ) (x x' : Z → A → Fin n → Bool) : FlipFlopTranscript Z L → ℝ

The original right envelope updated by both four-output left messages.

Equations

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