• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
          • Implementation
            • Jenkins-hash
            • Binary-tree
            • Tree-split
            • Heap<
            • Tree-join
            • Tree-delete
            • Rotations
            • Tree-insert
            • Tree-intersect
            • Tree-join-at
            • Tree-union
            • Hash
            • Tree-in
            • Tree-diff
            • Tree-nodes-count
          • Setp
          • Right
          • Left
          • Head
          • Double-containment
          • Subset
          • Intersect
          • Insert
          • In
          • Delete
          • Union
          • Diff
          • From-list
          • To-list
          • Set-equiv
          • Sfix
          • Pick-a-point
          • Cardinality
          • Set-induct
          • Set-bi-induct
          • Emptyp
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Set

Implementation

Implementation details of sets.

Here we describe the internal representation of sets. Users of the library should not depend on these details, opting instead to use the "primitive" operators abstractly.

Sets are represented internally as treaps (= "tree" + "heap"). Treaps are binary search trees with an additional max heap constraint (see bst-p and heapp, respectively). Crucially, the max heap property is maintained with respect to a different order than that which is used for the binary search tree property.

The binary search tree property uses the bst< order, which is just a wrapper around <<. The binary search tree property is what delivers logarithmic average-case complexity of our basic operations.

The max heap property uses the new heap< total order. This ensures that the tree has a canonical structure and that the tree is practically balanced. Treaps are only expected to be balanced in practice if the heap order and the binary search tree order are largely uncorrelated. That is, the heap order appears "random" with respect to the binary search tree order. To accomplish this, the heap< order is based on a non-cryptographic hash of its arguments.

References

  • https://www.cs.cmu.edu/~scandal/papers/treaps-spaa98.pdf
  • https://en.wikipedia.org/wiki/Treap

Subtopics

Jenkins-hash
An implementation of Jenkins one-at-a-timehash.
Binary-tree
Definition of a binary tree data structure.
Tree-split
Split a tree into two disjoint subtrees.
Heap<
A total order based on object hashes.
Tree-join
Join two trees which have previously been tree-split.
Tree-delete
Remove a value from the tree.
Rotations
Left and right tree rotations.
Tree-insert
Insert a value into the tree.
Tree-intersect
Take the intersection of two treaps.
Tree-join-at
Wrapper around tree-join annotated with a split point.
Tree-union
Take the union of two treaps.
Hash
The hash function used by heap<.
Tree-in
Determine if a value appears in the tree.
Tree-diff
Take the difference of two treaps.
Tree-nodes-count
The number of elements in a tree.