Commits · 5a02b19f52a3087b25971cb26b39a9f3f1eaeeff · cambium / cosmo

16 Feb, 2021 1 commit
- remove files commited by mistake · 5a02b19f
  Glen Mével authored Feb 16, 2021
  
  5a02b19f
12 Feb, 2021 4 commits
- start draft for paper about queue · d816ee5a
  Glen Mével authored Feb 12, 2021
  
  d816ee5a
- add proof of a simple pipeline (WIP) · f1fc18a8
  Glen Mével authored Feb 12, 2021
  
  f1fc18a8
- fix some OFEs · 819bc5be
  Glen Mével authored Feb 12, 2021
  
  819bc5be
- bounded queue: add spec for end-user enqueue/dequeue function · cf245895
  Glen Mével authored Feb 12, 2021
  
  cf245895
29 Jan, 2021 2 commits
- circular buffer: cleanup (rename stuff) · 64083a0f
  Glen Mével authored Jan 29, 2021
  
  64083a0f
- circular buffer: cleanup · 6abb9421
  Glen Mével authored Jan 29, 2021
  
  6abb9421
27 Jan, 2021 1 commit
- circular buffer: removed unneeded assertions from invariant · 53228669
  Glen Mével authored Jan 27, 2021
  
  53228669
22 Jan, 2021 1 commit
- circular buffer: proof of try_dequeue_spec · 0d115bda
  Glen Mével authored Jan 22, 2021
  
  0d115bda
03 Dec, 2020 1 commit
- circular buffer: support any capacity ≥ 1 by changing the encoding of statuses · 9f2fcc85
  Glen Mével authored Dec 18, 2020
  
  9f2fcc85
08 Dec, 2020 1 commit
- Whitespace, bump Iris. · 90032127
  Jacques-Henri Jourdan authored Dec 08, 2020
  
  90032127
03 Dec, 2020 3 commits
- WIP on the circular buffer: fill remaining gaps in the proof of `enqueue` · 91821a1d
  Glen Mével authored Dec 03, 2020
  
  91821a1d
- WIP on the circular buffer: remove redundant lemmas · eb19b4fa
  Glen Mével authored Dec 03, 2020
  
  eb19b4fa
- WIP again on the circular buffer · 9859019e
  Glen Mével authored Dec 03, 2020
  
  9859019e
08 Dec, 2020 1 commit
- more WIP on the circular buffer · 703d46f4
  Glen Mével authored Nov 15, 2020
  
  703d46f4
17 Nov, 2020 1 commit
- Cleanup vprop.v, better solve_monPred_in · d36633ad
  Jacques-Henri Jourdan authored Nov 17, 2020
  
  d36633ad
09 Nov, 2020 3 commits
- more WIP on the circular buffer · a12c4da0
  Glen Mével authored Nov 09, 2020
  
  a12c4da0
- more lemmas about Z-indexed lists · ceac119c
  Glen Mével authored Nov 09, 2020
  
  ceac119c
- remove unused things from base, add lattice for Z · 54bf4972
  Glen Mével authored Nov 09, 2020
  
  54bf4972
26 Oct, 2020 2 commits
- fix tactics for working with full arrays · dcb11f23
  Glen Mével authored Oct 27, 2020
  
  dcb11f23
- bump Iris · b956ace9
  Glen Mével authored Oct 22, 2020
  
  b956ace9
22 Oct, 2020 1 commit
- WIP on the circular buffer · fad54648
  Glen Mével authored Jul 02, 2020
  
  fad54648
16 Jul, 2020 1 commit
- add logical atomicity · 89acbcd7
  Glen Mével authored Jul 02, 2020
  
  89acbcd7
09 Jul, 2020 1 commit
- use Z as much as possible · b725bcf6
  Glen Mével authored Jul 09, 2020
  
  b725bcf6
15 Jun, 2020 1 commit
- update proofmode to work with arrays · 920f8b4b
  Glen Mével authored Jun 15, 2020
  
  920f8b4b
30 Apr, 2020 2 commits
- simplify proof of sp_alloc · 6f5a5346
  Jacques-Henri Jourdan authored Apr 30, 2020
  
  6f5a5346
- prove mapsto_na_block_equiv · 1d1eb80f
  Jacques-Henri Jourdan authored Apr 30, 2020
  
  1d1eb80f
29 Apr, 2020 2 commits
- re-prove adequacy · bdb1b0b6
  Glen Mével authored Apr 29, 2020
  
  bdb1b0b6
- end of lifting lemmas, fix blockwise store ownership and prove lemmas about it · 5a0f2f55
  Glen Mével authored Apr 29, 2020
  
  5a0f2f55
16 Apr, 2020 11 commits
- cleanup · 226ff4c3
  Glen Mével authored Apr 16, 2020
  
  226ff4c3
- proofs of all remaining lifting lemmas of the base logic · 3aa4bcdc
  Glen Mével authored Apr 16, 2020
  
  3aa4bcdc
- wp_write_na_view_lang · af608f41
  Glen Mével authored Apr 16, 2020
  
  af608f41
- gitignore even more files · 637765b2
  Glen Mével authored Apr 16, 2020
  
  637765b2
- gitignore more compiled files · 18787c36
  Glen Mével authored Apr 16, 2020
  
  18787c36
- Merge branch 'arrays' of gitlab.inria.fr:gmevel/momm into arrays · bcbf621d
  Glen Mével authored Apr 16, 2020
  
  bcbf621d
- simplify seen_interp to pure Coq · 82ee0e39
  Glen Mével authored Apr 14, 2020
  
  82ee0e39
- rename to_store_cmra into store_to_cmra · 143c38b1
  Glen Mével authored Apr 11, 2020
  
  143c38b1
- reorder parameters of constructors of `head_step` · 2b79c3ac
  Glen Mével authored Apr 11, 2020
  
  2b79c3ac
- `mem_step` is now store-wide · a43308a8
  Glen Mével authored Apr 11, 2020
```
also, `action` and `transition_label` have been merged and the new
datastructure is called `mem_event`
```
  a43308a8
- turn more type aliases into notations · 98b932d7
  Glen Mével authored Apr 09, 2020
  
  98b932d7