Exact composition laws for the advice chain #
The concrete chain processes advice in its given order and preserves its
original sources. These algebraic laws do not supply the statistical chain
invariant needed for correlation breaking; Advice.Extraction proves that
guarantee (adviceCorrelationBreaker_dist_le).
theorem
Algebraic.Cutwidth.Extractor.adviceFold_nil
(n m L e : ℕ)
(x : Fin n → Bool)
(y : Fin m → Bool)
(q : Fin (matchedBlockOutputBits 64 L) → Bool)
:
Empty advice preserves the supplied initial state.
theorem
Algebraic.Cutwidth.Extractor.adviceFold_cons
(n m L e : ℕ)
(x : Fin n → Bool)
(y : Fin m → Bool)
(q : Fin (matchedBlockOutputBits 64 L) → Bool)
(b : Bool)
(advice : List Bool)
:
adviceFold n m L e x y q (b :: advice) = adviceFold n m L e x y (flipFlopStep n m L e x y q b) advice
The first advice bit is processed before the remaining advice.
theorem
Algebraic.Cutwidth.Extractor.adviceFold_append
(n m L e : ℕ)
(x : Fin n → Bool)
(y : Fin m → Bool)
(q : Fin (matchedBlockOutputBits 64 L) → Bool)
(first last : List Bool)
:
adviceFold n m L e x y q (first ++ last) = adviceFold n m L e x y (adviceFold n m L e x y q first) last
Concatenating advice composes its two consecutive folds.