Repository navigation

feat(Algorithms/Lean/Karger): lay out the contraction structure in memory, with the sampling query - #2253

Open

SamuelSchlesinger wants to merge 32 commits into

mainfrom

feat/karger-memory-layout

Open

feat(Algorithms/Lean/Karger): lay out the contraction structure in memory, with the sampling query#2253
SamuelSchlesinger wants to merge 32 commits into
mainfrom
feat/karger-memory-layout

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(DataStructure): products over one memory, and glue charges for hop 3
  
  SamuelSchlesinger
  and
  claude
  committed
  f40fe1c
- feat(DataStructure): distributional refinements and a random table over memory
  
  SamuelSchlesinger
  and
  claude
  committed
  43ca605
Commits on Nov 2, 2026

Navigation Menu

Repository navigation

feat(Algorithms/Lean/Karger): lay out the contraction structure in memory, with the sampling query - #2253

feat(Algorithms/Lean/Karger): lay out the contraction structure in memory, with the sampling query#2253
SamuelSchlesinger wants to merge 32 commits into
mainfrom
feat/karger-memory-layout

Commits on Nov 1, 2026

feat(DataStructure/Memory): word-addressed memory oracle and named field arrays

doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018)

feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials

feat(DataStructure/StateTransition): weaken and rescale amortized refinements

Merge the memory-oracle branch (#2211) into the queue slice

fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement

Merge the refinement branch (#2212) into the queue slice

refactor(DataStructure/StateTransition): make Refinement.Amortized a structure

Merge the refinement branch (#2212) into the queue slice

wip: array stack over memory and queue method lemmas

feat(Foundations): affine cost bounds are O(size)

Merge the refinement branch (#2212) into the queue slice

wip: queue over memory

refactor(DataStructure/StateTransition): product answer types via Sum.elim

Merge the refinement branch (#2212) into the queue slice

feat(DataStructure): queue over two array stacks over the memory oracle

feat(DataStructure): products over one memory, and glue charges for hop 3

feat(DataStructure): distributional refinements and a random table over memory

Commits on Nov 2, 2026

feat(DataStructure): stack coin-using distributional hops; deterministic hops as distributional

feat(Algorithms/Lean/Karger): Karger's contraction algorithm as a randomized client, with its survival bound on the specification

feat(DataStructure/StateTransition): weakest preconditions with cost

Merge remote-tracking branch 'origin/main' into feat/ram-random-hop

Merge #2244 (weakest preconditions, on #2229) into #2241 (Karger specification)

fix(StateTransition): use OracleComp.sumHandler after #2201

Merge #2232 (OracleComp.sumHandler after #2201) into the coin-composition branch

Merge #2232 (sumHandler fix after #2201) into the Karger memory base

feat(Algorithms/Lean/Karger): lay out the contraction structure in memory, with the sampling query

Merge origin/main into feat/ram-random-coins (after #2232)

Merge #2236 (feat/ram-random-coins, merged with main) into feat/karger-spec

Merge origin/main into feat/karger-spec (after #2236)

Merge #2241 (feat/karger-spec, merged with main) into feat/karger-memory-layout

Merge origin/main into feat/karger-memory-layout (after #2241)