Systems and
Formalisms Lab

ProgramAnalysis hints

A few hints to help you if you get stuck on certain problems in lab 1.

Beware! Don't read further if you don't want spoilers!

Hint: Definition of validate

Our solution defines validate as a function of validate', and validate' takes an additional flag indicating whether the state on which `p will be run is nonzero.

Definition validate p := validate' p false.

Fixpoint validate' (p : Prog) (nz : bool) : bool.
Admitted.

In other words, if nz = true, then validate' can oeprate under the assumption that p will only be run with nonzero states. When calling validate' recursively, make sure to pass an nz that corresponds to the state after the current operation.

Hint: Arithmetic lemmas

Some lemmas about arithmetic on natural numbers are necessary to prove the soundness of this validator. Some of them can be proven inline using lia. The rest that we needed we found from the standard library by using Search.

Hint: Soundness of validate

To prove soundness of validate' from hint 1, it makes sense to do induction on the input program. The key to choosing the predicate P is to relate the nz indicator to the state of a program during a hypothetical execution of the program.

Hint: Soundness of validate (more details)

To prove soundness of validate' by induction on the program and develop a workable P, consider the two cases in executing validate' separately. Split the soundness of validate' into the case where the indicator passed into validate' is true and in the case where it is false.

Hint: Soundness of validate (spoiler)

To prove soundness of validate' by induction on the program, one workable P is

forall p,
  (validate' p true = true ->
   forall s, s <> 0 -> runPortable p s = (true, run p s)) /\
  (validate' p false = true ->
   forall s, runPortable p s = (true, run p s)).