Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Feb 4, 2016

• New _CoqProject based build system

  Show description for 03ba4b3
  dwoos

  committed
  03ba4b3

  Copy full SHA for 03ba4b3

Commits on Feb 3, 2016

• added general simulation theorems for total params mappings, adapted ghost params results to use them

  

  palmskog

  authored and

  wilcoxjay

  committed
  89b97b1

  Copy full SHA for 89b97b1

Commits on Jan 28, 2016

• new ltac-in-terms syntax

  dwoos

  committed
  ae2a7ac

  Copy full SHA for ae2a7ac

Commits on Aug 13, 2015

• Fix trace proofs

  dwoos

  committed
  726fae7

  Copy full SHA for 726fae7

• Fix decomposition proofs

  dwoos

  committed
  674b8a7

  Copy full SHA for 674b8a7

Commits on Aug 6, 2015

• prove a list lemma!!!!!!!!!!!!

  wilcoxjay

  committed
  e5c4692

  Copy full SHA for e5c4692

Commits on Aug 5, 2015

• Refinement proof

  dwoos

  committed
  664f469

  Copy full SHA for 664f469

• port ghost log log matching!!!!

  wilcoxjay

  committed
  4cbff5f

  Copy full SHA for 4cbff5f

• port ghost logs log properties!

  wilcoxjay

  committed
  5f46653

  Copy full SHA for 5f46653

• port ghost log all entries!

  wilcoxjay

  committed
  69103e6

  Copy full SHA for 69103e6

• port SMS!

  wilcoxjay

  committed
  f453c97

  Copy full SHA for f453c97

• delete unused lemma in SMS!

  wilcoxjay

  committed
  446b373

  Copy full SHA for 446b373

• kill last SMS admit!!!

  wilcoxjay

  committed
  1dddba6

  Copy full SHA for 1dddba6

• fix duplicate lifted_entries_sorted_nw!!

  wilcoxjay

  committed
  9c7d8e0

  Copy full SHA for 9c7d8e0

• finish rest of CRC cases!

  wilcoxjay

  committed
  05fcf5f

  Copy full SHA for 05fcf5f

• Prove hAE preserves committed!

  dwoos

  committed
  e85143f

  Copy full SHA for e85143f

• preserve nw invariant in CRC hCR case!

  wilcoxjay

  committed
  d12d98c

  Copy full SHA for d12d98c

• establish nw invariant!

  wilcoxjay

  committed
  00fddd6

  Copy full SHA for 00fddd6

• finish CRC AE host case!

  wilcoxjay

  committed
  6f3c6dc

  Copy full SHA for 6f3c6dc

Commits on Aug 4, 2015

• correct statement of commit preservation thing

  dwoos

  committed
  9e8ee1f

  Copy full SHA for 9e8ee1f

• t' -> currentTerm in pre-state

  dwoos

  committed
  18238a9

  Copy full SHA for 18238a9

• kill first case of AE CRC host

  wilcoxjay

  committed
  e9c7f2b

  Copy full SHA for e9c7f2b

• lift SMSNW'

  dwoos

  committed
  e32551f

  Copy full SHA for e32551f

• wip commit_invariant_append_entries

  wilcoxjay

  committed
  e6843f4

  Copy full SHA for e6843f4

Commits on Aug 2, 2015

• prove GLAE

  dwoos

  committed
  04f7ede

  Copy full SHA for 04f7ede

• Prove ILIAE

  dwoos

  committed
  11ee763

  Copy full SHA for 11ee763

• state CRC nw invariant

  wilcoxjay

  committed
  fc4fbbc

  Copy full SHA for fc4fbbc

• lifted sms

  wilcoxjay

  committed
  1a95854

  Copy full SHA for 1a95854

Commits on Jul 31, 2015

• Ghost log log matching proved

  dwoos

  committed
  49cb6cc

  Copy full SHA for 49cb6cc

• Admit some invariants

  dwoos

  committed
  401707f

  Copy full SHA for 401707f

• Use pre-state instead of post state for ghost log

  dwoos

  committed
  6665c9f

  Copy full SHA for 6665c9f

• state and prove ghost logs log properties

  dwoos

  committed
  992d028

  Copy full SHA for 992d028

• Strengthen GhostLogCorrect

  dwoos

  committed
  430a050

  Copy full SHA for 430a050

Commits on Jul 30, 2015

• prove ghost_log_correct

  dwoos

  committed
  98f632c

  Copy full SHA for 98f632c

Commits on Jul 29, 2015

• fix E2E build.

  Show description for dc78c34
  wilcoxjay

  committed
  dc78c34

  Copy full SHA for dc78c34

Pagination

Previous

Next