Provide limited visibility into the Crucible state while inside a CrucibleSetup ()

[weaversa]

I often find myself writing two functions to describe each struct or set of conditions, i.e. one to be used in the pre-state and one to be used in the post-state. If it were possible to know whether we were in a pre or post state (via some flag --- Are we above the crucible_execute_func line, or below it?) I would only have to write one function for each and test on this flag.

Here is an example. The notable differences here are crucible_precond vs. crucible_postcond and the bitvector_t_setup function taking slightly different arguments.

let bitvector_t_struct (rw : Term) (n : Int) (name : String) = do {
  bv <- bitvector_t_setup rw n name;
  let bvt = bv.t;
  precond {{ bvt.bits.nLength_max >= bvt.bits.nLength }};
  return {s=bv.s, bucket=bv.t};
};

let bitvector_t_struct' (n : Int) (name : String) = do {
  bv <- bitvector_t_setup CONST n name;
  let bvt = bv.t;
  postcond {{ bvt.bits.nLength_max >= bvt.bits.nLength }};
  return {s=bv.s, bucket=bv.t};
};

[weaversa]

Of course, if I got this capability I’d immediately write:

let assert = if (eval_bool {{ `in_crucible_prestate == True }}) then crucible_precond else crucible_postcond;

So, what is the reason for separating the pre and post conditions into different functions? Crucible already knows whether a condition is happening in the pre or post state. If I write a condition before crucible_execute_func it’s a precondition, etc. Why not just have one function instead of 2?

[atomb]

Complex operations like this, and some of the things you recently committed to the saw-demos repo, are likely to be much easier using the RPC API to SAW, and the Python client, since you'll have a fully-featured programming language available, and because contracts in that interface are purely data structures.

We actually had a single assert function for a little while, and had comments from users that it was confusing, and that they understood pre- and postconditions better, so we adopted the two-function approach. They do, indeed, do exactly the same thing in the implementation. One approach that could potentially be viable would be to provide three functions: one that works in either state, and the two current ones that check their state and produce an error if used in the wrong state.

[atomb]

It seems as though there's consensus that Python is the better way to go for verification scripts that need this sort of flexibility, and that this would be an awkward thing to implement in SAWScript, so I'm going to close this issue.

[pnwamk]

N.B., currently the __state field on a Contract reports what state things are in. We could make this more "publicly" visible, and/or add an assert that chooses "pre" or "post" condition as expected.