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 operate 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 can be found in the standard library by using Search.

Hint: Tactics used in validate

Here is the complete list of commands used in one possible solution:

Search, for example Search (_ + 0).
induction, for example induction x
simpl
simpl in, for example simpl in *
split
reflexivity
lia
congruence
injection
assumption
destruct, for example destruct (X =? Y)
apply, for example apply H
apply in, for example apply H1 in H2 or apply somelemma in H1
apply with, for example apply H1 with (x:=2)
apply in with, for example apply H1 with (x:=2) in H2
rewrite, for example rewrite H
rewrite in, for example rewrite H1 in H2 or rewrite somelemma in H1
;, for example simpl in *; congruence

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)).