Crit-Bit Iterators and 64-bit Compatibility#429

Merged

samuelgruetter merged 25 commits intomit-plv:masterfrom vfukala:iterators

Aug 12, 2024

+2,856-445

Commits on Jan 30, 2024

Implement and verify get_min, get_max, and next_ge modulo admissions
vfukala
committed
Reorder preconditions to have memory predicates at the end
vfukala
committed

Commits on Feb 8, 2024

Implement + verify a function writing the n key-value pairs following key k from a CBT into an array
vfukala
committed
Merge branch 'master' into iterators
vfukala
committed

Commits on Mar 9, 2024

Merge branch 'master' into iterators
vfukala
committed

Commits on Mar 12, 2024

Change page_from_cbt spec to use map_to_sorted_list
vfukala
committed

Commits on Mar 20, 2024

Proving admissions WIP
vfukala
committed

Commits on Mar 21, 2024

Finish map_to_sorted_list proofs, prove set_bit lemmas
vfukala
committed

Commits on Mar 22, 2024

Commits on Mar 23, 2024

Commits on Jun 5, 2024

Commits on Jun 6, 2024

Commits on Jun 7, 2024

Factor out map definitions and lemmas to be moved to coqutil
vfukala
committed

Commits on Jun 11, 2024

Commits on Aug 10, 2024

Commits on Aug 11, 2024

Make compatible with Coq 8.20
vfukala
committed