aboutsummaryrefslogtreecommitdiff
path: root/handwritten_support
AgeCommit message (Expand)AuthorFilesLines
2023-10-11Implement menvcfgTim Hutt3-0/+9
2023-06-15Run the pre-commit hook on all filesAlex Richardson7-72/+72
2023-05-31Fix build for Coq 8.17Michael Sammler1-1/+1
2023-05-31Coq updates for Sail 0.15Brian Campbell2-15/+1
2023-05-29apply_headers: regenerate copyright headersupdate-copyright-headersPhilipp Tomsich6-6/+18
2023-05-29Add Zfa extension support (excl. quad-precision)Philipp Tomsich1-0/+27
2023-02-23Remove duopodBrian Campbell1-5/+0
2022-08-09Minimal updates for Coq proof assistant outputBrian Campbell1-2/+4
2022-01-19Add support for Zfh extension (#129)Bilal Sakhawat2-0/+128
2021-11-22Implement support for Zfinx (#130)Jessica Clarke4-0/+16
2021-11-17Revert "Initial introduction of zfinx (#75)"Jessica Clarke4-16/+0
2021-11-17Initial introduction of zfinx (#75)Ibrahim Abu Kharmeh4-0/+16
2021-10-18scalar-crypto: Initial commit of 1.0.0-rc2 spec work. (#99)Ben Marshall2-0/+8
2021-07-29Use headache to apply copyright header at request of Peter Sewell.Robert Norton6-0/+408
2021-02-11Make N extension configurable.Prashanth Mundkur5-0/+17
2020-06-15Remove obsolete Coq axiomBrian Campbell1-2/+0
2020-06-15Update handwritten Coq support files to match current Sail.Brian Campbell2-10/+4
2020-04-07Switch floating-point comparisons to using softfloat to avoid missed corner-c...Prashanth Mundkur2-0/+32
2020-01-23Add lem stubs for softfloat externs.rsnikhilPrashanth Mundkur2-0/+218
2020-01-22Some fixes for lem build.Prashanth Mundkur2-0/+8
2020-01-22Fix coq build.Prashanth Mundkur1-0/+1
2020-01-17Update handwritten Coq to use boolean predicatesBrian Campbell2-11/+13
2019-11-26Fix RV32 Coq buildThomas Bauereiss1-4/+4
2019-11-25Fix RV32 Lem buildThomas Bauereiss2-4/+4
2019-10-09Add {read,write}_ram for CoqThomas Bauereiss1-0/+11
2019-10-09Read/write memory values and metadata together atomicallyThomas Bauereiss2-0/+32
2019-08-13Update barriers in Coq.Brian Campbell1-11/+11
2019-07-18Make sure everything builds correctlyAlasdair Armstrong2-45/+79
2019-07-18Revert "Support DMB/DSB domains"Alasdair Armstrong2-22/+22
2019-07-18Support DMB/DSB domainsShaked Flur2-22/+22
2019-06-24Add PMP checks to physical memory accesses.Prashanth Mundkur2-0/+8
2019-04-25Fix coq build.Prashanth Mundkur1-19/+19
2019-04-25riscv_extras.lem: update read/write_mem calls with (dummy) addrsize argumentJon French1-18/+18
2019-04-10Update Coq memory interfacesBrian Campbell1-20/+27
2019-04-04Add `sys_enable_writable_misa` and `sys_enable_rvc` to Coq extras fileBrian Campbell1-0/+3
2019-04-03Tweak print_* bindings for LemThomas Bauereiss2-0/+6
2019-04-01Add missed lem definitions for sys misa/rvcflags.Prashanth Mundkur2-0/+16
2019-02-26Restore riscv_extras damaged by merge.Prashanth Mundkur1-9/+13
2019-02-13Make repository have shape RMEM expectsAlasdair Armstrong4-3/+140
2019-02-13Switch version of riscv_extras.lem depending on Sail versionAlasdair Armstrong1-0/+137
2019-01-22Add build Makefile targets for prover backendsThomas Bauereiss1-4/+6
2019-01-21Output auxiliary Isabelle theories into generated_definitions/isabelleThomas Bauereiss1-2/+2
2019-01-19Moved gen/ to handwritten_support/hgenShaked Flur19-0/+1367
2019-01-16More reorg.Prashanth Mundkur5-0/+439
generated by cgit v1.1 at 2024-07-24 09:23:41 +0000