Skip to content

feat(WordRAM/Dictionary): add uniform probing model and Word-RAM dictionary #1709

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(WordRAM/Dictionary): add uniform probing model and Word-RAM dictionary #1709

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
a31eaf9
feat(WordRAM/Dictionary): add uniform probing model and Word-RAM dict…
orbitingflea Oct 30, 2026
9f9a7b1
docs(WordRAM/Dictionary): clarify CLRS 3rd-ed locators and Theorem 11…
orbitingflea Oct 30, 2026
6e53cb9
Merge upstream/main d0d220c93 into wordram-uniform-probing
orbitingflea Oct 30, 2026
db34ad6
Merge upstream/main 311e9841f into wordram-uniform-probing
orbitingflea Oct 30, 2026
3013adb
chore(wordram): merge main for uniform probing integration
SamuelSchlesinger 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 @@ -29,6 +29,7 @@ public import Complexity.Algorithms.Lean.Sort.Bitonic.Basic
public import Complexity.Algorithms.Lean.Sort.Bitonic.Correctness
public import Complexity.Algorithms.Lean.Sort.Bitonic.Trace
public import Complexity.Algorithms.Lean.Sort.Bitonic.ZeroOne
public import Complexity.Algorithms.Lean.UniformProbing
public import Complexity.Algorithms.Lean.VanEmdeBoas.Basic
public import Complexity.Algorithms.Lean.VanEmdeBoas.Elements
public import Complexity.Algorithms.Lean.VanEmdeBoas.Insert
Expand Down Expand Up @@ -86,6 +87,7 @@ 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.Dictionary.UniformProbing
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