Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Nov 8, 2024

• qed hist_extend_put

  sanjit-bhat

  committed
  588e45d

  Copy full SHA for 588e45d

Commits on Nov 7, 2024

• move reusable list lemmas

  sanjit-bhat

  committed
  9cc3891

  Copy full SHA for 9cc3891

Commits on Aug 16, 2024

• Bump iris and stdpp

  Show description for b1d1143
  tchajed

  committed
  b1d1143

  Copy full SHA for b1d1143

Commits on Jul 31, 2024

• add list helper lemmas for singleton / snoc exists

  sanjit-bhat

  committed
  6b7c0ab

  Copy full SHA for 6b7c0ab

Commits on Jul 12, 2024

• Improvements to list library for simplefs

  tchajed

  committed
  8d5a045

  Copy full SHA for 8d5a045

Commits on Apr 15, 2023

• Update stdpp

  

  proux01

  authored and

  RalfJung

  committed
  1410e48

  Copy full SHA for 1410e48

Commits on Dec 7, 2021

• Use strict bulleting more consistently

  tchajed

  committed
  e681641

  Copy full SHA for e681641

Commits on Nov 10, 2021

• Finish append_new_ghost

  tchajed

  committed
  66bbcc5

  Copy full SHA for 66bbcc5

Commits on May 21, 2021

• update std++ and Iris

  RalfJung

  committed
  e0950b5

  Copy full SHA for e0950b5

Commits on May 3, 2021

• ConditionalPut marshaling

  RalfJung

  committed
  51cf65a

  Copy full SHA for 51cf65a

Commits on Nov 20, 2020

• Move some helper theorems out of installer_proof

  tchajed

  committed
  860f7d0

  Copy full SHA for 860f7d0

• Prove circ_matches_txns can be combined

  Show description for c218234
  tchajed

  committed
  c218234

  Copy full SHA for c218234

Commits on Nov 16, 2020

• Prove subslice admit

  tchajed

  committed
  f56b6ec

  Copy full SHA for f56b6ec

Commits on Oct 20, 2020

• subslice/struct helper lemmas

  krawthekrow

  committed
  46affa2

  Copy full SHA for 46affa2

Commits on Oct 3, 2020

• some easy admits

  zeldovich

  committed
  1ee9827

  Copy full SHA for 1ee9827

Commits on Oct 2, 2020

• get rid of is_highest_txn

  Show description for f6d0027
  zeldovich

  committed
  f6d0027

  Copy full SHA for f6d0027

Commits on Sep 21, 2020

• another admit, hopefully did not break too much other stuff

  zeldovich

  committed
  d401458

  Copy full SHA for d401458

Commits on Aug 6, 2020

• Note something missing from the invariant

  tchajed

  committed
  79be743

  Copy full SHA for 79be743

Commits on Aug 4, 2020

• Port txns_ctx to new append_list algebra

  tchajed

  committed
  f33064b

  Copy full SHA for f33064b

• Implement append-only list algebra

  Show description for 607f4e4
  tchajed

  committed
  607f4e4

  Copy full SHA for 607f4e4

Commits on Jul 28, 2020

• - subslice list lemma helper

  Show description for c3b5473
  tslilyai

  committed
  c3b5473

  Copy full SHA for c3b5473

• prove concat_insert_app

  tslilyai

  committed
  fbb2513

  Copy full SHA for fbb2513

Commits on Jul 25, 2020

• Prove byte decoding

  Show description for b5f0568
  tchajed

  committed
  b5f0568

  Copy full SHA for b5f0568

Commits on Jul 24, 2020

• Add partial reimplementation of marshal proof

  Show description for b038d97
  tchajed

  committed
  b038d97

  Copy full SHA for b038d97

Commits on Jul 21, 2020

• change proofs to use concat, adding admitted concat lemma in List.v

  tslilyai

  committed
  41d9d14

  Copy full SHA for 41d9d14

Commits on May 12, 2020

• Finish up proof of wp_endGroupTxn

  tchajed

  committed
  2fed034

  Copy full SHA for 2fed034

Commits on May 11, 2020

• Finish re-proving lock invariant after append

  tchajed

  committed
  d1cff1d

  Copy full SHA for d1cff1d

Commits on May 6, 2020

• Merge branch 'wal-sliding'

  tchajed

  committed
  ca36954

  Copy full SHA for ca36954

• Fix moved proof

  tchajed

  committed
  e59ecd1

  Copy full SHA for e59ecd1

Commits on May 5, 2020

• Product/Sum rules, fill in shelved evars.

  jtassarotti

  committed
  221b0d7

  Copy full SHA for 221b0d7

• Move subslice to Helpers/List

  tchajed

  committed
  6a37263

  Copy full SHA for 6a37263

• Struct offset case in logical reln.

  jtassarotti

  committed
  8f87836

  Copy full SHA for 8f87836

Commits on May 1, 2020

• Add incl_Forall for Coq v8.11 compatibility

  tchajed

  committed
  8ab3fb6

  Copy full SHA for 8ab3fb6

Commits on Apr 25, 2020

• Add missing lemma for Coq 8.11 compat

  tchajed

  committed
  686051c

  Copy full SHA for 686051c

• minor admits

  zeldovich

  committed
  a3db289

  Copy full SHA for a3db289

Pagination

Previous

Next