Commits · stacked_borrows · Iris / simuliris

Jun 21, 2021
- refactoring · bd912148
  Lennard Gäher authored 3 years ago
  
  bd912148
Jun 20, 2021
- close more lemmas · 59345785
  Lennard Gäher authored 3 years ago
  
  59345785
Jun 14, 2021
- close the deferred UB things · 9f1722f0
  Lennard Gäher authored 3 years ago
  
  9f1722f0
Jun 11, 2021
- remove the well-formedness requirement on tags · 5aef079a
  Lennard Gäher authored 3 years ago
  
  5aef079a
- lemmas and a bit of cleanup · 6f397b02
  Lennard Gäher authored 3 years ago
  
  6f397b02
Jun 09, 2021
- close some lemmas · eac20259
  Lennard Gäher authored 3 years ago
  
  eac20259
Jun 08, 2021
- Merge branch 'master' into stacked_borrows · c8f2aae8
  Lennard Gäher authored 4 years ago
  
  c8f2aae8
- close admitted IrredUnless instance · f2972212
  Lennard Gäher authored 4 years ago
  
  f2972212
- work on closing some lemmas · 961a66d8
  Lennard Gäher authored 4 years ago
  
  961a66d8
- make val and expr no longer mutually recursive · a860cd53
  Ralf Jung authored 4 years ago
  
  a860cd53
Jun 05, 2021
- adjust to new job naming scheme · 8e112951
  Ralf Jung authored 4 years ago
  
  8e112951
- update dependencies · 2d6ad2b4
  Ralf Jung authored 4 years ago
  
  2d6ad2b4
Jun 04, 2021
- prove fair_div_step · c5db9733
  Ralf Jung authored 4 years ago
  
  c5db9733
- prove beh_rel beh_rel_alt (with one axiom about fair_div) · 8430e116
  Ralf Jung authored 4 years ago
  
  8430e116
- make beh_rel about the main thread return value only · 357cae2c
  Ralf Jung authored 4 years ago
  
  357cae2c
- tweak ctx_rel definition · 9f49d264
  Ralf Jung authored 4 years ago
  
  9f49d264
- rename expr_rel -> log_rel · 71934f8b
  Ralf Jung authored 4 years ago
  
  71934f8b
- Import bi more locally · 15bbe0f4
  Ralf Jung authored 4 years ago
  
  15bbe0f4
- add definition of contextual refinement · a285ce8d
  Ralf Jung authored 4 years ago
  
  a285ce8d
Jun 03, 2021
- rename some of our typeclasses to follow new Iris naming scheme · da0c82a9
  Ralf Jung authored 4 years ago
  
  da0c82a9
- update dependencies · b7fa3129
  Ralf Jung authored 4 years ago
  
  b7fa3129
- define beh_rel_alt · e5111a83
  Ralf Jung authored 4 years ago
  
  e5111a83
- introduce tpool type; start defining a more classical notion of refinement · 572e7db2
  Ralf Jung authored 4 years ago
  
  572e7db2
Jun 02, 2021
- rename B → beh_rel · 4c81fda7
  Ralf Jung authored 4 years ago
  
  4c81fda7
- rename stutter_adequacy -> adequacy · 55459883
  Ralf Jung authored 4 years ago
  
  55459883
- remove some old files that are not built any more · a588e430
  Ralf Jung authored 4 years ago
  
  a588e430
- more comment · 7462fb75
  Ralf Jung authored 4 years ago
  
  7462fb75
- move 'B' definition to its own file; explain adequacy_alt assumptions · 242da260
  Ralf Jung authored 4 years ago
  
  242da260
- prove that expr_rel is closed under contexts · 7ff25ce8
  Ralf Jung authored 4 years ago
  
  7ff25ce8
- no reason to be sad, val_wf · 593b6b5c
  Ralf Jung authored 4 years ago
  
  593b6b5c
- fix subst_map_rel: take 'context' and require all its variables to be in the map · bbecfe2f
  Ralf Jung authored 4 years ago
  
  bbecfe2f
Jun 01, 2021
- Merge branch 'master' into stacked_borrows · 7199a85a
  Lennard Gäher authored 4 years ago
  
  7199a85a
- avoid simplifying the subst's multiple times · 7f16c95f
  Ralf Jung authored 4 years ago
  
  7f16c95f
- fix comment · 25e2378a
  Ralf Jung authored 4 years ago
  
  25e2378a
- use multiple free variables in reorder_alloc · c7cddb7e
  Ralf Jung authored 4 years ago
  
  c7cddb7e
- add tactic to prove expr_rel on open terms · 6fd84cbf
  Ralf Jung authored 4 years ago
  
  6fd84cbf
- port reorder_malloc to expr_rel · b89be956
  Ralf Jung authored 4 years ago
  
  b89be956
- move expr_rel to a separate file, and demand the substitution to be truly closing · de74a0fe
  Ralf Jung authored 4 years ago
  
  de74a0fe
- update dependencies · a4cef452
  Ralf Jung authored 4 years ago
  
  a4cef452
- start using expr_rel to state example theorems · 98a1b537
  Ralf Jung authored 4 years ago
  
  98a1b537