Refreshing against a fixed left-side tampered seed

The transcript records a left-only tampered seed, the original right input to the initial-seed map, the tampered refresh, and the honest first output. The original left and right states are retained in the factored law. The refresh law additionally retains the full left state and outputs the actual honest refresh, without replacing either source by fresh randomness.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.FixedTamperingTranscript (Z : Type u_10) (Q : Type u_11) (Mid : Type u_12) (Out : Type u_13) : Type (max (max (max u_13 u_11) u_12 u_10) u_12)

Original tag and left leak, then right input and tampered refresh, then honest first output.

Equations

• Algebraic.Cutwidth.Extractor.FixedTamperingTranscript Z Q Mid Out = (((Z × Mid) × Q × Out) × Mid)

def Algebraic.Cutwidth.Extractor.fixedTamperingRightMessage {Z : Type u_1} {B : Type u_3} {Q : Type u_5} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} (q : Z → B → Q) (y' : Z → B → Y) (R : Y → Mid → Out) (zm : Z × Mid) (b : B) : Q × Out

Once the left leak is fixed, both the right input and tampered refresh are right messages.

Equations

• Algebraic.Cutwidth.Extractor.fixedTamperingRightMessage q y' R zm b = (q zm.1 b, R (y' zm.1 b) zm.2)

def Algebraic.Cutwidth.Extractor.fixedTamperingHonestMessage {Z : Type u_1} {A : Type u_2} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Out : Type u_9} (x : Z → A → X) (initialSeed : Q → Seed) (W : X → Seed → Mid) (t : (Z × Mid) × Q × Out) (a : A) : Mid

Once the right input is fixed, the honest first output is a left message.

Equations

• Algebraic.Cutwidth.Extractor.fixedTamperingHonestMessage x initialSeed W t a = W (x t.1.1 a) (initialSeed t.2.1)

def Algebraic.Cutwidth.Extractor.fixedTamperingTranscriptValue {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} (x : Z → A → X) (q : Z → B → Q) (y' : Z → B → Y) (leak : Z → A → Mid) (initialSeed : Q → Seed) (W : X → Seed → Mid) (R : Y → Mid → Out) (z : Z) (a : A) (b : B) : FixedTamperingTranscript Z Q Mid Out

The actual transcript computed from the original pair of states.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.fixedTamperingTranscriptWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (q : Z → B → Q) (y' : Z → B → Y) (leak : Z → A → Mid) (initialSeed : Q → Seed) (W : X → Seed → Mid) (R : Y → Mid → Out) : FixedTamperingTranscript Z Q Mid Out → ℝ

Exact transcript weights after the left, right, and final left observations.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.fixedTamperingLeft {Z : Type u_1} {A : Type u_2} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Out : Type u_9} [Fintype A] (l : Z → A → ℝ) (x : Z → A → X) (leak : Z → A → Mid) (initialSeed : Q → Seed) (W : X → Seed → Mid) : FixedTamperingTranscript Z Q Mid Out → A → ℝ

The normalized original left-state kernel after all observations.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.fixedTamperingRight {Z : Type u_1} {B : Type u_3} {Q : Type u_5} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} [Fintype B] (r : Z → B → ℝ) (q : Z → B → Q) (y' : Z → B → Y) (R : Y → Mid → Out) (t : FixedTamperingTranscript Z Q Mid Out) : B → ℝ

The normalized original right-state kernel after its observed input and tampered refresh.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.fixedTamperingRefreshWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} {Out : Type u_9} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (q : Z → B → Q) (y y' : Z → B → Y) (leak : Z → A → Mid) (initialSeed : Q → Seed) (W : X → Seed → Mid) (R : Y → Mid → Out) : (FixedTamperingTranscript Z Q Mid Out × A) × Out → ℝ

The actual honest refresh, retaining the full transcript and original left state.

Equations

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