rely/guarantee for external library functions

[l-kent]

Allows procedure-level rely/guarantee to be specified for external library functions.

I think this does what it's supposed to but the proof for the example doesn't go through yet, I'm not quite sure what needs to be done there.

[ailrst]

This will also need a transitivity check on $R_c \vee G_f$ at some point, as well as that $G_f \implies G_c$.

It would also be nice to encode the procedure R/G s as functions rather than repeating them in the calls.

I also can't figure out why this example doesn't verify but that might have to wait until next year.

[l-kent]

Yeah, I forgot about G_f ==> G_c. I did remember the transitivity check but haven't gotten to it yet. Neither is difficult so I will add them today.

I agree that it would probably be nice to encode the procedure rely/guarantees as functions, but this was just the fastest way to implement it since there was a desire to have this functionality ASAP.

[ailrst]

If its possible it might be simpler to prove the side-condition by contradiction without explicitly constructing a throw-away state in variables.

ie with the relys and guarantees (Rc, Gc, Rf, Gf) as just predicates referring to the current state directly

procedure RcORGf ();
  ensures Rc || Gf

proccure NOTRcIMPLIESRf ();
  ensures (Rc && !Rf)

Then the rely check is an inline if block

... P ... 
if (*) {
  call RcORGf();        // assume Rc \/ Gf
                        // new state after Rc \/ gf step
  call NOTRcIMPLIESRf;  // assume ! (Rc ==> Rf)
  assert false;
}
... P ... 
call ...
... Q ...

I think this assert false is proving the predicate we want, and means that the state gets 'thrown away' because the if's fall-through is unreachable.

[l-kent]

it crashes when no spec is supplied

I think I've fixed this now.

doesnt seem to automatically add the mem$inv2.

Can you give an example of this?

If its possible it might be simpler to prove the side-condition by contradiction without explicitly constructing a throw-away state in variables.

I don't think this is really meaningfully simpler. I think it probably works but I'm really not inclined to think through it all again and there isn't any reason to change.

[ailrst]

doesnt seem to automatically add the mem$inv2.

Can you give an example of this?

It was due to a local modification of mine where it didn't refer to inv2 in the final assertion, don't worry about it.

I don't think this is really meaningfully simpler. I think it probably works but I'm really not inclined to think through it all again and there isn't any reason to change.

No worries, the reason I want it is to be able to refer to other auxiliary variables in the invariant (without explicitly pulling them into the$inv procedures), but I'll talk to Kirsten and Graeme about it next week and implement it in a separate PR if its useful.

[l-kent]

I've finally committed the transitivity check for Inv and the G_f ==> G_c check, though they don't verify with the current example and that may well be due to an error on my part. Do we need a reflexivity check for Inv too?

[ailrst]

Do we need a reflexivity check for Inv too? From the paper; reflexivity of inv follows from the reflexivity of Rf and Rc. So we just need a reflexivity check for Rf.

I've updated the example but its a bit less interesting now.

I also triggered the error I mentioned before, the Gamma_/mem$inv2 don't get declared if it they are not mentioned in the procedure's Rely.

[l-kent]

Can you just give a version of the spec file that causes that problem?

[ailrst]

Globals:
x: int
z: int

L: z -> true, x -> (z mod 2bv32 == 0bv32)
// env doesn't reduce security level of x
// env doesn't change the security classification of x
Rely: old(Gamma_x) ==> Gamma_x, z == old(z)
Guarantee: z >= old(z)

Subroutine: main
Requires: Gamma_x == true
Requires: Gamma_z == true
Requires: z == 0bv32

Subroutine: secret
Requires: z mod 2bv32 == 1bv32
Ensures: !Gamma_x && (z mod 2bv32 == 1bv32)
// env doesn't change security classification or level of x
Rely: z mod 2bv32 == 1bv32, z == old(z)
// we don't change the security classification of x
Guarantee: z == old(z)

// Rely: !Gamma_x && (z == old(z)) && (old(Gamma_x) == Gamma_x)
// Guarantee:  !Gamma_x, (old(Gamma_x) == Gamma_x), z == old(z)

// Gf ==> Gc
// transitive Rc \/ Gf 

[l-kent]

Fixed that, will merge it now