Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • alloc_align
  • bits-deep-backup
  • case-pgtable
  • ci/VerifyThis2021
  • ci/VerifyThis2022
  • ci/allocstack
  • ci/bff-artifact
  • ci/bits-record-param
  • ci/bitvec_typed
  • ci/bool-simpl
  • ci/case-mt7601u
  • ci/case_router
  • ci/free_no_layout
  • ci/frontent_fix
  • ci/lithium-dissertation-sammler
  • ci/more-bit-cases
  • ci/more_prov
  • ci/pkvm-hof
  • ci/pldi21-submission-artifact
  • ci/ptrfrag
  • vip-popl22-submission-artifact
  • pldi21-submission-artifact
22 results
Created with Raphaël 2.2.011Aug653230Jul28272620191716151413129865330Jun292825242221181614109754231May272521201929Apr282723191615148231Mar302927262524231698542126Feb25242322191817161512111085432129Jan282726232219181514121117Dec11987643230Nov2726252420181716131211109543229Oct222172130Sep29261715147432131Aug2827201829Jul28272321adapt proofs to macrosre-verify pgtable client functionsstick to old name 'Z_lunot_spec'nat -> Zrebase from masterprove new rewriting rulesMByte sig changetest solve_Z_eqrename Hcase -> HCASEmore tests on prove_Zeq_bitwiseadd coqutil Z and bitblast testsproofs: Z bits simpl rulessimpl rules for pgtable client functionsfinish macro proofs; update gencodeverify macro using Zredefine mask, data with Z opsadd rewriting rulesminor for rebaseupdate spec of kvm_pte_tablefinish kvm_pte_table with manual tacticssimpl rulesclean up some proofs in bitvecproofs: genenal typing rules for bitwise op and negtype_val_expr_wandpure lemmas proofsproving pure lemmasgeneral lemmas for typing rulesbinary to rule them allupdate definitions of bin functions; resolve a few pure sideconddraft impl for mask uniontry adding typing rules for bitsbitvec is Copyablesimplify bvec ops and proofsencode bvec as vec booldefine bitvec typehelper typestry define and customize fieldsdraftpgtable case study code draftadd subsumption between values of structures