sail/mips, branch sail2 Formal specification language for ISAs Remove old specs that have more up to date version 2020-07-31T12:30:53+00:00 Alasdair 2020-07-31T12:30:53+00:00 dd76fdfd819bb1a5423cea369df0e7f2ae449b62 Move outdated things into old subdirectory 
Move outdated things into old subdirectory
Remove cheri and mips specs -- they now have their own repository. 2018-09-21T14:11:56+00:00 Robert Norton 2018-09-21T14:09:08+00:00 2bdc5d09389c8fccd8100c0c07c54b2b8895c76a 






Coq: rework generation of dependent pairs so that they are only
2018-09-03T11:03:32+00:00

Brian Campbell

2018-09-03T11:00:16+00:00

5a947f5d5f5fd9b83f27bfd4e43170f51d4a27a7

constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.

Also
- Don't simplify nexps before printing (note that we usually end up
  needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
  because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
  fill in metavariables (because manipulating the goal can interfere with
  instantiating them)
- Update RISC-V patch





constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.

Also
- Don't simplify nexps before printing (note that we usually end up
  needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
  because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
  fill in metavariables (because manipulating the goal can interfere with
  instantiating them)
- Update RISC-V patch







Adapt theory imports for Isabelle 2018
2018-08-28T17:10:13+00:00

Thomas Bauereiss

2018-08-28T16:31:43+00:00

9232814ed220cff16e6cac808f327b326f2e2f2c

Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860





Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860







Add the type an expression was checked against to tannots, and use for Coq
2018-08-16T16:32:42+00:00

Brian Campbell

2018-08-16T16:32:32+00:00

18900d3c0da37c4dc7079749f84517fb7456e551

Tweak extra Coq files to match.
Tweak early return rewrite to use declared return type, which can always
be put into an E_cast.





Tweak extra Coq files to match.
Tweak early return rewrite to use declared return type, which can always
be put into an E_cast.







Coq mips: fix deprecation warning
2018-08-02T17:16:55+00:00

Brian Campbell

2018-08-02T17:16:45+00:00

430cf3778555fd9dfef5dccb3f57052df994cbc4












Coq: remove type removal holdover from Lem backend, add MIPS lemma
2018-08-02T17:16:55+00:00

Brian Campbell

2018-08-02T17:15:02+00:00

d2a01be233f1ea4bed66819096949aa4f56b2695












Merge remote-tracking branch 'origin/sail2' into c_fixes
2018-07-24T17:09:18+00:00

Alasdair Armstrong

2018-07-24T17:09:18+00:00

6b4f407ad34ca7d4d8a89a5a4d401ac80c7413b0












Now builds mips spec again.
2018-07-24T00:09:14+00:00

Alasdair

2018-07-24T00:09:14+00:00

dafb09e7c26840dce3d522fef3cf359729ca5b61

Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging





Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging







Coq: faster MIPS extras without confusing message
2018-07-23T15:15:53+00:00

Brian Campbell

2018-07-23T15:15:29+00:00

294ff935decaf8450bf3d3557218b936b473ce0b