summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Expand)Author
2020-09-30Tweak Coq proof to avoid incompatibility with IrisBrian Campbell
2020-09-12Merge some of the gitignore filesColumbus240
2020-08-26Coq: replace other uses of omega with liaBrian Campbell
2020-08-26Coq: replace a lot of omega with liaBrian Campbell
2020-08-26Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issueBrian Campbell
2020-08-26Coq: make some uses of auto in the library more robustBrian Campbell
2020-06-17Coq: implement shl_int_1Brian Campbell
2020-06-14Coq: tidy up scope in libraryBrian Campbell
2020-06-12Coq: fix matching bug in solverBrian Campbell
2020-06-11Coq: specialise the andor solvers to avoid excessive search and solve more goalsBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-04-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
2020-01-17Coq: add hex_strBrian Campbell
2020-01-07Coq: accelerate wp steps by improving application of existing specsBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
2019-12-09Coq: improve solver enough to handle arm specBrian Campbell
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
2019-12-05Coq: more solving support for boolean predicatesBrian Campbell
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
2019-11-20Coq: port a couple of definitions from Isabelle for address translation specBrian Campbell
2019-11-13Coq: more proof supportBrian Campbell
2019-11-04Coq: compatiblity with 8.10 as well as 8.9Brian Campbell
2019-10-25Coq: make sure solver can't accidentally use recursive definitionsBrian Campbell
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
2019-10-18Coq: tweak a state monad lifting rule to improve performanceBrian Campbell
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
2019-09-19Change Coq Hoare logic rules to produce nicer preconditionsBrian Campbell
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-08-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-08-14Coq library work for proofs:Brian Campbell
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
2019-07-31Coq: Update barrier definitionsBrian Campbell
2019-07-31Coq: tweak Hoare proofs a littleBrian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-29Coq: add state monad version of while/until loops and lifting resultsBrian Campbell
2019-07-25Update Coq barrier definitionBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
2019-06-27Coq: less constrained version of slice for ARM modelBrian Campbell
2019-06-21Coq: even more robust handling of unknown goalsBrian Campbell
2019-06-21Coq: better handling of unknown constraintsBrian Campbell
2019-06-20Coq: avoid some unnecessary reduction in the constraint solverBrian Campbell
2019-06-13Coq: add eq_bit built-inBrian Campbell
2019-06-11Coq: add concatenation operator for polymorphic vectorsBrian Campbell
2019-06-06Coq: more aggressive rewriting before solvingBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:47:12 +0000