Soundness of program transformation

Using Rocq
1

Hello!

Consider the following small (typed) language with conditionals :

Inductive const :=
| BOOL (b : bool)
| INT (n : nat).

Inductive exp :=
| CONST (c : const)
| IFV (e1 e2 e3 : exp)
| ADD (e1 e2 : exp).

Inductive ty :=
| TINT
| TBOOL.

The typing judgement is given by:

Inductive hastype : exp -> ty -> Prop :=
| T_BOOL : forall b, hastype (CONST b) TBOOL
| T_INT : forall n, hastype (CONST (INT n)) TINT
| T_IFV : forall e1 e2 e3 ty,
    hastype e1 TBOOL ->
    hastype e2 ty ->
    hastype e3 ty ->
    hastype (IFV e1 e2 e3) ty
| T_ADD : forall e1 e2,
    hastype e1 TINT ->
    hastype e2 TINT ->
    hastype (ADD e1 e2) TINT.

Now define a program transformation which consists in lifting the IFV nodes outside of nested expressions to the top level of the term. We define a type for the target of the transformation:

Inductive uexp :=
| UCONST (c : const)
| UADD (e1 e2 : uexp).

Inductive sexp :=
| SIFV (e1 : bool) (e2 e3 : sexp)
| SEXP (e : uexp).

(Note that in this type the condition of SIFV is always a literal boolean.)

The transformation itself is defined by:

Fixpoint bool_of_exp e :=
  match e with
  | UCONST (BOOL b) => Some b
  | _ => None
  end.

Definition dummy := SEXP (UCONST (INT 42)).

Fixpoint push (e : exp) (f : uexp -> sexp) : sexp :=
  match e with
  | CONST c => f (UCONST c)
  | IFV e1 e2 e3 =>
    push e1 (fun e1 => match bool_of_exp e1 with
                       | Some b => SIFV b (push e2 f) (push e3 f)
                       | None => dummy (* cannot happen if [e] is well typed *)
                       end)
  | ADD e1 e2 =>
    push e1 (fun e1 => push e2 (fun e2 => f (UADD e1 e2)))
  end.

Definition doit e := push e SEXP.

For example, doit rewrites (if true then 1 else 2) + 5 to if true then 1 + 5 else 2 + 5 (in obvious notation).

QUESTION: When reasoning about this function, I would like to deduce that the dummy branch is never taken if the input of the push is well-typed, but I do not see how to do it (or even how to write it in Coq). I can imagine two possible approaches:

  1. try to give a stronger signature to push so that it becomes “type-preserving”, but this would involve passing proofs of well-typedness around and I don’t know how to do that.

  2. make push return an option, with None used for the “badly-typed” case, but then I am afraid of all the extra book-keeping that will imply in every statement (and proof) involving it.

Does this look reasonable? Should I be looking along these lines or should I try a completely different approach?

Any suggestions or comments would be appreciated!

Cheers,
Nicolas

2

Your original approach looks somewhat reasonable to me. To make further progress I would advise to use a variant of your option 1: instead of refining the type of push, just prove a lemma stating what you want: if hastype e TBOOL then there exists a b : bool such that bool_of_exp e = Some b and use that while reasoning on your function push. You will probably see quickly 2 things:

  1. that the lemma I propose does not hold (and I think you want to fix bool_of_exp)
  2. that you will need so called inversion lemmas for your typing derivations.

You could prove intrinsically that push is type preserving (by providing a notion of typing derivation for sexp, passing a proof of well-typedness of e as argument, a proof that f is type preserving, and building a proof that the result is well-typed), but mixing code and reasoning is not such a good practice when you have the opportunity to split them apart (which is the case here).

With respect to your point 2, I think that using dummy directly is much more straightforward and your lemmas on push should show that it can not be obtained unintentionally (following the adage “Garbage in, garbage out”).

3

Thanks! I ended up doing something slightly different, but your response pointed me in the right direction.

– Nicolas