Indexed Binary Min-Heap: Exact-Basis Word-RAM Program

This file defines the structured word-RAM code (Cslib.WordRAM.Code .exact 25) and PQCode calling convention for the standalone indexed binary min-heap on rBin = 25 registers.

Registers 0..4 (baseReg, nReg, hb, pb, sz) are persistent (input = false); registers 5..24 (frontierReg, tags, arguments, outputs, constants, and sift scratch registers) are caller-overwritable (input = true). Parent positions are computed via p ← k >>> one (k >>> 1 = k / 2), so no constant larger than 1 is ever loaded and all operations succeed at every word width w with Fits w (base + space n) and Fits w K_max (including n = 0, w = 1).

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.rBin: register count (25).
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftUp, Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftDown: heap-order restoration loops.
• Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.pqCode: packaged PQCode .exact rBin.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.rBin : ℕ

Total register count of the standalone binary heap (5 persistent + 20 caller/scratch).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.baseReg : Fin rBin

Persistent base address base of the key array ([base, base + n)).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.nReg : Fin rBin

Persistent handle bound n.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.hb : Fin rBin

Persistent heap array base base + n (slots 1..sz at base + n + i).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.pb : Fin rBin

Persistent pos array base base + 2 * n + 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.sz : Fin rBin

Persistent current heap size sz ≤ n.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.frontierReg : Fin rBin

Bump-allocation frontier register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.tag2 : Fin rBin

High operation-tag bit (1 iff extractMin).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.tag1 : Fin rBin

Middle operation-tag bit (1 iff insert or decreaseKey).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.tag0 : Fin rBin

Low operation-tag bit.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.argV : Fin rBin

Input handle argument v.val.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.argK : Fin rBin

Input key argument k.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.outFlag : Fin rBin

Output status/presence flag (output register).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.outV : Fin rBin

Output handle register (extractMin).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.outK : Fin rBin

Output key register (getKey, extractMin).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.zero : Fin rBin

Scratch constant 0 (also zeroReg for SubroutineCode.zeroFillCode).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.one : Fin rBin

Scratch constant 1 (also oneReg for SubroutineCode.zeroFillCode).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.t : Fin rBin

Scratch address / comparison register (also curReg for SubroutineCode.zeroFillCode).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.k : Fin rBin

Current 1-based heap position during siftUp / siftDown.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.p : Fin rBin

Parent or chosen child position during siftUp / siftDown.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.vk : Fin rBin

Handle at position k (or right child during siftDownChoose).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.vp : Fin rBin

Handle at position p.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.dk : Fin rBin

Key of vk.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.dp : Fin rBin

Key of vp.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.l : Fin rBin

Left child 2 * k during siftDown.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Reg.szp : Fin rBin

sz + 1 bound during siftDown.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.inputMask (i : Fin rBin) : Bool

Register classification: 0..4 are persistent (false), 5..24 are caller/scratch (true).

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.allocSpan : WordRAM.Code WordRAM.Basis.exact rBin

Bump-allocate space n = 3 * n + 1 words at frontierReg, recording baseReg, hb, and pb.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.initSetup : WordRAM.Code WordRAM.Basis.exact rBin

Initialize hb := base + n, pb := base + 2 * n + 1, and sz := 0 assuming [base, base + space n) is already zero-filled.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.swapCode : WordRAM.Code WordRAM.Basis.exact rBin

Swap heap entries at positions k (handle vk) and p (handle vp), updating pos.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.cmpEntries (vA dA vB dB : Fin rBin) : WordRAM.Code WordRAM.Basis.exact rBin

Set t := 1 iff IndexedMinPQ.RawPrioLT (vA, dA) (vB, dB), else t := 0.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.cmpKP : WordRAM.Code WordRAM.Basis.exact rBin

Set t := 1 iff IndexedMinPQ.RawPrioLT (vk, dk) (vp, dp), else t := 0.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.cmpPK : WordRAM.Code WordRAM.Basis.exact rBin

Set t := 1 iff IndexedMinPQ.RawPrioLT (vp, dp) (vk, dk), else t := 0.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftUpBody : WordRAM.Code WordRAM.Basis.exact rBin

One iteration of siftUp from k ≥ 2, using k >>> one = k / 2 for the parent position.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftUp : WordRAM.Code WordRAM.Basis.exact rBin

Repair upward from position k.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftDownChoose : WordRAM.Code WordRAM.Basis.exact rBin

Choose the lexicographically smaller child of k (l vs l + 1) into (p, vp, dp).

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftDownSink : WordRAM.Code WordRAM.Basis.exact rBin

Swap k with chosen child (p, vp, dp) if IndexedMinPQ.RawPrioLT (vp, dp) (vk, dk), else stop siftDown.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftDownBody : WordRAM.Code WordRAM.Basis.exact rBin

One iteration of siftDown.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.siftDown : WordRAM.Code WordRAM.Basis.exact rBin

Repair downward from position k.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.doIsEmpty : WordRAM.Code WordRAM.Basis.exact rBin

Handle isEmpty: outFlag := 1 when sz = 0, outFlag := 0 otherwise.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.doGetKey : WordRAM.Code WordRAM.Basis.exact rBin

Handle getKey v: sets outFlag := 0 if pos[v] = 0, else outFlag := 1 and outK := key[v].

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.doInsert : WordRAM.Code WordRAM.Basis.exact rBin

Handle insert v k: stores key[v] := argK, appends v at sz + 1, and sifts up.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.doDecreaseKey : WordRAM.Code WordRAM.Basis.exact rBin

Handle decreaseKey v k: updates key[v] := argK, reads k := pos[v], and sifts up.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.doExtractNonEmpty : WordRAM.Code WordRAM.Basis.exact rBin

Non-empty branch of extractMin: reads root into (outV, outK), clears pos[outV], moves last entry to root when sz - 1 > 0, and sifts down.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.doExtractMin : WordRAM.Code WordRAM.Basis.exact rBin

Handle extractMin: sets outFlag := 0 if empty, otherwise runs doExtractNonEmpty.

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.opCode : WordRAM.Code WordRAM.Basis.exact rBin

Dispatch a single IndexedMinPQ.Op encoded in (tag2, tag1, tag0, argV, argK).

def Cslib.Algorithms.WordRAM.PriorityQueue.BinaryHeap.pqCode : PQCode WordRAM.Basis.exact rBin

Packaged PQCode .exact rBin for the standalone binary heap.