sets

python.Sets.wordSize

def Sets.wordSize : Nat

2^64: CPython’s hashes are 64-bit words in the table’s arithmetic.

python.Sets.unsigned

def Sets.unsigned (hash : Int) : Nat

The hash as an unsigned 64-bit word.

python.Sets.signed

def Sets.signed (x : Nat) : Int

The 64-bit word x read as a signed hash.

python.Sets.noneHash

def Sets.noneHash : Int

hash(None), a constant since CPython 3.12.

python.Sets.lane

def Sets.lane (acc : Nat) (hash : Int) : Nat

One step of tuplehash (xxHash) taking in an item’s hash as the lane: acc + lane * PRIME_2, rotated left 31 bits, times PRIME_1.

python.Sets.tupleHash

def Sets.tupleHash (hashes : List Int) : Int

hash(t) of a tuple from its items’ hashes.

python.Sets.rotate

def Sets.rotate (x : Nat) (b : Nat) : Nat

The word x rotated left b bits as a 64-bit word.

python.Sets.plus

def Sets.plus (a : Nat) (b : Nat) : Nat

The sum of the 64-bit words a and b, wrapping.

python.Sip

record Sip

SipHash’s four words of state.

python.Sip.round

def Sip.round (s : Sip) : Sip

One SipRound on the state s.

python.Sip.absorb

def Sip.absorb (s : Sip) (m : Nat) : Sip

The state s taking in the 64-bit word m (one round, SipHash-1-3).

python.Sip.word

def Sip.word (bytes : List Nat) : Nat

The bytes as a little-endian number.

python.Sip.blocks

def Sip.blocks (fuel : Nat) (s : Sip) (bytes : List Nat) (count : Nat) : Sip

The state s taking in the bytes eight at a time, then the last ones with the length count of all of them in the top byte, within fuel blocks.

python.Sip.hash

def Sip.hash (bytes : List Nat) : Nat

SipHash-1-3 of the bytes with the key zero (CPython’s string hash under PYTHONHASHSEED=0).

python.Sets.codeBytes

def Sets.codeBytes (width : Nat) (c : Nat) : List Nat

The code point c as width little-endian bytes.

python.Sets.textHash

def Sets.textHash (cs : Codes) : Int

hash(s) of the str of the code points cs under PYTHONHASHSEED=0: SipHash-1-3 of CPython’s storage of them (one, two or four bytes each, by the largest), 0 for the empty string, -1 taken as -2.

python.Value.hash

def Value.hash (v : Value) : Option Int

CPython’s hash of the value v, when the model gives it (a str’s as under PYTHONHASHSEED=0, an object’s from its model address; the callers have checked it is hashable and not hashed by the user’s code): none for a NaN and anything else.

python.Value.chosenHash

def Value.chosenHash (v : Value) : List String

The implementation’s choices the hash of the value v depends on: a str’s, an object’s, those of a tuple’s items.

python.Value.chosenAny

def Value.chosenAny (vs : List Value) : List String

The implementation’s choices the hashes of the values vs depend on.

python.Value.hashAll

def Value.hashAll (vs : List Value) : Option (List Int)

The hashes of the values vs, when the model gives every one.

python.Sets.empty

def Sets.empty (n : Nat) : List Slot

n empty slots.

python.Sets.emptyTable

def Sets.emptyTable : SetTable

The smallest table: eight empty slots.

python.Sets.slotAt

def Sets.slotAt (slots : List Slot) (i : Nat) : Slot

The slot at position i of slots.

python.Sets.withSlot

def Sets.withSlot (slots : List Slot) (i : Nat) (slot : Slot) : List Slot

The slots with the one at position i replaced by slot.

python.Sets.jump

def Sets.jump (size : Nat) (i : Nat) (perturb : Nat) : Nat

Where probing goes in a table of size slots after a run that started at i: (i * 5 + 1 + perturb) & mask.

python.Sets.run

def Sets.run (size : Nat) (i : Nat) : Nat

How many slots a run from i looks at in a table of size slots: ten when they are in the table (LINEAR_PROBES is nine more), else one.

python.Sets.fuel

def Sets.fuel (slots : List Slot) : Nat

Probing at most this many slots reaches every slot of the table’s slots (it is never full).

python.Probed

data Probed

What looking up a key finds: the slot holding it, or the empty slot that ends the search with the first dummy seen before it.

python.Sets.probe

def Sets.probe (fuel : Nat) (slots : List Slot) (hash : Int) (key : Value) (start : Nat) (j : Nat) (left : Nat) (perturb : Nat) (dummy : Option Nat) : Probed

The search in slots for key with its hash (CPython’s set_add_entry and set_lookkey), within fuel slots: at slot j of the run that started at start, with left slots left in the run, perturb, and the first dummy so far.

python.Sets.find

def Sets.find (slots : List Slot) (hash : Int) (key : Value) : Probed

Looking up key with its hash in slots.

python.Sets.cleanSlot

def Sets.cleanSlot (fuel : Nat) (slots : List Slot) (start : Nat) (j : Nat) (left : Nat) (perturb : Nat) : Nat

The first empty slot in slots (a table with no dummies) for an item, within fuel slots: at slot j of the run that started at start, with left slots left in the run and perturb (CPython’s set_insert_clean).

python.Sets.insertClean

def Sets.insertClean (slots : List Slot) (hash : Int) (key : Value) : List Slot

The item key put in the first empty slot of slots its hash reaches (no dummies, no equal item).

python.Sets.entries

def Sets.entries (slots : List Slot) : List (Int * Value)

