Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Jan 6, 2020

• A shorter proof for dom_ord2 by @anton-trunov

  germanD

  committed
  23667bd

  Copy full SHA for 23667bd

Commits on Jan 3, 2020

• Fix compilation of SeqFacts.v with mathcomp dev's branch

  Show description for 935b73d
  germanD

  committed
  935b73d

  Copy full SHA for 935b73d

Commits on Feb 20, 2019

• Properly instantiate Blocks (see Types.v)

  

  George Pîrlea

  committed
  9080de8

  Copy full SHA for 9080de8

Commits on Feb 18, 2019

• Only 'Address' left to extract as a type

  

  George Pîrlea

  committed
  cfbcf4c

  Copy full SHA for cfbcf4c

• Confused about how to extract types

  

  George Pîrlea

  committed
  29507d3

  Copy full SHA for 29507d3

Commits on Feb 17, 2019

• 'Address' is a Protocol concern

  Show description for 363cde3
  

  George Pîrlea

  committed
  363cde3

  Copy full SHA for 363cde3

• Finish making Toychain modular

  Show description for ff665d8
  

  George Pîrlea

  committed
  ff665d8

  Copy full SHA for ff665d8

• WIP Structure things into modules

  

  George Pîrlea

  committed
  4a75599

  Copy full SHA for 4a75599

Commits on Feb 16, 2019

• Sketch a structure for extraction

  

  George Pîrlea

  committed
  6bca7be

  Copy full SHA for 6bca7be

• Change VAF to take whole block as argument

  Show description for a2beae0
  

  George Pîrlea

  committed
  a2beae0

  Copy full SHA for a2beae0

• Separate 'Blocks.v' file again

  Show description for ee35375
  

  George Pîrlea

  committed
  ee35375

  Copy full SHA for ee35375

• Move all parameters & axioms to 'Parameters.v'

  

  George Pîrlea

  committed
  aad5680

  Copy full SHA for aad5680

Commits on Feb 15, 2019

• WIP progress on invariant

  

  George Pîrlea

  committed
  830144f

  Copy full SHA for 830144f

Commits on Jan 26, 2019

• WIP invariant

  

  George Pîrlea

  committed
  ae9a7c4

  Copy full SHA for ae9a7c4

Commits on Jan 25, 2019

• WIP Prove btExtend_fold_comm

  

  George Pîrlea

  committed
  d6d1cb4

  Copy full SHA for d6d1cb4

• WIP Fix breakage

  

  George Pîrlea

  committed
  2c324ea

  Copy full SHA for 2c324ea

Commits on Jan 23, 2019

• WIP Can this be proven without validH?

  

  George Pîrlea

  committed
  06104d9

  Copy full SHA for 06104d9

• WIP prove btExtend_fold_in_either

  

  George Pîrlea

  committed
  1b15661

  Copy full SHA for 1b15661

• WIP progress & move stuff around

  

  George Pîrlea

  committed
  8d84646

  Copy full SHA for 8d84646

• WIP btExtendV_fold_dup

  

  George Pîrlea

  committed
  7976e0f

  Copy full SHA for 7976e0f

Commits on Jan 21, 2019

• WIP Prove btExtendV_comm

  

  George Pîrlea

  committed
  7a7f9b3

  Copy full SHA for 7a7f9b3

Commits on Jan 20, 2019

• WIP fold_comm

  

  George Pîrlea

  committed
  b67b746

  Copy full SHA for b67b746

Commits on Jan 5, 2019

• Finish refactoring Forests.v

  

  George Pîrlea

  committed
  a83eaab

  Copy full SHA for a83eaab

• WIP

  

  George Pîrlea

  committed
  3c17191

  Copy full SHA for 3c17191

Commits on Jan 2, 2019

• WIP

  

  George Pîrlea

  committed
  7922512

  Copy full SHA for 7922512

• Prove btExtend_chain_prefix

  

  George Pîrlea

  committed
  ec2f1c3

  Copy full SHA for ec2f1c3

• Prove btExtend_comm

  

  George Pîrlea

  committed
  f570b18

  Copy full SHA for f570b18

• WIP replace hashB_inj with PCM reasoning

  

  George Pîrlea

  committed
  fb82f0f

  Copy full SHA for fb82f0f

Commits on Dec 29, 2018

• Prove in_ext in terms of hashB_inj

  

  George Pîrlea

  committed
  b28bb76

  Copy full SHA for b28bb76

• Fix breakage in other files; prep for refactor

  

  George Pîrlea

  committed
  8ef3356

  Copy full SHA for 8ef3356

Commits on Dec 28, 2018

• Remove one more use of hashB_inj

  

  George Pîrlea

  committed
  ae58f28

  Copy full SHA for ae58f28

• Remove some unnecessary uses of hashB_inj

  

  George Pîrlea

  committed
  c1162c5

  Copy full SHA for c1162c5

Commits on Dec 21, 2018

• Restrict inconsistency within in_ext lemma

  Show description for 1bee7fe
  

  George Pîrlea

  committed
  1bee7fe

  Copy full SHA for 1bee7fe

Commits on Dec 20, 2018

• Make compute_chain' collision-resilient

  

  George Pîrlea

  committed
  160c18e

  Copy full SHA for 160c18e

• Start removing hashB_inj

  

  George Pîrlea

  committed
  1ba057b

  Copy full SHA for 1ba057b

Pagination

Previous

Next