mit-plv / bedrock2 Goto Github PK

View Code? Open in Web Editor NEW

283.0 283.0 55.0 8.39 MB

A work-in-progress language and compiler for verified low-level programming

Home Page: http://adam.chlipala.net/papers/LightbulbPLDI21/

License: MIT License

Makefile 0.83% Shell 0.30% Coq 94.24% Verilog 3.80% Python 0.56% Emacs Lisp 0.12% C 0.15% Vim Snippet 0.01%

bedrock2's People

Contributors

Stargazers

Watchers

bedrock2's Issues

ecancel_assumption triggers unification

We make quite some effort to prevent the separation logic tactics from running unification, but here's an example where it still does run unification, as the slowness shows:

Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Open Scope Z_scope.

Definition mul1(a b: Z): Z :=
  List.fold_left Z.add
                 (List.concat (List.repeat (List.repeat 1 (Z.to_nat a)) (Z.to_nat b)))
                 0.

Goal mul1 200 100 = mul1 100 200. Time reflexivity. Qed.

Goal mul1 100 200 = mul1 200 101. Time Fail reflexivity. Abort.

Require Import coqutil.sanity coqutil.Map.Interface.
Require Import bedrock2.Map.Separation.
Require Import bedrock2.Map.SeparationLogic.

Section Test.
  Context {value} {map : map.map Z value} {ok : map.ok map}.

  Goal forall v R m, sep (ptsto (mul1 100 200) v) R m -> sep R (ptsto (mul1 201 100) v) m.
    intros.
    Time Fail ecancel_assumption.
(* The command has indeed failed with message:
         No matching clauses for match.
   Finished transaction in 22.093 secs (21.88u,0.012s) (successful)
*)
  Abort.

  Goal forall v R m, sep (ptsto (mul1 100 200) v) R m -> sep R (ptsto (mul1 200 100) v) m.
    intros.
    Time ecancel_assumption.
(* Finished transaction in 5.429 secs (5.378u,0.s) (successful) *)
  Qed.
End Test.

remove wsplit, make word non-indexed

I would like to make word not have operations that use a different width on output than on input when I factor out the library. After all, the name already clues a fixed size. Currently flat->riscv compilation uses wsplit, for the riddiculous preparation of constants. let's get rid of it? do you think we are better of if you do it or will I likely get it just fine as well?

feature requests from kernel programmers

better syntax for struct access
type-based pointer arithmetic
easy declaration of external functions, with support for including relevant header files during printing of C code
story for statically allocated (/external) variables / linker symbols
debugger plugin for printing bedrock structs?

not really big issue:

lack of break, continue, return (as long as require exists)
purely syntactic differences

Why was the decision made to not support function pointers?

Is there documentation on these sorts of design decisions?

feature request: hex constants

from bbv or coq master?

consider git.sr.ht + builds.sr.ht instead of github+travis

builds.sr.ht has provides operating systems from this century, beefier runners, even beefier runners on request, and currently much better queuing times (e.g. I regularly have a sr.ht build finish before a travis builds starts). Amongst other things, this would enable us to use coq built by the coq devs instead of @JasonGross.

we would probably want to keep a copy of the source code on github as well because that is considered neutral ground at many companies when deciding what their employees can contribute to. another consideration is that sr.ht is is planned to be a paid-for service, although it is currently "alpha" (read: much more stable than travis) and thus pay-what-you-want for now. The fees are negligible when compared to plv budget or Jason travis support dev time, though.

it is also possible to use builds.sr.ht with github but doing so requires giving it full access to a github account https://todo.sr.ht/~sircmpwn/dispatch.sr.ht/22#comment-1112

Define a semantics in the bedrock2 directory

Right now, the bedrock2 directory contains the syntax, but the Semantics.v file doesn't contain an actual semantics (just some auxiliary definitions). As a first guess, I would assume that ExprImp needs to be moved to the bedrock2 directory, though it seems to have a lot of dependencies, so it should probably be split up.

@samuelgruetter Thoughts on this?

Split Machine-specific and language-specific parameters

The parameters types seem to be quite monolithic and might benefit from some separation. Some comments below:

Class parameters := {
  varname : Set; (* language choice *)
  funname : Set; (* language choice *)
  actname : Set; (* machine specific *)
  bopname : Set; (* machine specific *)
}.

