aboutsummaryrefslogtreecommitdiff
path: root/handwritten_support
AgeCommit message (Expand)AuthorFilesLines
2026-01-27Add a missed file for the Lean build fix in #1499. (#1505)Prashanth Mundkur1-1/+1
2026-01-24Update Lean builds to use separate Sail support library (#1499)Brian Campbell1-1/+1
2026-01-19Add rocq `sys_enable_experimental_extensions` definition (#1497)Jordan Carlin1-0/+2
2025-12-12add ConcurrencyInterfaceV1 as required by Nov lean nightly toolchain (#1423)Julie Newcomb1-0/+1
2025-12-10Lean: adapt to Sail change (#1420)Léo Stefanesco1-0/+1
2025-11-12Support a configurable reservation set size. (#1386)Prashanth Mundkur2-2/+2
2025-10-28Rocq updates (#1359)Brian Campbell3-38/+13
2025-09-16Return softfloat flags and result as a tuple (#1275)Tim Hutt3-268/+268
2025-09-14Add support for Zfbfmin extension (#1158)Nadime Barhoumi3-0/+4
2025-09-14Fix experimental extension failure in theorem prover targets (#1272)Jordan Carlin3-0/+4
2025-09-07Reset PC on reset, and improve tohost address handling (#1247)Tim Hutt5-26/+0
2025-09-02Remove unused definitions from handwritten_support files (#1252)Jordan Carlin3-131/+0
2025-09-02Update copyright header in handwritten_support files (#1249)Jordan Carlin7-325/+29
2025-06-24Remove speculate_conditional (#1060)Tim Hutt4-9/+0
2025-06-05Add executable version of the Lean model (#991)Léo Stefanesco1-0/+150
2025-05-12Add the Zawrs extension (#777)Prashanth Mundkur3-0/+3
2025-04-30Disable HTIF when the `tohost` symbol is not foundMingzhu Yan3-0/+5
2025-04-11Update Isabelle and Rocq supportBrian Campbell6-350/+18
2025-04-03Change extensionEnabled to currentlyEnabledJordan Carlin1-1/+1
2025-04-02Add cmake support for RocqBrian Campbell2-0/+18
2025-03-28Lean: refine sizeOf instance for extension typeJakob von Raumer1-14/+3
2025-03-23Fix Lean support for ZvkbTobias Grosser1-0/+1
2025-03-17Lean: remove printing dummies that are now in the sail's Sail.leanJakob von Raumer1-4/+0
2025-02-28Lean: update handwritten supportLéo Stefanesco1-6/+6
2025-02-27Lean: improve handwritten supportLéo Stefanesco1-2/+22
2025-02-24Handwritten support for the Lean backendLéo Stefanesco1-0/+141
2025-01-23Update support for Coq outputBrian Campbell2-14/+19
2024-11-29Remove N extension flagJordan Carlin3-9/+0
2024-08-29Implement Zicbom, Zicboz (cbo.flush, cbo.inval, cbo.zero)Tim Hutt2-0/+8
2024-05-10lem: Add PMP related stubs for Isabelle buildAlasdair1-0/+8
2024-02-05Improve PMP supportTim Hutt2-8/+0
2023-12-19lem: Fix issues created by vector extensionAlasdair7-688/+146
2023-10-17RISC-V Vector Extension SupportXinlai Wan1-0/+9
2023-10-11Rename enable-fiom to enable-writable-fiomTim Hutt3-7/+7
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 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
generated by cgit v1.1 at 2026-03-10 02:54:49 +0000