bedrock2
bedrock2 copied to clipboard
mit-plv
A work-in-progress language and compiler for verified low-level programming
We have many separation-logic predicates for what is essentially bytes in memory. Here is a probably incomplete list, based on what arguments they take: - sepclause\_of\_map(map.of_list_word_at bs addr): list, truncated...
It looks the semantics style has changed between bedrock1 and bedrock2. Is there an overview of which properties we can expect to continue to hold? Of course, one could read...
While working on [silveroak](https://github.com/project-oak/silveroak/pull/814/), I got an error where `straightline_call` says `Error: Cannot infer this placeholder of type "spec_of put_wait_get" (no type class instance found)`, and `Check (_ : spec_of...
I am trying to add the submodule dependencies of bedrock2 to coq's ci, however I am finding it really difficult to get bedrock2 to depend on already built versions of...
Compared to C, bedrock2 is missing quite a few operators: Unary operators: * ~~unary minus `-`~~ * logical not `!` * ~~bitwise not `~`~~ Binary operators: * unsigned division `/`...
Let's say I'm trying to prove termination for a loop that looks like this: ``` done = 0 while (!done) { status = MMIOREAD (status_register_addr) ; done = status &...
pending integration with the trace predicate library
I am currently attempting to use Bedrock2 for cryptographic applications that use field arithmetic generated by Fiat Crypto. I am however having a bit of trouble with the ecancel_assumption tactic....
Currently the opam package at https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-bedrock2/coq-bedrock2.dev/opam makes `bedrock_ex` which seems to be quite small (~4min on the bench) Could we have a more complete package for Coq's benchmark infrastructure?
In usage in fiat-crypto, I find myself needing to recreate some of the logic from https://github.com/mit-plv/bedrock2/blob/13365e8113131601a60dd6b6ffddc5a0b92aed58/bedrock2/src/bedrock2/ToCString.v#L149-L156 I would like a function like ```coq c_arrange_arguments {A R} (args : list A)...
