Skip to content

feat(Algorithms/WordRAM/Dictionary): open-addressed linear probing with 5-wise independent hashing #1708

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 34 commits into from
Oct 30, 2026
Merged

feat(Algorithms/WordRAM/Dictionary): open-addressed linear probing with 5-wise independent hashing #1708

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
874872f
feat(stateful,word-ram): add relational specifications and subroutine…
orbitingflea Oct 29, 2026
012511e
feat(wordram): geometric Las Vegas loop expected-time bound and rando…
orbitingflea Oct 29, 2026
cdfda0c
Merge remote-tracking branch 'upstream/main' into wordram-randomized-…
orbitingflea Oct 29, 2026
8079947
Add ExecSteps trace to SubroutineDS and expand randomized subroutine …
orbitingflea Oct 29, 2026
0289bd0
Merge remote-tracking branch 'upstream/main' into wordram-randomized-…
orbitingflea Oct 29, 2026
4f99627
Merge remote-tracking branch 'upstream/main' into stateful-relational…
orbitingflea Oct 29, 2026
cefa21f
Update author header and MitzenmacherUpfal2017 section locators
orbitingflea Oct 29, 2026
a7461e8
refactor(stateful,word-ram): share Execution/DynamicProgram/Subroutin…
orbitingflea Oct 29, 2026
888918d
chore(deps): track CSLib main and Lean rc2
SamuelSchlesinger Oct 29, 2026
9a1b754
refactor(probability): use generic infinite-sum lemmas
SamuelSchlesinger Oct 29, 2026
d7dcd79
fix(build): adapt proofs to the rc2 Mathlib API
SamuelSchlesinger Oct 29, 2026
7925011
Merge remote-tracking branch 'origin/main' into work/cslib-rc2-sync-1…
SamuelSchlesinger Oct 29, 2026
f5a70cb
test(quantum): qualify the protected matrix lemma
SamuelSchlesinger Oct 29, 2026
bb3e910
fix(build): normalize goals before proof automation
SamuelSchlesinger Oct 29, 2026
0d38523
Merge commit '96fd02a85579bbbce97c02110ed80da02684cb2e' into work/csl…
SamuelSchlesinger Oct 29, 2026
23d812a
Merge commit '0d38523e96f8b431aeadc86c548c9994714f9b00' into work/rep…
SamuelSchlesinger Oct 29, 2026
a18cb36
Merge commit '0d38523e96f8b431aeadc86c548c9994714f9b00' into work/rep…
SamuelSchlesinger Oct 29, 2026
1cdc80e
test(wordram): exercise two-outcome randomized subroutines
SamuelSchlesinger Oct 29, 2026
e62c359
refactor(wordram): index dynamic programs by operation signatures
SamuelSchlesinger Oct 29, 2026
211a82c
Merge commit 'e62c359d802b888d1576882481152dfe650bce0d' into work/rep…
SamuelSchlesinger Oct 29, 2026
a115e42
refactor(wordram): share basis-preserving subroutine plumbing
SamuelSchlesinger Oct 29, 2026
a3d83b6
Merge commit 'a115e42b53774978d96e2202cb74ea05bea5f7e7' into work/rep…
SamuelSchlesinger Oct 29, 2026
fb42ef6
refactor(wordram): reuse randomized subroutine plumbing and probabili…
SamuelSchlesinger Oct 29, 2026
78981ac
feat(WordRAM/Hashing): add self-contained k-wise independent and tabu…
orbitingflea Oct 29, 2026
8f23b11
fix(WordRAM/Hashing): compose isKWiseIndependentHash_eval and extract…
orbitingflea Oct 30, 2026
90abcec
Merge remote-tracking branch 'upstream/main' into wordram-kwise-hashi…
orbitingflea Oct 30, 2026
8656f2b
Merge landed supported-pin main into relational repair
SamuelSchlesinger Oct 30, 2026
61c2f92
Merge actual-main relational checkpoint into randomized repair
SamuelSchlesinger Oct 30, 2026
d7b17b4
Merge remote-tracking branch 'origin/wordram-kwise-hashing-code' into…
orbitingflea Oct 30, 2026
bc61368
feat(Algorithms/WordRAM/Dictionary): add linear probing dictionary on…
orbitingflea Oct 30, 2026
ae034db
docs(LinearProbing): add Pagh-Pagh-Ruzic 2009 source statement, locat…
orbitingflea Oct 30, 2026
bcf3c1c
Merge upstream/main a32dda9d2 into wordram-linear-probing
orbitingflea Oct 30, 2026
92a5c28
Merge upstream/main d0d220c93 into wordram-linear-probing
orbitingflea Oct 30, 2026
33cda07
Merge upstream/main 311e9841f into wordram-linear-probing
orbitingflea Oct 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Complexity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,8 @@ public import Complexity.Algorithms.WordRAM.Deduplicate.Program
public import Complexity.Algorithms.WordRAM.Dictionary.ChainedHash
public import Complexity.Algorithms.WordRAM.Dictionary.CuckooHashing
public import Complexity.Algorithms.WordRAM.Dictionary.CuckooHashing.HashFamily
public import Complexity.Algorithms.WordRAM.Dictionary.LinearProbing
public import Complexity.Algorithms.WordRAM.Dictionary.LinearProbing.FiveWise
public import Complexity.Algorithms.WordRAM.Dijkstra.Fibonacci
public import Complexity.Algorithms.WordRAM.Dijkstra.FibonacciStatement
public import Complexity.Algorithms.WordRAM.Dijkstra.GenericPQ
Expand Down
Loading
Loading