🥮 mooncakes.io

    skiplist

    Skip List with geometric level distribution and invariant checks (Pugh, CACM 1990).

    skiplist
    data-structures
    probabilistic
    Download zip
    Version
    0.1.1
    License
    Apache-2.0
    Repository
    Last updated
    1 hour ago
    Downloads
    14

    No dependencies

    #skiplist-mbt

    Skip List with geometric level distribution and invariant checks, per Pugh (CACM 1990) Fig. 2/4/5.

    moon test

    #Provenance & License

    • Algorithm: independently implemented in MoonBit from "Skip List (Pugh, CACM 1990)" (see EXTRACTION.md for the full citation and judgment mapping).
    • Code: original MoonBit implementation, Apache-2.0.

    LCG

    source
    pub struct LCG {
      // private fields
    }

    LCG::new

    source
    fn LCG::new(seed : UInt64) -> LCG

    LCG::next_double

    source
    fn LCG::next_double(self : LCG) -> Double

    Uniform double in [0, 1) — top 53 bits.

    LCG::next_u64

    source
    fn LCG::next_u64(self : LCG) -> UInt64

    Node

    source
    pub struct Node {
      id : Int
      key : Int
      forward : Array[Node]
      // private fields
    }

    SkipList

    source
    pub struct SkipList {
      header : Node
      nil_node : Node
      p : Double
      max_level : Int
      rng : LCG
      // private fields
    }

    SkipList::check_invariants

    source
    fn SkipList::check_invariants(self : SkipList) -> Bool

    Structural invariants: level-1 strictly ascending; every higher chain is a subsequence of the one below it.

    SkipList::current_level

    source
    fn SkipList::current_level(self : SkipList) -> Int

    SkipList::delete

    source
    fn SkipList::delete(self : SkipList, search_key : Int) -> Bool

    Fig. 4 Delete: splice out, then shrink list->level while the top is empty.

    SkipList::get

    source
    fn SkipList::get(self : SkipList, key : Int) -> Int

    Fig. 2 search returning the stored value of an existing key.

    SkipList::insert

    source
    fn SkipList::insert(self : SkipList, search_key : Int, new_value : Int) -> Unit

    Fig. 4 Insert: duplicate key updates value; a new node whose level exceeds the list level raises list->level and fills update with header.

    SkipList::last_comparisons

    source
    fn SkipList::last_comparisons(self : SkipList) -> Int

    SkipList::new

    source
    fn SkipList::new(max_level : Int, p? : Double, seed? : UInt64) -> SkipList

    Initialization (paper §Search Algorithm): level := 1, all header forward pointers point to NIL.

    SkipList::search

    source
    fn SkipList::search(self : SkipList, search_key : Int) -> Bool

    Fig. 2 Search. Returns whether the key is present; comparison count recorded for the T-COST paper judgment.

    SkipList::size

    source
    fn SkipList::size(self : SkipList) -> Int

    SkipList::to_level1_keys

    source
    fn SkipList::to_level1_keys(self : SkipList) -> Array[Int]

    Level-1 chain keys (ascending) — oracle comparison and invariant checks.

    cap_level

    source
    fn cap_level(run : Int, max_level : Int) -> Int

    Random level from a run of zero bits (paper: for p = 1/2 the level is "easy to generate from a stream of random bits"). FORMAL contract: the result stays in [1, max_level].

    random_level

    source
    fn random_level(rng : LCG, p : Double, max_level : Int) -> Int

    Fig. 5 randomLevel for arbitrary p: lvl := 1; while random() < p && lvl < MaxLevel.

    Source Files