summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2020-04-21Fix sub_bits interpreter bindingThomas Bauereiss
2020-04-21Add more monomorphisation rewritesThomas Bauereiss
Supporting more ASL idioms
2020-04-21Add support for some ASL idioms in mono rewritesThomas Bauereiss
2020-04-21Add more mono rewrites for bitvector subrangesThomas Bauereiss
2020-04-10Add Lem builtins for operations on realsThomas Bauereiss
... that match the names in lib/real.sail. Also fix the lem mapping for abs_int_atom and a Lem syntax error with nested record updates.
2020-04-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-02-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2020-02-21Add barriers to regfp.sail for full ARMv8Alasdair Armstrong
Again use an $ifdef to avoid breaking RMEM. We can't use the same barrier_kind, because we *really* want a plain enumeration both for its simple SMT representation and a simple 1 to 1 mapping to the cat models used by herd. Technically for Isla, all the read_kind/write_kind/barrier_kind etc types can be defined separately on a per-architecture basis anyway, so maybe using this file at all is a bit of an anachronism.
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2020-02-03Add an __instr_announce builtin in regfp.sailAlasdair Armstrong
Allows keeping track of which instructions actually get executed in a trace
2020-02-03Update regfp.sail with ifetch changes from poly_mapping branchAlasdair Armstrong
However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because otherwise the generated lem for RMEM will break.
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
Also be more careful to avoid pattern bindings with identifiers to avoid parsing clashes, eg `let 'bytes := ...` which is confused with the notation for binary literals.
2020-01-17Merge branch 'coq-bool-props' into sail2Brian Campbell
2020-01-17Coq: add hex_strBrian Campbell
Now used in RISC-V model.
2020-01-07Coq: accelerate wp steps by improving application of existing specsBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
- add liftRS support to tactics - define uint and sint in terms of functions without proof terms - eq_vec correctness - lemma that rounding up integers using reals is the obvious integer calculation - another proof irrelevance tactic - try lemmas in the sail hintdb both before and after goal processing
2019-12-09Coq: improve solver enough to handle arm specBrian Campbell
- break up goals more in unbool - remove intuition from guess_ex_solver because it can be too expensive - flip goals around because the side that evars appears on has changed - generalise the and/or tactics - make a couple of tactics more specific/robust
2019-12-06Don't introduce uneccesary control flow when compilingAlasdair Armstrong
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
Includes removing an explicit use of a lemma generated by abstract, which was causing problems with different versions of Coq because the names change.
2019-12-05Coq: more solving support for boolean predicatesBrian Campbell
Mostly from making the aarch64 model compile again - switch order some arithmetic lemmas - move list membership rewrites alongside other comparisons to enable more rewriting - copy hypotheses used in other types/definitions so that they can be rewritten - lift boolean existentials out of implications in hypotheses so they can be used as witnesses without proving the condition - add negation to solve_bool_with_Z - add some new bool solving for goals from and_boolMP/or_boolMP
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
- ArithFact takes a boolean predicate - defined in terms of ArithFactP, which takes a Prop predicate, and is used directly for existentials - used abstract in more definitions with direct proofs - beef up solve_bool_with_Z to handle more equalities, andb and orb
2019-11-21Implement -cycle-limit option for OCaml emulator similar to one for C.Robert Norton
2019-11-20Coq: port a couple of definitions from Isabelle for address translation specBrian Campbell
2019-11-14Update location of sail2_instr_kinds.lemRobert Norton
2019-11-14Perform isabelle check only when heap-img rule is used to avoid calling opam ↵Robert Norton
(which might not be present).
2019-11-13Coq: more proof supportBrian Campbell
- add state versions of foreach combinators - support dependent sumbool pattern matching (i.e., those where the property is actually used) - add rewriting congruence rules, state monad lifting rules, and invariant proof rules for these
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
- requires fixpoint definitions containing proofs to be processed in proof mode (due to a bug in Coq), so change libraries and pretty printing to do that - adjust some lemmas to avoid extra evars
2019-10-18Coq: tweak a state monad lifting rule to improve performanceBrian Campbell
2019-10-17Allow generating C that doesn't hard code any librariesAlasdair Armstrong
2019-10-16Now builds arm address translation with clang -target aarch64-none-eabiAlasdair Armstrong
Some builtins need properly implementing still Use modified spinlock implementation from hafnium with stdatomic, rather than assembly
2019-10-16Make nostd Sail arena allocator thread safe (maybe)Alasdair
2019-10-15More work on bare-metal SailAlasdair Armstrong
2019-10-14Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and ↵Alasdair Armstrong
bitvectors in C Assumes a Sail C library that has functions with the right types to support this. Currently lib/int128 supports the -Ofixed_int option, which was previously -Oint128. Add a version of Sail C library that can be built with -nostdlib and -ffreestanding, assuming the above options. Currently just a header file without any implementation, but with the right types
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
It only produces them when necessary (because some types do not have decidable equality due to embedded proofs). Also add trivial instance for the unit type.
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
- in particular at monadic interfaces (i.e., sufficient for instruction ast types) - see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an example that's not currently supported - generate definitions for type-level Bool definitions (i.e., predicates)
2019-09-19Change Coq Hoare logic rules to produce nicer preconditionsBrian Campbell
In particular, shift state lambdas outside of if/match/let which avoids unnecessary abstraction/applications. Add more rules to the tactic.
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
Also tweak the informative and/or boolean definitions so that they use the same proofs in both monads.
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-29Turn the two abs_int declarations into overloadsBrian Campbell
(otherwise Sail uses the type from one and the extern from the other)
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-14Use bitvector type in mono rewritesThomas Bauereiss
Also don't require a previously declared default vector indexing order in vector_dec.sail.
2019-08-14Fix bug in mono rewritesThomas Bauereiss
2019-08-14Coq library work for proofs:Brian Campbell
* rename state fields to avoid clash with regstate type * use rewriting to automate some proofs
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
Add count_leading_zeros, and correct a precedence error in min/max.
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
Mostly in the Coq backend, plus a few testcases that use bitvector builtins on poly-vectors (which works on some backends, but not Coq). Also handle some additional list inclusion proofs in Coq.
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-07-31Coq: Update barrier definitionsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 06:51:26 +0000