Skip to content

Activity

Port to dune and fix warnings

tperamicreated dune • 0f9a2f3 • 
9 days ago

acks

bacampushed 1 commit to main • 90f3356…6918e8f • 
15 days ago

Update version dependencies for opam packages

bacampushed 1 commit to main • c458262…90f3356 • 
16 days ago

Version bump

bacampushed 2 commits to main • 4bcec15…c458262 • 
16 days ago

Add dec_bits functions

bacampushed 1 commit to main • bf4178d…4bcec15 • 
29 days ago

Add placeholders for translation information

bacampushed 1 commit to main • 0bc5a5d…bf4178d • 
on Feb 3

Compatibility with recent stdpp

bacampushed 1 commit to main • 76bfa29…0bc5a5d • 
on Jan 27

Tidy up imports

bacampushed 2 commits to main • 833aafb…76bfa29 • 
on Jan 27

Fix build for Coq 8.20

Pull request merge
bacampushed 1 commit to main • 7f1f5b2…833aafb • 
on Jan 27

Add count_trailing_zeros operation

bacampushed 25 commits to main • 562597f…7f1f5b2 • 
on Jan 17

Add count_trailing_zeros operation

bacampushed 2 commits to newregstate • 01ccfbb…7f1f5b2 • 
on Jan 17

More idiomatic eqb for stdpp

bacampushed 7 commits to newregstate • 197fc93…01ccfbb • 
on Dec 9, 2024

Add explicit system register access operations and id type

bacampushed 1 commit to newregstate • 0b11c2c…197fc93 • 
on Oct 4, 2024

A more direct treatment of bitvector sizes and indices

bacampushed 2 commits to newregstate • 9bd1f04…0b11c2c • 
on Sep 24, 2024

Remove legacy dependency annotations from the interface

tperamipushed 1 commit to newregstate • 94a2891…9bd1f04 • 
on Sep 18, 2024

Minor interface updates

bacampushed 1 commit to newregstate • e9a9c1b…94a2891 • 
on Sep 13, 2024

We should have pa_eq and pa_countable now

bacampushed 1 commit to newregstate • fdf41bb…e9a9c1b • 
on Aug 27, 2024

Add EqDecision instances for other types in the concurrency interface

bacampushed 1 commit to newregstate • be97a73…fdf41bb • 
on Aug 26, 2024

Add instances for built-in concurrency interface types

bacampushed 1 commit to newregstate • 78688d6…be97a73 • 
on Aug 20, 2024

Start updating concurrency interface Arch module

bacampushed 1 commit to newregstate • 094c6b0…78688d6 • 
on Aug 14, 2024

Add support for printing effects

bacampushed 1 commit to newregstate • 50b92c9…094c6b0 • 
on Aug 9, 2024

Use more scalable proof for record decidable equality

bacampushed 2 commits to newregstate • e9ee50e…50b92c9 • 
on Jul 31, 2024

Make BBV version of Inhabited use same implicits in constructor as stdpp

Force push
bacamforce pushed to newregstate • 7682831…e9ee50e • 
on Jul 29, 2024

Tighten hex bits parsing to match tests

bacampushed 2 commits to main • 04b6b8f…562597f • 
on Jul 24, 2024

Change vec_init to vector_init to match new Sail library declaration

bacampushed 1 commit to main • 64f5d7e…04b6b8f • 
on Jul 2, 2024

Use stdpp's Inhabited when targeting it

bacampushed 2 commits to main • 0aba030…64f5d7e • 
on Jul 2, 2024

Eta-expand the integer in get_slice_int to stop eager tactics

bacampushed 2 commits to main • 8036042…0aba030 • 
on Jun 27, 2024

Remove obsolete constraint solving tactics

bacampushed 2 commits to main • 160c673…8036042 • 
on Jun 27, 2024

Eta-expand the integer in get_slice_int to stop eager tactics

Force push
bacamforce pushed to newregstate • 97fd27d…7682831 • 
on Jun 23, 2024

Tweak type checking of Mem_write_request constructor

bacampushed 1 commit to main • 5150697…160c673 • 
on Jun 19, 2024