Solver

The solver is the "most interesting" component of rif.

The solver has a custom internal state type. This is a record:

module S = Map.Make (String)

type state = {
  aliasing : string S.t;
  terms : Term.term S.t;
  predicates : Term.term S.t S.t;
}

In which aliasing is a map from spec variable names to term names, terms is a map from term names to the actual CVC5 terms, and predicates is a map from term name to predicate name to boolean value.

The idea is a Lifter.IR.instruction can be translated into a SolverState.state_function, which can be partially-evaluated into a simple transition function from state -> state, and similarly for both relies and guarantees. Once you can express all your state-transitions (relies & instructions) as simple state -> state functions, you can chain them together, like so:

let instruction_one = i1 |> SolverInst.translate tm |> SolverState.apply_inst tm solver sort in

(* imagine everything else is defined here *)
...
let s1 = rely initial_state in
let s2 = instruction_one s1 in
let s3 = rely s2 in
let s4 = instruction_two s3 in
let final_state = rely s4

Alternatively, thanks to ocaml's reverse-function-application operator |>, you can write this:

let final_state = initial_state |> rely |> instruction_one |> rely |> instruction_two |> rely

which is very nice and convenient.

Other state applications

Options

The state has different behaviour for specification and instructions. E.g. Getting None in an instruction is a failure, because the instruction is trying to find a term that the state doesn't have (which should be impossible). This made sense at the time but should be made more explicit.

However, getting None in a specification indicates that the solver should create a new arbitrary variable. This allows expressing stuff like "If the lock is locked, nothing happens, otherwise, X goes to some arbitrary unknown value".

It would be wise to not overload option types like this in the future.

Guarantees

Sometimes it's hard to express the requirements of a guarantee as a function (purely from a syntactic perspective - how do you express something like "X goes to some arbitrary value but is still locked"? It's much easier to just add the constraint that x is locked, without any other constraints on its value.). So we have the ability to not just do state transitions as functions, but also inject constraints over an existing state transition.

This is only really useful for guarantees, but we have the ability to partially-evaluate a set of "constraints" down to a function with type (state -> state) -> state -> state: it takes a state function and produces a state function, except it also injects constraints over the top. In practice this looks like this:

let guarantee_over : ((state -> state) -> state -> state) = SolverState.assert_over tm solver sort guarantee in

let final_state = initial_state |> rely |> guarantee_over instruction_one |> rely |> ...

and in this snippet of code, what we're expressing is that we transition states in the same way as above, but when we transition from s1 to s2, we also apply the constraints from the guarantee between these two states. The set of states produced by guarantee_over instruction_one is the set of states that satisfy both the behaviour of the guarantee and the behaviour of instruction_one.

Predicates

Note also that the state predicates are actually "evaluated" in ocaml code, not passed down to the solver. This limits the behaviour that we can account for (it gives up as soon as you get anything that isn't a straight assignment) but it is necessary to get around a behaviour in CVC5.

Effectively, if we tell CVC5 "There exists x and f such that f(x) is true", it treats this primarily as a constraint on x, not a constraint on f. So it thinks X is the special value for which F is true, not that f is the function that is true for x. Which means "f(x) is true for all x" doesn't actually make a function that's always true, it just constrains X in a totally meaningless way.

Essentially, if "f(x)" is true for all x, then "f(y) is not true for all y", because the assumption isn't that "f" is always true. This is a blessing and a curse; if f(y) was true for all y then we would collapse when generating states like, e.g. locked(x) && locked(y), because these two would be treated as totally contradictory constraints. However, it also limits how we can reason about updates to variables.

We get around this by implementing the predicates as a full lookup from term name to predicate name to boolean. So, whenever we execute code where e.g. str r0, [r1] (storing the value r0 into memory at r1), the code also does a corresponding replacement where every predicate for R0 overwrites every predicate for MR1. This way we don't actually inject any "secret(x) is true" assumptions into the model, because they don't work as you'd expect. The cost is just that we limit the behaviour we can handle a little bit, but in practice this doesn't seem to come up.

Constraints vs Asserts

The only really-core problem with the solver as it currently stands is that there's no ability to express "things that must be true always" without this modifying the actual problem. Because it's trying to create a state that meets the constraints, if you add the guarantees as constraints, CVC5 will succeed if it can create a state that suits the guarantees. This is different to requiring that all state suit the guarantees. CVC5 has assertions but they don't work in SyGuS mode.

It is probably possible to express the problem in just the right way that this doesn't matter. Something along the lines of how we need to show that for all out-of-order execution there exists a corresponding in-order execution. This may actually already be expressed correctly but I haven't thought too hard about it.