# Soundness of program transformation

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 ->
``````

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

1 Like

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â€ť).

1 Like

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

â€“ Nicolas