search

vellvm / ctrees

An itree-like data-structure to additionally support internal non-determinism
MIT License
13 stars 2 forks source link

Prove *complete* simulations for the constant and state schedulers #25

Open nchappe opened 1 year ago

nchappe commented 1 year ago

The theorems refine_cst_refinement and refine_state_refinement are proved with regular strong simulations, but it would make more sense to use complete simulations (cssim).