Copying a bit block without consuming the source

DefinitionTwo-destination bit-block transfer#✓fully proved

Pop a bit block onto two distinct destinations, reversing both copies.

def splitB (a b c : K) (d : Γ a → Option Bool)
    (gb : Bool → Γ b) (gc : Bool → Γ c) (self next : Λ) :
    TM2.Stmt Γ Λ Bool :=
  .peek a (fun _ o => isBit d o) <| .branch id
    (.pop a (fun _ o => bitOf d o) <|
      .push b gb <| .push c gc <| .goto fun _ => self)
    (.goto fun _ => next)

Uses 2 · Used by 3

Statement usesBit on top of a stack · Bit test for the top of a stack

Used byBit-block copy keeps the order and restores source and scratch · Two-destination bit transfer takes one step per bit plus one · Program of the raw-input SUBSET-SUM to PARTITION machine

TheoremTwo-destination bit transfer takes one step per bit plus one#✓fully proved

Two-destination bit transfer takes one step per bit plus one, with exact suffix and unrelated-stack preservation.

theorem splitB_run {M : Λ → TM2.Stmt Γ Λ Bool}
    {a b c : K} {d : Γ a → Option Bool}
    {gb : Bool → Γ b} {gc : Bool → Γ c} {self next : Λ}
    (hM : M self = splitB a b c d gb gc self next)
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (ga : Bool → Γ a) (hga : ∀ bit, d (ga bit) = some bit)
    (p : List Bool) : ∀ (tail : List (Γ a)) (v : Bool)
      (S : ∀ k, List (Γ k)), EndsBitBlock d tail →
      S a = p.map ga ++ tail →
      ∃ S', Run M (p.length + 1) ⟨some self, v, S⟩
        ⟨some next, false, S'⟩ ∧ S' a = tail ∧
        S' b = (p.map gb).reverse ++ S b ∧
        S' c = (p.map gc).reverse ++ S c ∧
        ∀ k, k ≠ a → k ≠ b → k ≠ c → S' k = S k

Uses 6 · Used by 1

Statement usesTwo-destination bit-block transfer · End of a bit block · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label · Bit on top of a stack · Bit test for the top of a stack

Used byBit-block copy keeps the order and restores source and scratch

TheoremBit-block copy keeps the order and restores source and scratch#✓fully proved

Copy a bit block in its original order, restoring both the source and scratch, in exactly 2 * p.length + 2 steps.

Cslib.Complexity.PolynomialEncoding.copyB_run · 16 lines

theorem copyB_run {M : Λ → TM2.Stmt Γ Λ Bool}
    {a b t : K} {da : Γ a → Option Bool} {dt : Γ t → Option Bool}
    {ga : Bool → Γ a} {gb : Bool → Γ b} {gt : Bool → Γ t}
    {first second next : Λ}
    (h₁ : M first = moveB a t da gt first second)
    (h₂ : M second = splitB t a b dt ga gb second next)
    (hab : a ≠ b) (hat : a ≠ t) (hbt : b ≠ t)
    (hga : ∀ bit, da (ga bit) = some bit)
    (hgt : ∀ bit, dt (gt bit) = some bit)
    (p : List Bool) (tail : List (Γ a)) (v : Bool)
    (S : ∀ k, List (Γ k)) (ha : S a = p.map ga ++ tail)
    (htail : EndsBitBlock da tail) (ht : EndsBitBlock dt (S t)) :
    ∃ S', Run M (2 * p.length + 2) ⟨some first, v, S⟩
      ⟨some next, false, S'⟩ ∧ S' a = S a ∧ S' t = S t ∧
      S' b = p.map gb ++ S b ∧
      ∀ k, k ≠ a → k ≠ b → k ≠ t → S' k = S k

Uses 7 · Used by 1

Statement usesTwo-destination bit-block transfer · End of a bit block · Flag bit of a machine state · Exact-length runs of a TM2 machine · Bit-moving loop

Proof usesTwo-destination bit transfer takes one step per bit plus one · Running the bit-moving loop

Used byQuadratic run of the raw-input SUBSET-SUM to PARTITION machine

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.