A second-output refresh with an arbitrary left-only tampered seed #
The actual transcript records the left-only leak, original right input, tampered refresh, and both honest look-ahead outputs. The honest refresh uses the second output and reads the original right source. The output law also retains the entire original left state. Every value is computed from the original factored source law, without independently resampling a source.
@[reducible, inline]
abbrev
Algebraic.Cutwidth.Extractor.FixedTamperingSecondTranscript
(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 observation, then both honest look-ahead outputs.
Equations
Instances For
def
Algebraic.Cutwidth.Extractor.fixedTamperingSecondHonestMessage
{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)
(QExt : Q → Mid → Seed)
(t : (Z × Mid) × Q × Out)
(a : A)
:
Both honest look-ahead outputs are left-only once the original right input is fixed.
Equations
- Algebraic.Cutwidth.Extractor.fixedTamperingSecondHonestMessage x initialSeed W QExt t a = (W (x t.1.1 a) (initialSeed t.2.1), W (x t.1.1 a) (QExt t.2.1 (W (x t.1.1 a) (initialSeed t.2.1))))
Instances For
def
Algebraic.Cutwidth.Extractor.fixedTamperingSecondTranscriptValue
{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)
(QExt : Q → Mid → Seed)
(R : Y → Mid → Out)
(z : Z)
(a : A)
(b : B)
:
FixedTamperingSecondTranscript Z Q Mid Out
The actual full transcript computed from the original left and right states.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.Cutwidth.Extractor.fixedTamperingSecondRefreshWeight
{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)
(QExt : Q → Mid → Seed)
(R : Y → Mid → Out)
:
(FixedTamperingSecondTranscript Z Q Mid Out × A) × Out → ℝ
The honest second-output refresh retaining the full transcript and original left state.
Equations
- One or more equations did not get rendered due to their size.