bedrock2
bedrock2 copied to clipboard
mit-plv
A work-in-progress language and compiler for verified low-level programming
Bumps [deps/coqutil](https://github.com/mit-plv/coqutil) from `5d391eb` to `21b0ec1`. Commits 21b0ec1 map.of_olist_Z f6430e0 fix a[i] list indexing notation 2a3970b more ZList lemmas 41494bc relax preconditions of len_from/len_upto See full diff in compare view...
![dependabot[bot] avatar](https://avatars.githubusercontent.com/in/29110?v=4 "dependabot[bot] avatar"){kind=avatar}
This PR adds support for metrics in the `RegAlloc` and `Spilling` passes. - [ ] Fix the cost for `SInteract` in FlatImp - [ ] Update bedrock2 source semantics to...
The Coq team released Coq `8.16+rc1` on June 01, 2022. The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**. It can be delayed in case of...
so I've been asked for this several times now. Here are some thoughts of what we should do. ## References to non-bedrock2-specific background resources - basic coq usage, like one...
creating a PR, hoping that it will let me comment on several commits at a time...
@Carotti this is what I had in mind with my last comment in the metrics PR. Does this make send and seem acceptable to you? (this is not done yet)
Do we still have a verified interpreter for the pure subset of bedrock2? It would be neat to run it side-by-side with ToCString on a comprehensive set of programs. I'm...
As discussed with @vmurali and @sifive-emarzion, it would be nice to eventually split this repository in a way that allows for the sifive end-to-end repository to include bedrock2 (and probably...