Commits · 612e3938c87967a6a0f7d653f543c52317d25495 · Iris / c

01 Nov, 2018 6 commits
- incorrect proof of acquire · 05b75498
  Dan Frumin authored Nov 01, 2018
  
  05b75498
- Implement `own_frag_emp` · 823bfcad
  Dan Frumin authored Nov 01, 2018
  
  823bfcad
- Prove the specification for cancel · 00c5460f
  Dan Frumin authored Nov 01, 2018
  
  00c5460f
- Simplify a proof · 8d7a6268
  Dan Frumin authored Nov 01, 2018
  
  8d7a6268
- flocked accessor · 3736872f
  Dan Frumin authored Nov 01, 2018
  
  3736872f
- A wee bit of cleanup · 2299d5e8
  Dan Frumin authored Nov 01, 2018
  
  2299d5e8
31 Oct, 2018 3 commits
- FLOCK FREE ADMIT THREE · 79e07b5f
  Dan Frumin authored Oct 31, 2018
  
  79e07b5f
- Get rid of two admits · cd9c189a
  Dan Frumin authored Oct 31, 2018
  
  cd9c189a
- FLOCK FLOCK FLOCK ?!?!?!? · c5ec5ddf
  Dan Frumin authored Oct 31, 2018
  
  c5ec5ddf
10 Jul, 2018 1 commit
- Remove an admit from flock.v · 45e74acc
  Dan Frumin authored Jul 10, 2018
  
  45e74acc
30 Jun, 2018 1 commit
- working in progress on a_par. Captain crew, take off. · 97c0d2c3
  Léon Gondelman authored Jun 30, 2018
  
  97c0d2c3
15 Jun, 2018 1 commit
- WIP: multi-flock-res acquire · 92e9852f
  Dan Frumin authored Jun 15, 2018
  
  92e9852f
07 Jun, 2018 2 commits
- [flock2] Get rid of some admits · 2985f8dd
  Dan Frumin authored Jun 07, 2018
  
  2985f8dd
- [flock2] flock_res is fractional · 8f5c5363
  Dan Frumin authored Jun 07, 2018
  
  8f5c5363
04 Jun, 2018 1 commit
- Flock v 2 · c4d5aec7
  Dan Frumin authored Jun 04, 2018
  
  c4d5aec7
31 May, 2018 1 commit
- fixed and proved vcgen with list of permissions · 9bcba503
  Léon Gondelman authored May 31, 2018
  
  9bcba503
28 May, 2018 5 commits
- More liberal masks in flock.v · 9c4c7f6d
  Dan Frumin authored May 28, 2018
  
  9c4c7f6d
- More flock.v cleaning · b33bd3c2
  Dan Frumin authored May 28, 2018
```
- Use all_props lemmas
```
  b33bd3c2
- Clean up flock.v · 7a195a66
  Dan Frumin authored May 28, 2018
```
- Reorder the lemmas
- Use to_props_map properties
```
  7a195a66
- Dynamically add resources to AWP · ece2644a
  Dan Frumin authored May 28, 2018
```
This implements
- Composable propositions in flock with `flock_res`
- Ability to add resources to AWP "on the fly"
```
  ece2644a
- Allow for dynamic allocation of propositions in the flock · c24f5451
  Dan Frumin authored May 27, 2018
  
  c24f5451
03 May, 2018 1 commit
- Use `gen_proofmode`. · 2abfd22c
  Robbert Krebbers authored May 03, 2018
  
  2abfd22c
29 Apr, 2018 1 commit
- Get rid of all the timeless stuff. · 08039edc
  Robbert Krebbers authored Apr 29, 2018
  
  08039edc
23 Apr, 2018 1 commit
- Implement the cancellable locks specification · 0672696e
  Dan Frumin authored Apr 23, 2018
  
  0672696e
22 Apr, 2018 1 commit
- The initial import of files · bb6daa40
  Léon Gondelman authored Apr 22, 2018
  
  bb6daa40