Repository navigation

feat(Algorithms/Lean/Dijkstra): Dijkstra with a binary heap over the memory oracle - #2238

Merged

SamuelSchlesinger merged 27 commits into

mainfrom

feat/ram-dijkstra-memory

Nov 2, 2026

Merged

feat(Algorithms/Lean/Dijkstra): Dijkstra with a binary heap over the memory oracle#2238
SamuelSchlesinger merged 27 commits into
mainfrom
feat/ram-dijkstra-memory

Commits on Nov 1, 2026
- feat(DataStructure/Memory): word-addressed memory oracle and named field arrays
  
  SamuelSchlesinger
  and
  claude
  committed
  5909d1b
- doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018)
  
  SamuelSchlesinger
  and
  claude
  committed
  412f614
- feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials
  
  SamuelSchlesinger
  and
  claude
  committed
  16a647f
- feat(DataStructure/StateTransition): weaken and rescale amortized refinements
  
  SamuelSchlesinger
  and
  claude
  committed
  2f12c49
- Merge the memory-oracle branch (#2211) into the queue slice
  
  SamuelSchlesinger
  and
  claude
  committed
  fba5208
- fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement
  
  SamuelSchlesinger
  and
  claude
  committed
  98e3290
- Merge the refinement branch (#2212) into the queue slice
  
  SamuelSchlesinger
  and
  claude
  committed
  02ba9f7
- refactor(DataStructure/StateTransition): make Refinement.Amortized a structure
  
  SamuelSchlesinger
  and
  claude
  committed
  56232f9
- Merge the refinement branch (#2212) into the queue slice
  
  SamuelSchlesinger
  and
  claude
  committed
  1b4e2ea
- wip: array stack over memory and queue method lemmas
  
  SamuelSchlesinger
  and
  claude
  committed
  fe7d60d
- feat(Foundations): affine cost bounds are O(size)
  
  SamuelSchlesinger
  and
  claude
  committed
  aad5f3e
- Merge the refinement branch (#2212) into the queue slice
  
  SamuelSchlesinger
  and
  claude
  committed
  78cf872
- wip: queue over memory
  
  SamuelSchlesinger
  and
  claude
  committed
  6698e86
- refactor(DataStructure/StateTransition): product answer types via Sum.elim
  
  SamuelSchlesinger
  and
  claude
  committed
  7dda248
- Merge the refinement branch (#2212) into the queue slice
  
  SamuelSchlesinger
  and
  claude
  committed
  93adf90
- feat(DataStructure): queue over two array stacks over the memory oracle
  
  SamuelSchlesinger
  and
  claude
  committed
  412ad37
- feat(Algorithms/Lean/Dijkstra): Dijkstra as a client of the priority-queue spec
  
  SamuelSchlesinger
  and
  claude
  committed
  ad9fa15
- feat(Algorithms/Lean/Dijkstra): count operations by edges as well as vertices
  
  SamuelSchlesinger
  and
  claude
  committed
  b2ebc4a
- feat(DataStructure): products over one memory, and glue charges for hop 3
  
  SamuelSchlesinger
  and
  claude
  committed
  f40fe1c
Commits on Nov 2, 2026
- feat(DataStructure/PriorityQueue): indexed binary heap over the memory oracle
  
  SamuelSchlesinger
  and
  claude
  committed
  524056b
- test(DataStructure/PriorityQueue): allow #guard in the binary-heap memory test
  
  SamuelSchlesinger
  and
  claude
  committed
  8c5cd8e
- Merge #2220 (Dijkstra client) onto the binary heap (#2237)
  SamuelSchlesinger
  committed
  4d59fe8
- fix(Algorithms/Lean/Dijkstra): evaluate client calls under Sum.elim product answers
  
  SamuelSchlesinger
  and
  claude
  committed
  b417144
- feat(Algorithms/Lean/Dijkstra): Dijkstra with a binary heap over the memory oracle
  
  SamuelSchlesinger
  and
  claude
  committed
  9fd04ae
- test(Dijkstra): allow #guard in the memory test
  
  SamuelSchlesinger
  and
  claude
  committed
  a9e0b2e
- refactor(Algorithms/Lean/Dijkstra): state the allocated structures separately
  
  SamuelSchlesinger
  and
  claude
  committed
  9a20b2f
- Merge origin/main into feat/ram-dijkstra-memory (after #2237, #2220)
  
  SamuelSchlesinger
  and
  claude
  committed
  5ca02f1

Commits

Commits on Nov 1, 2026

Commits on Nov 2, 2026