issues
search
mit-plv
/
riscv-coq
RISC-V Specification in Coq
BSD 3-Clause "New" or "Revised" License
109
stars
17
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Adapt to https://github.com/coq/coq/pull/19530
#39
proux01
opened
2 months ago
0
Leakage Traces
#38
OwenConoly
opened
4 months ago
10
[coq-platform] Smoke test broken
#37
rtetley
opened
8 months ago
3
Please create a tag for Coq 8.19 in Coq Platform 2024.01
#36
rtetley
closed
8 months ago
0
Add `install-all`, `install-spec` targets
#35
JasonGross
closed
9 months ago
0
Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10
#34
rtetley
closed
1 year ago
3
Adapt w.r.t. coq/coq#17322.
#33
ppedrot
closed
1 year ago
3
Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03
#32
MSoegtropIMC
closed
1 year ago
2
Add BoolSpec instances for verify
#31
JasonGross
opened
2 years ago
2
Adapt w.r.t. coq/coq#16004
#30
Alizter
closed
2 years ago
0
Support `EXTERNAL_COQUTIL=1`
#29
JasonGross
closed
2 years ago
0
Adapt to Coq PR #13664: keywords starting with a number can now be effectively used in the parser
#28
herbelin
closed
3 years ago
2
Add field to MMIOSpec for hardware guarantees
#27
jadephilipoom
closed
3 years ago
3
CI fails on master
#26
JasonGross
closed
4 years ago
1
Add .gitattributes
#25
JasonGross
closed
4 years ago
0
Add install target
#24
JasonGross
closed
5 years ago
0
ExtSpec for FE310
#23
joonwonc
closed
5 years ago
1
Use COQPATH for coqutil and allow using COQPATH for riscv-coq
#22
JasonGross
closed
5 years ago
0
Add Travis CI
#21
JasonGross
closed
5 years ago
1
Formalising the privileged specification
#20
Columbus240
opened
5 years ago
0
Document the overall structure
#19
Columbus240
opened
5 years ago
0
Avoid relying on `Export` bugs
#18
maximedenes
closed
5 years ago
3
Add documentation
#17
Columbus240
opened
5 years ago
2
Ideas about implementing multiple harts
#16
Columbus240
opened
5 years ago
1
Simplify with* functions of MetricRiscvMachine
#15
Columbus240
closed
5 years ago
1
Speed up instance proofs of `Primitives`
#14
Columbus240
closed
5 years ago
5
Remove some trailing whitespace
#13
Columbus240
closed
5 years ago
0
Implement ExecuteA and ExecuteA64
#12
Columbus240
closed
5 years ago
13
Add restrictions to `RiscvMachine`
#11
Columbus240
closed
5 years ago
7
Minimal MMIO Instance with metrics
#10
Carotti
closed
5 years ago
0
Add info about supported ISA extensions to README
#9
Columbus240
closed
5 years ago
8
Add [runsTo_det_step]
#8
tchajed
closed
5 years ago
0
Add metric logging
#7
Carotti
closed
5 years ago
0
Fix build on Windows
#6
JasonGross
closed
5 years ago
0
Add metric logging capabilities
#5
Carotti
closed
5 years ago
0
Add `coqutil` as dependency in README.md
#4
Columbus240
closed
5 years ago
1
non-vectored interrupts?
#3
andres-erbsen
closed
5 years ago
2
Export BinIntDef in util.Word
#2
JasonGross
closed
6 years ago
0
Prepare porting to lia
#1
maximedenes
closed
6 years ago
0