Repository navigation

feat(WordRAM): guarded loops in realize - #2285

Merged

SamuelSchlesinger merged 41 commits into

mainfrom

feat/realize-while

Nov 2, 2026

Merged

feat(WordRAM): guarded loops in realize#2285
SamuelSchlesinger merged 41 commits into
mainfrom
feat/realize-while

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(WordRAM): certify compositional register-word glue
  SamuelSchlesinger
  committed
  4283b8f
- Merge commit '4283b8fb714450e78ba170865bcb54ce8563bce3' into codex/ram-realization-c2-20261101
  SamuelSchlesinger
  committed
  cb0adff
- feat(WordRAM): realize memory queries with uniform bind and glue
  SamuelSchlesinger
  committed
  45dd184
- fix(WordRAM): normalize the memory return simp rule
  SamuelSchlesinger
  committed
  d8f6bea
- feat(WordRAM): realize bounded loops and initialized client programs
  SamuelSchlesinger
  committed
  4977e9b
Commits on Nov 2, 2026
- feat(WordRAM): derive global and framed implementation certificates
  SamuelSchlesinger
  committed
  04a06b5
- chore(WordRAM): combine published realization and queue prerequisites
  SamuelSchlesinger
  committed
  e768e0a
- feat(WordRAM): realize runtime-layout memory-stack methods
  SamuelSchlesinger
  committed
  5917ae4
- refactor(WordRAM): centralize realization history and word encodings
  SamuelSchlesinger
  committed
  a929a76
- feat(WordRAM): realize tactic for memory-client realizations
  
  SamuelSchlesinger
  and
  claude
  committed
  a91fb0a
- feat(WordRAM): loops whose body issues a query in realize
  
  SamuelSchlesinger
  and
  claude
  committed
  141d112
- test(WordRAM): a whole stack client to a flat program via realize
  
  SamuelSchlesinger
  and
  claude
  committed
  de22695
- feat(WordRAM): realize measure-bounded early-exit while loops
  SamuelSchlesinger
  committed
  15eed51
- perf(WordRAM): state realize certificates per form in the client's terms
  
  SamuelSchlesinger
  and
  claude
  committed
  212e582
- Merge remote-tracking branch 'origin/work/c5-while-1651-20261102' into feat/realize-while
  SamuelSchlesinger
  committed
  fc11f56
- chore: regenerate the aggregate import after merging #2270
  
  SamuelSchlesinger
  and
  claude
  committed
  929ced0
- fix(WordRAM): state iterate₀ in iterateRuntime's named-component form
  
  SamuelSchlesinger
  and
  claude
  committed
  3193d5b
- feat(WordRAM): guarded loops in realize
  
  SamuelSchlesinger
  and
  claude
  committed
  381a01d
- style(WordRAM): wrap a long line in the realize loop tests
  
  SamuelSchlesinger
  and
  claude
  committed
  df7a183
- refactor(WordRAM): use appendWords for the stack client's environments
  
  SamuelSchlesinger
  and
  claude
  committed
  ddbc31f
- fix(WordRAM): keep iterate₀'s statement, as in #2277's proof-only repair
  
  SamuelSchlesinger
  and
  claude
  committed
  78098fd
- test(WordRAM): a heartbeat budget for the realize transfer loop
  
  SamuelSchlesinger
  and
  claude
  committed
  bd1b010
- test(WordRAM): place the transfer loop's heartbeat budget before its docstring
  
  SamuelSchlesinger
  and
  claude
  committed
  0d221c2
- test(WordRAM): a realize loop whose guard and step capture the environment
  
  SamuelSchlesinger
  and
  claude
  committed
  83a32ba
- chore(WordRAM): merge actual main into reviewed while automation
  SamuelSchlesinger
  committed
  56c6fe9

Commits

Commits on Nov 1, 2026

Commits on Nov 2, 2026