Documentation

Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalDeliver

Charged native output delivery for one traversal node #

The three actual heavy counts are read from the node allocation. The packed pointer is appended to the reserved output table and the fresh heap advances past all node output and scratch cells. Address computation is repeated explicitly instead of assuming scratch-register outputs that the node builder's public contract does not export.

Main definitions #

Main results #

The layout and native composition proofs are original.

source
def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState (x : WordRAM.Data 128) :
WordRAM.Data 128

All arithmetic results of the native delivery block, including its sole memory store.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState_mem (x : WordRAM.Data 128) :
    (deliveryState x).mem = Function.update x.mem (x.regs outputs + x.regs outputCount) (x.regs heap + 3 + x.regs (slot 2) + x.regs (slot 4) + x.regs (slot 6))

    Delivery writes exactly one output-pointer cell; all other memory retains the node output.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState_packed (x : WordRAM.Data 128) :
    (deliveryState x).regs packed = (NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))).packed

    The appended pointer is the existing node layout's packed base.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState_heap (x : WordRAM.Data 128) :
    (deliveryState x).regs heap = (NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))).endpoint

    All allocated node output, residues and histogram lie below the new fresh heap.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState_count (x : WordRAM.Data 128) :
    (deliveryState x).regs outputCount = x.regs outputCount + 1

    Exactly one node is appended to the output table.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState_heavy_length (x : WordRAM.Data 128) (j : Fin 3) :
    (deliveryState x).regs (heavyLength j) = x.mem ((NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))).descriptor j)

    Each delivered count was read from its actual count-prefixed heavy array.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState_heavy_base (x : WordRAM.Data 128) (j : Fin 3) :
    (deliveryState x).regs (heavyBase j) = (NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))).heavy j

    Each delivered data pointer is the existing heavy-array base.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.delivery_output (x : WordRAM.Data 128) (values : Fin 3 → ℕ → ℤ) (before : ℕ → ℕ) (h : NodePacking.Output (NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))) values before x.mem) (htable : x.regs outputs + x.regs outputCount < x.regs heap) :
    have L := NodePacking.layout (WordRAM.Data.comap kernel (nodeState x)); NodePacking.Output L values (Function.update before (x.regs outputs + x.regs outputCount) L.packed) (deliveryState x).mem

    Output delivery preserves the node builder's exact heavy/packed readback and allocation frame. The sole external output-pointer store is recorded explicitly in the before-memory.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.delivery_heavy_card (x : WordRAM.Data 128) (values : Fin 3 → ℕ → ℤ) (before : ℕ → ℕ) (h : NodePacking.Output (NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))) values before x.mem) (j : Fin 3) :
    (deliveryState x).regs (heavyLength j) = (ThreeSum.ChanHe.heavy (Finset.image (values j) (Finset.range ((NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))).n j))) (NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))).M).card

    The delivered register is the existing heavy-set cardinality, not a capacity or pair count.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliver_preserves (i : Fin 128) :
    i ≠ heap → i ≠ outputCount → i ≠ temporary → ↑i < 88 ∨ 96 ≤ ↑i → WordRAM.Code.Preserves i deliver

    All non-output controller parameters and the entire stack workspace survive delivery.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliveryState_preserves (x : WordRAM.Data 128) (i : Fin 128) (hh : i ≠ heap) (hc : i ≠ outputCount) (ht : i ≠ temporary) (hi : ↑i < 88 ∨ 96 ≤ ↑i) :
    (deliveryState x).regs i = x.regs i

    The explicit delivered state retains every non-output controller and stack register.

    source
    theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.deliver_exec {w : ℕ} (x : WordRAM.Data 128) (hone : x.regs one = 1) (htable : x.regs outputs + x.regs outputCount < x.regs heap) (hfit : WordRAM.Fits w (x.regs heap + 3 + 2 * (x.regs (slot 2) + x.regs (slot 4) + x.regs (slot 6)) + 4 * x.regs groups + x.regs selected)) :
    WordRAM.Exec w deliver x (deliveryState x) 24

    Every intermediate address and the output-count increment fit once the final endpoint fits. The output table precedes the fresh allocation, so its store cannot change a heavy-count load.