Class parameters := {
  syntax :> Syntax.parameters;

  (* begin machine specific *)
  word : Set;
  word_zero : word;
  word_succ : word -> word;
  word_test : word -> bool;
  word_of_Z : BinNums.Z -> option word;
  interp_binop : bopname -> word -> word -> word;

  byte : Type;
  (* nat included for conceptual completeness, only middle-endian would use it *)
  combine : nat -> byte -> word -> word;
  split : nat -> word -> byte * word;

  mem :> map word byte; (* it isn't clear that there is any benefit from including this *)
  (* end machine specific *)

  locals :> map varname word; (* it isn't clear that there is any benefit from including this *)

  funname_eqb : funname -> funname -> bool (* language choice *)
}.

My proposal is to separate the machine model (fields marked "machine specific") from the language choices. This allows for some flexibility, mainly that compiler passes and program writers choose any variable representation they want without needing to state explicitly that they don't change the machine semantics.

@samuelgruetter I can probably make a PR for this, this issue is mostly to get your thoughts so I don't do work that you don't want to merge.

a "getting started" guide

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 or two chapters of software foundations or frap. no induction or datatypes stuff, just proof.
Hoare logic (software foundations? frap? VST?)
Separation Logic (* and emp, no fancy things like magic wand).
- https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Map/Separation.v is actually short
separation logic automation. perhaps read the first bedrock paper, and ignore the higher order stuff about code pointers http://adam.chlipala.net/papers/BedrockPLDI11/BedrockPLDI11.pdf chapter 2. SeparationLogic.ecancel is the bedrock2 script to perform cancellation.
coq tactic lia, ring documentation
reading coq type errors (reification by parametricity repo might have a thing on this?)

Common infrastructure in bedrock2 (just skim)

bedrock2 semantics (read enough to understand structure)

https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Notations.v
https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/WeakestPrecondition.v expr_body, its callees, and cmd_body
first example proof: https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Examples/swap.v
- in particular, try to match up the spec_of_* definitions with WeakestPrecondition.call and try to think through in your head what the precondition ends up being
- follow along with the bedrock paper, single-step straightline instead of using repeat
loop invariant example https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Examples/ipow.v#L74 (the arithmetic proof after the refine statement is not bedrock2-specific)
how to mention memory in loop invariants: https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Examples/bsearch.v#L89

Things that we don't really know how to teach

how to actually prove interesting things about your program. this requires a clear plan and direction, and good understanding of coq to evaluate different choices of stating "the same" thing
how to understand very generic dependently typed lemmas like `tailrec, copy-pasting their usages is hopefully fine though

make is very noisy, even when there's nothing to be done

See also mit-plv/coqutil#15; it's the same problem in the submakefiles here

Please bump submodules

Since mit-plv/coqutil#2 and mit-plv/riscv-coq#6 have been merged. This will help with the build on Windows.

feature request: make clean (that'd be safer than git clean -dxf)

feature request: make up to specific .vo

variable scoping and program logic

I think the following program would be problematic because for the same loop invariant there are two different sets of defined variables during runtime:

n=2
while (n<2) {{ n++; x = n }}
return x

In particular, the loop invariant couldn't state that x is defined. Obviously, this is easily fixed:

n=2
x=0
while (n<2) {{ n++; x = n }}
return x

except for this issue, the first program is also well-defined and otherwise supported.

if we want to keep giving an exact list of defined and live variables for all iterations of a loop in the program logic, we should rule out the first program and allow the second. I guess we could state it as a scoping restriction: a variable that is read after the loop must be initialized before the loop.
OTOH, the same thing with an if would work fine right now:

n=2
if (y) {{ x = 1 }} else {{ x = 2 }}
return x

but this works only because the program logic does pathblasting, i.e. treats the previous program equivalently to

n=2
if (y) {{ x = 1; return x }} else {{ x = 2; return x }}

or we could just initialize live but uninitialized variables to 0 -- that would resolve these conceptual issues, at the cost of extra machinery. Now when I am thinking about it, we could even sidestep proving correctness of the liveness analysis used for this purpose if we used its output in for both program verification and compilation.

EDIT: I guess there is also the option of initializing variables to an undefined value. would work for program logic, and would avoid initialization overhead in cases where liveness analysis is imprecise (e.g. the example above). and for deterministic execution we could still consider that an error.

Bump submodules

Once mit-plv/riscv-coq#22 is merged, please bump the submodules for coqutil and riscv-coq to the latest versions. Once this is done, I can make bedrock2 use COQPATH for its dependencies, and then we can work on making bedrock2 itself a non-insane dependency.

feature request: linking readonly data

I want to write code that accesses readonly data, and have that linked into my bedrock2 binary.

Travis should test this on CI

The pre-req for getting this added to Coq's CI is to have this repo run continuous integration. Please add a .travis.yml to test this against master and 8.8 (and any other branches you care about). If you do that, I can add this to Coq's CI, and the bench.

liveness analysis

As discussed for program logic simplicity we want the source code to be supplemented with "kill" statements marking when a variable becomes dead. we would need to prove that transformation correct.

To prove this transformation correct, we would need to prove correct the underlying liveness analysis. idk if we actually want to do this (perhaps we should change the program logic instead), but if we do, the same analysis could be used to zero-initialize uninitialized variables in the compiler.

standardize mmio compiler instantiation

We have multiple copies of it, and some of the bugs I am fixing are familiar...

Lagging riscv-coq version

Please bump riscv-coq to latest commit. Is there a general plan for timely propagation of updates?

splitting the repository

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 the compiler) but not mit mit-plv/kami.

should types be record members or record parameters?

Currently, the record defining maps takes the type of the map as a parameter but NameWithEq has name as a field. Is there a good reason for this difference?

Translating everything directly from ocaml-style module signatures would leave types as record members, so I would think map could be changed. On addition on top of that that I have seen in the Coq world is to use separate records for the proof and non-proof parts of a module to enable more parallel compilation -- so map lemmas could be in a separate record from map types and functions. But Decidable eh-intentionally breaks that pattern.

Previous discussion: mit-plv/fiat-crypto#233

ensure and test that return values are assigned left to right

we do want them left-to-right, right?

kami needs bbv, add bbv submodule?

Bedrock2 notation breaks record notation

After importing Bedrock2 notations, you can no longer write records. The issue seems to be related to the overloading of ;.

seq associativity

to minimize proof obligation rolling postcondition size in WP, all seq should be normalized to the same associativity as cons. This mirrors the style where stmt and list stmt are mutually inductive.

RFC: input and output

So it seems that returning from C to assembly for each i/o operation is actually prohibitive, so I am contemplating ways of adding minimal input and output functionality to bedrock, in a modular way so that the special case of pure code is still nice. The current idea is as follows:

Add a new language parameter for codes for input and output actions, io. Instantiating io := Empty_set allows to precommit to pure code, different instantiations can be chosen for different setsof input-output functionality / system calls.
Add a syntax tree node SIO (binds : list var) (_ : io) (args : list expr) to ExprImp and intermediate languages. If io is not inhabited, this constructor is unusable. Syntactically, this is intentionally similar to function calls (e.g. extern in C, as opposed to *(volatile*)x = y).
Output semantics are quite simple: add language parameters event : io -> Type and output : forall op:iop, list wXLEN -> memstate -> event op. If the code only produced output and took no input, it could be given semantics using a trace of output events. The list of words is populated with the arguments passed from the program, and io functions like send(pointer, length) would also look at some part of the memory.
I think the best way to handle input is to parametrize over a monad very similar to that in the riscv semantics. This can then be instantiated with a deterministic model of the outside world for concrete execution or a completely nondeterministic model for conservative reasoning. In practice, programs would be proven in a context paramerized over a monad along with some properties of it. eval_stmt would probably return option (m (varstate * memstate)).
The lowest-level compiler would take an "io compiler" and its correctness proof as an argument and call it when compiling SIO, perhaps passing registers holding the inputs as arguments. For extern functions that perform io, this would just be the function call compiler. For the example of memory-mapped GPIO ports, the lemma to prove would be that the cpu-architecture-level trace of gpio events would correspond to the calls to gpio_toggle(i) and v = gpio_read(i). A more interesting example could perhaps be constructed from the memory-mapped graphics api in the hardware semantics repo but I have not investigated.

@samuelgruetter can you tell me whether you see anything obviously wrong with this, and if you can tell, what the correctness condition for "io compiler" might look like? If you don't see any red flags, I'll probably go ahead and prototype this to see how reasonable it looks and whether it might make sense to merge the result to this repo.

continuous integration

Spinned off from coq/coq#7878

It would be great if bedrock2 could be built as a part of the Coq continutous integration system so that coq changes do not break it. Secondarily, it would also be nice to have a computer nanny us to make sure we don't break the build ourselves. I think there are three blockers for this:

Continually ensure that bedrock2 builds with the latest coq release and with coq master.
Support EXPECTED_COQC_VERSION=any so coq devs can bump their version numbers without breaking their CI
Write a script that downloads and compiles or dependencies (or offload this to git submodules and makefile).
Set up travis on our own
Tell coq devs that bedrock2 is good to go for CI

@samuelgruetter is this a direction where you would like to see bedrock2 go? If so, would you like to do some of the above steps yourself, or give me guidance on how to do them in a way that does not conflict with your plans?

the build output contains a lot of noise

let's try to reduce it as we refactor files?

duplication of Instance definitions after removal of primitive projections

@samuelgruetter do you have any understanding why lines such as the following are necessary?

https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Examples/bsearch.v#L86

make clean does not clean dependency information

after updating today I got

2 kevix@ashryn ~/mit-plv/bedrock2 (git)-[master] % env EXPECTED_COQC_VERSION=8.8.0 make -j4 :(
make: *** No rule to make target '../riscv-coq/src/RiscvBitWidths.vo', needed by 'src/ExprImp.vo'. Stop.

samuelgruetter/riscv-coq@01f3196 seems to have moved that file.

then I ran make clean and got the same thing again

then I ran git clean -dxf and make and then everything worked

feature request: use immediate operands when compiling binops

proliferation of Local in files with program logic proofs

We should probably make a file that we can Load to set up the correct parsing/elaboration environment for source code, specs, and program logic proofs.

test 8.9beta in travis

build bedrock2 semantics separately from the compiler

We should make sure tools/code for the bedrock2 language is easy to use, and given the current build time of riscv-semantics, it would probably be a good idea to support requiring bedrock2 semantics without the compiler. Two options would be splitting the repository more and adding a separate makefile target, there probably are more.

load8 can be implemented on 32-bit instead of loadWord

on 32-bit it can be implemented as load4, as that's what truncating a load8 would look like. store8(x) would be store4(x) and store4(0), still not too bad.

consolidate and factor out map library

a proper fix for reduce_locals_map would require nontrivial Ltac development that would depend on the exact shape of map definitions, and I don't want to do this before we have some tentatively acceptable definitions to go on with.

all files should Global Unset Refine Instance Mode

to get saner behavior on incomplete typeclass instances

also see https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/GlobalSettings.v and https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/FixCoqMistakes.v

@samuelgruetter @stellamplau

state_calc should fail if it doesnt find key_eq_dec

Boolean equality on bytes is incorrect

bedrock2/bedrock2/src/Byte.v

Lines 32 to 36 in 99e4aeb

 Definition eqb (a b : byte) : bool := 

 let '(a7, (a6, (a5, (a4, (a3, (a2, (a1, a0))))))) := to_bits a in 

 let '(b7, (b6, (b5, (b4, (b3, (b2, (b1, b0))))))) := to_bits b in 

 eqb a0 b1 && eqb a1 b1 && eqb a2 b2 && eqb a3 b3 && 

 eqb a4 b4 && eqb a5 b5 && eqb a6 b6 && eqb a7 b7.

eqb a0 b1 should be eqb a0 b0

RFC: object-language structs

one Inductive for the fields of each record, with the constructors representing field names
each field name is interpreted as an offset into the struct
all fields are disjoint by construction
ABI-compatible with gcc/llvm __attribute__ ((__packed__)). this is probably trivially true right now but would be important if new types are added
notations TBD, C-style

allow weakening of locals map in program logic

before entering an if or a while, the locals map should be weakened to only include variables inside that block. Further, variables used (syntactically) read-only in that block would ideally be lifted and omitted from the postcondition. This would hopefully make it feasible to write pre- and postconditions for ifs instead of pathblasting. just weakening should be rather simple, having a separate read-only variables map would be effort and maybe more than it is worth.

warnings policy?

The current build generates a lot of warnings, including deprecation warnings (e.g. here. We probably want to fix some of them. Opinions?

bedrock2 is incompatible with numeral notations

I am preparing a PR to fix the code in bedrock2 itself, but please merge mit-plv/bbv#20 and mit-plv/riscv-coq#2 asap and update the submodules in bedrock2.

word library specification

defining operations: to_Z of_Z
fully specified: == + - * s* s*s << >> s>> & | xor < s<s
fully specified as redundant:> >=
Maybe later: partially specified: / s/ s/s

record for language parameters

I think it would be an improvement to have ExprImp and FlatImp parametrized over something of a type like the following:

Record LanguageParameters :=
{ 
  Bw: RiscvBitWidths;
  Name: NameWithEq;
  var := name Name;
  FName : NameWithEq.
  func := (@name FName);
  state: Type;
  stateMap: Map state var (word wXLEN);
}.

Othwerwise typeclass resultion picks up some arbitrary instantiation of this unless care is taken to do otherwise, making stating general theorems rather difficult.

program logic proofs are slow in PG, patch it

ProofGeneral/PG#415

debugging typeclass resolution in semantics

As a part of an experiment I tried modeling continuations with explicit stacks. In ExprImp.v after defining stmt, the following code

  Inductive cont: Set :=
    | CLoad(x: var)(addr: expr): cont
    | CStore(addr val: expr): cont
    | CSet(x: var)(e: expr): cont
    | CIf(cond: expr)(bThen bElse: cont): cont
    | CWhile(cond: expr)(body: cont): cont
    | CSeq(s1 s2: cont): cont
    | CSkip: cont
    | CCall(binds: list var)(f: func)(args: list expr)
    | CStack(st: state)(c: cont)(binds rets: list var).

  Section WithEnv.
    Context {env} {funcMap: Map env func (list var * list var * stmt)} (e:env).
    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont): option (state * mem) :=
      match f with
      | 0 => None (* out of fuel *)
      | S f => match s with
        | CLoad x a =>
            a <- eval_expr st a;
            v <- read_mem a m;
            Return (put st x v, m)
        | CStore a v =>
            a <- eval_expr st a;
            v <- eval_expr st v;
            m <- write_mem a v m;
            Return (st, m)
        | CSet x e =>
            v <- eval_expr st e;
            Return (put st x v, m)
        | CIf cond bThen bElse =>
            v <- eval_expr st cond;
            eval_cont f st m (if weq v $0 then bElse else bThen)
        | CWhile cond body =>
            v <- eval_expr st cond;
            if weq v $0 then Return (st, m) else
              p <- eval_cont f st m body;
              let '(st, m) := p in
              eval_cont f st m (CWhile cond body)
        | CSeq s1 s2 =>
            p <- eval_cont f st m s1;
            let '(st, m) := p in
            eval_cont f st m s2
        | CSkip => Return (st, m)
        | CCall binds fname args =>
          fimpl <- get e fname;
          let '(params, rets, fbody) := fimpl in
          argvs <- option_all (map (eval_expr st) args);
          st0 <- putmany params argvs empty;
          st1m' <- eval_cont f st0 m fbody;
          let '(st1, m') := st1m' in
          retvs <- option_all (map (get st1) rets);
          st' <- putmany binds retvs st;
          Return (st', m')
        | CStack stf cf binds rets =>
          stf'm' <- eval_cont f stf m cf;
          let '(stf', m') := stf'm' in
          retvs <- option_all (map (get stf') rets);
          st' <- putmany binds retvs st;
          Some (st', m')
        end
      end.

fails to check with an error

Error: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X170==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args
          |- Map
               ?X167@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args}
               ?X168@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args}
               ?X169@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args}] (parameter Map of
          @get) {?Map}
 ?X185==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets
          |- Monad
               ?X184@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets}] (parameter Monad of
          @Bind) {?Monad}
 ?X193==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs
          |- Monad
               ?X192@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}]
          (parameter Monad of @Bind) {?Monad0}
 ?X199==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs
          |- Map
               ?X196@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X197@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X198@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}]
          (parameter TMap of @putmany) {?TMap}
 ?X200==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args {fimpl} {p} {fbody} {params} {rets}
          {argvs} |- Type] (parameter K of @putmany) {?K}
 ?X203==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs |- Type]
          (parameter K of @empty) {?K0}
 ?X204==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs |- Type]
          (parameter V of @empty) {?V}
 ?X205==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs
          |- Map
               ?X202@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X203@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}
               ?X204@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs}]
          (parameter Map of @empty) {?Map0}
 ?X208==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0
          |- Monad
               ?X207@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0}]
          (parameter Monad of @Bind) {?Monad1}
 ?X221==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m'
          |- Monad
               ?X220@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}] (parameter Monad of @Bind) {?Monad2}
 ?X230==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m'
          |- Map
               ?X227@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}
               ?X228@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}
               ?X229@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'}] (parameter Map of @get) {?Map1}
 ?X232==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args {fimpl} {p} {fbody} {params} {rets}
          {argvs} {st0} {st1m'} {st1} {m'} |- Type] (parameter A of map) {?A}
 ?X235==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' retvs
          |- Monad
               ?X234@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}]
          (parameter Monad of @Bind) {?Monad3}
 ?X241==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' retvs
          |- Map
               ?X238@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}
               ?X239@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}
               ?X240@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs}] (parameter TMap
          of @putmany) {?TMap0}
 ?X242==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' {retvs} |- Type] (parameter V of @putmany) {?V0}
 ?X245==[Bw Name FName state stateMap vars varset env funcMap e eval_cont f0
          st m s f binds fname args fimpl p fbody params rets argvs st0 st1m'
          st1 m' retvs st'
          |- Monad
               ?X244@{__:=Bw; __:=Name; __:=FName; __:=state; __:=stateMap;
                      __:=vars; __:=varset; __:=env; __:=funcMap; __:=e;
                      __:=eval_cont; __:=f0; __:=st; __:=m; __:=s; __:=f;
                      __:=binds; __:=fname; __:=args; __:=fimpl; __:=p;
                      __:=fbody; __:=params; __:=rets; __:=argvs; __:=st0;
                      __:=st1m'; __:=st1; __:=m'; __:=retvs; __:=st'}]
          (parameter Monad of @Return) {?Monad4}

even if I replace the new case with _, I get a typelcass resolution error instead of a failed to infer something of type which I normally use to debug mistyped code. There is probably just a typo or something equally stupid in this code, but the typeclass magic puts debugging it beyond my ability -- please help.

bedrock2.Syntax.parameters needs a better name

liveness analysis draft

I did not manage to make sense of the liveness analysis stuff in regalloc so I wrote my own. Let's discuss whether we could arrive on a version that both of us understand and like. Note that the application I have in mind is minimizing locals context size in program logic proofs.

in exprimp after allVars_expr:

Axiom remove : var -> list var -> list var.
  Definition removes pos neg := List.fold_right remove pos neg.
  Local Infix "--" := removes (at level 60).
  Axiom unsets : list var -> cmd.
  Axiom seq : cmd -> cmd -> cmd.
  Fixpoint live (c : cmd) (usedlater : list var) : cmd * list var :=
    match c with
    | cmd.store _ a e =>
      let usednow := allVars_expr a ++ allVars_expr e in
      (seq c (unsets (usednow -- usedlater)), usednow ++ usedlater)
    | cmd.set x e =>
      let usednow := allVars_expr e in
      (seq c (unsets (usednow -- usedlater)), usednow ++ remove x usedlater)
    | cmd.unset x => (c, remove x usedlater)
    | cmd.cond e c1 c2 =>
      let ue := allVars_expr e in
      let (c1', l1) := live c1 usedlater in
      let (c2', l2) := live c2 usedlater in
      (cmd.cond e (seq (unsets (ue--l1)) c1') (seq (unsets (ue--l2)) c2'),
       ue++l1++l2)
    | cmd.while e c =>
      let ue := allVars_expr e in
      (* fixed point in 2 iterations? EXPONENTIAL TIME. Could we do in 1?*)
      let (c', lc) := live c usedlater in
      let (c', lc) := live c (lc++usedlater) in
      (seq (cmd.while e (seq c' (unsets (ue--lc)))) (unsets ((ue++lc)--usedlater)),
       ue ++ lc ++ usedlater)
    | cmd.seq c1 c2 =>
      let (c2', l) := live c2 usedlater in
      let (c1', l) := live c1 l in
      (cmd.seq c1' c2', l)
    | cmd.skip => (c, usedlater)
    | cmd.call binds _ args | cmd.interact binds _ args =>
      let uargs := List.fold_right (@List.app _) nil (List.map allVars_expr args) in
      (seq c (unsets (uargs -- usedlater))
      , uargs ++ (usedlater -- binds))
    end.

	Definition eqb (a b : byte) : bool :=
	let '(a7, (a6, (a5, (a4, (a3, (a2, (a1, a0))))))) := to_bits a in
	let '(b7, (b6, (b5, (b4, (b3, (b2, (b1, b0))))))) := to_bits b in
	eqb a0 b1 && eqb a1 b1 && eqb a2 b2 && eqb a3 b3 &&
	eqb a4 b4 && eqb a5 b5 && eqb a6 b6 && eqb a7 b7.