The hashes and items of slots, in the slots’ order.

python.Sets.sizeFor

def Sets.sizeFor (fuel : Nat) (size : Nat) (minused : Nat) : Nat

The smallest power of two past minused, from size doubling at most fuel times.

python.Sets.resize

def Sets.resize (slots : List Slot) (used : Nat) (minused : Nat) (chosen : List String) : SetTable

set_table_resize: a table of the size for minused with the items of slots inserted in their order; used items, and the chosen hashes its order depends on.

python.Sets.growth

def Sets.growth (used : Nat) : Nat

How a table of used items grows after an add fills it: four times the items, twice past 50000.

python.Sets.addHashed

def Sets.addHashed (slots : List Slot) (used : Nat) (fill : Nat) (chosen : List String) (hash : Int) (key : Value) : SetTable

set_add_entry of key with its hash on the hash table of slots (used items, fill used and dummy slots, the chosen hashes its order depends on): an equal item leaves it as it is; else the first dummy seen, or the empty slot (growing the table when used and dummy slots reach three fifths).

python.Sets.appended

def Sets.appended (items : List Value) (key : Value) : List Value

The items in the order they were added, with key after them unless an equal one is there.

python.Sets.add

def Sets.add (t : SetTable) (key : Value) : SetTable

Adding the item key to the table t; an item whose hash the model does not give turns the table into the order the items were added.

python.Sets.ofItems

def Sets.ofItems (xs : List Value) : SetTable

A set from the items xs added in order (a literal, or any iterable but a set or a dict).

python.Sets.discard

def Sets.discard (t : SetTable) (key : Value) : SetTable * Bool

set_discard_entry of key from the table t: the item’s slot becomes a dummy; whether it was there.

python.Sets.contains

def Sets.contains (t : SetTable) (key : Value) : Bool

Whether the set’s table t has the item key.

python.Sets.size

def Sets.size (t : SetTable) : Nat

How many items the set’s table t has.

python.Sets.merge

def Sets.merge (target : SetTable) (source : SetTable) : SetTable

set_merge: another set’s items into a set. An empty target of the same size whose source has no dummies gets the slots as they are; an empty target gets them by clean inserts in the source’s order; otherwise each is added. The target first grows when the items would fill three fifths of it.

python.Sets.mergeInto

def Sets.mergeInto (target : SetTable) (others : List Slot) (otherUsed : Nat) (otherFill : Nat) : SetTable

set_merge once the target has room: the source’s slots others, with otherUsed items and otherFill used and dummy slots.

python.Sets.copy

def Sets.copy (t : SetTable) : SetTable

The copy of the set’s table t (set_copy: a new set merged from it).

python.Operand

data Operand

What a set operation reads from its other operand: a set’s table, a dict’s keys, or an iterable’s items.

python.Sets.update

def Sets.update (t : SetTable) (other : Operand) : SetTable

set_update_internal of the table t with the other operand: a set’s items merged, a dict’s keys added (the table first grown for them), or an iterable’s items added in order.

python.Sets.operandItems

def Sets.operandItems (other : Operand) : List Value

The items of the other operand in the order it gives them.

python.Sets.intersection

def Sets.intersection (t : SetTable) (other : Operand) : SetTable

set_intersection of the table t and the other operand: iterating the smaller of two sets (or the iterable), the items the other has, added in that order to a new set (whose order depends on a str’s hash when either set’s did).

python.Sets.discardAll

def Sets.discardAll (t : SetTable) (xs : List Value) : SetTable

Discarding the items xs from the table t in turn, then resizing away the dummies when more than a quarter of the table holds them (set_difference_update_internal).

python.Sets.differenceUpdate

def Sets.differenceUpdate (t : SetTable) (other : Operand) : SetTable

set_difference_update_internal of the table t: the other operand’s items discarded (a set more than eight times larger replaced by the intersection first).

python.Sets.difference

def Sets.difference (t : SetTable) (other : Operand) : SetTable

set_difference of the table t and the other operand: a copy with the other’s items discarded when this set is more than four times larger (or the other is an iterable), else this set’s items the other lacks, added in order.

python.Sets.symmetricUpdate

def Sets.symmetricUpdate (t : SetTable) (other : Operand) : SetTable

set_symmetric_difference_update of the table t: each item of the other operand (made a set first) discarded when present, else added.

python.Sets.symmetricDifference

def Sets.symmetricDifference (t : SetTable) (other : Operand) : SetTable

set_symmetric_difference of the table t and the other operand: the other made a set, then toggled by this set’s items.

python.Heap.setOf

def Heap.setOf (h : Heap) (t : SetTable) : Changed

A new set on the heap h from the table t.

python.Value.userHashed

def Value.userHashed (h : Heap) (v : Value) : Bool

Whether the hash of the value v on the heap h would run the user’s code: an instance whose class has its own __hash__ (or a tuple holding one).

python.Value.anyUserHashed

def Value.anyUserHashed (h : Heap) (vs : List Value) : Bool

Whether the hash of any of the values vs on the heap h would run the user’s code.

python.Sets.userHashed

def Sets.userHashed (h : Heap) (xs : List Value) : Option Raised

Unsupported when the hash of one of the items xs on the heap h would run the user’s code.

python.Heap.set

def Heap.set (h : Heap) (xs : List Value) : Changed

A new set on the heap h from the items xs added in order.

python.Heap.setTable

def Heap.setTable (h : Heap) (v : Value) : Option SetTable

The set’s table, if the value v is a set on the heap h.