Provable Compiler

Progress

I have chosen for my project in the Formal Methods (CS6110) class is to prove a very simple compiler. This compiler only recognizes four basic statement types: Assignment, Condition, Loop, and Iterate. An additional statement, Procedure Call, may be added later if time permits.
For a more detailed description, read the proposal (PDF).

The prover will work with two tools, ML and HOL. Since there are many different versions of HOL and since each appears to work differently, I have made the version I am using through this download. Please keep in mind that this is about 7MB.
I began working on a tool that will facilitate working with HOL. This tool opens a server socket on a host machine and connects to a HOL session. Eventually, I would like to use a Java client to track a session for the user.

While working on the proof, I had to convince myself that it is possible to prove a compiler "correct". Here (PDF) I used both theoretical and functional methods to demonstrate that a program is an ordered array of statements and a compiler is a composite of transform functions that match up with each program statement. Later, I wrote a program interpreter, compiler, and opcode-evaluator in ML.

My effort was to convert the full ML program to a HOL program.

(***********************************************************************)
load "intLib";
load "stringLib";
type_abbrev("ID", Type`:string`);
Hol_datatype `operand = Num of int | VarName of ID | Empty`;
Hol_datatype `opcode = opPush of operand | opAdd | opSub | opMul | opDiv | opGt | opGtEq
    | opLt | opLtEq | opEq | opNEq | opNeg | opAnd | opOr | opNot | opXor
    | opBrT of int| opBrF of int| opJmp of int| opPop of ID | Label of int`;

Hol_datatype `arith_exp =
     Term     of operand
    |Add      of arith_exp => arith_exp
    |Subtract of arith_exp => arith_exp
    |Multiply of arith_exp => arith_exp
    |Divide   of arith_exp => arith_exp
    |Negate   of arith_exp`;

Hol_datatype `bool_exp =
     Gt  of arith_exp => arith_exp
    |Lt  of arith_exp => arith_exp
    |Eq  of arith_exp => arith_exp
    |LtE of arith_exp => arith_exp
    |GtE of arith_exp => arith_exp
    |NEq of arith_exp => arith_exp
    |And of  bool_exp => bool_exp
    |Or  of  bool_exp => bool_exp
    |Xor of  bool_exp => bool_exp
    |Not of  bool_exp`;

Hol_datatype `statement =
     Assign        of ID => arith_exp
    |Loop_PreTest  of bool_exp => statement list
    |Loop_PostTest of statement list => bool_exp
    |Iterate       of ID => arith_exp => arith_exp => arith_exp => statement list
    |If_Then       of bool_exp => statement list
    |If_Then_Else  of bool_exp => statement list => statement list`;

val getnum_def = Define `
   (getnum(Num(i)) = i)`;

val STRLT_def = Define `
   (STRLT "" s = T) /\
   (STRLT (STRING c s) "" = F) /\
   (STRLT (STRING c1 t1) (STRING c2 t2) = ORD c1 < ORD c2 /\ STRLT t1 t2)`;

val setvar_def = Define `
   (setvar([], n:ID, v:operand) = [(n,v)]) /\
   (setvar(((N, V)::List), n, v) =
      if STRLT N n then (N,V)::setvar(List, n, v)
      else if N = n then (N, v)::List
      else (n,v)::(N,V)::List)`;

val getvar_def = Define ` 
   (getvar([], n:ID) = Empty) /\
   (getvar(((N, V)::List), n) =
      if STRLT N n then getvar(List, n)
      else if N = n then V
      else Empty)`;

val evalexp_def = Define `
   (evalexp(Term(Empty), VarTable) = 0) /\
   (evalexp(Term(Num(r)), VarTable) = r) /\
   (evalexp(Add A B, VarTable) = evalexp(A, VarTable) + evalexp(B, VarTable)) /\
   (evalexp(Subtract A B, VarTable) = evalexp(A, VarTable) - evalexp(B, VarTable)) /\
   (evalexp(Multiply A B, VarTable) = evalexp(A, VarTable) * evalexp(B, VarTable)) /\
   (evalexp(Divide A B, VarTable) = evalexp(A, VarTable) / evalexp(B, VarTable)) /\
   (evalexp(Negate A, VarTable) = ~(evalexp(A, VarTable))) /\
   (evalexp(Term(VarName(v)), VarTable) = getnum(getvar(VarTable, v)))`;

val evalbool_def = Define `
   (evalbool((Gt A1 A2), VarTable) = evalexp(A1, VarTable) > evalexp(A2, VarTable)) /\
   (evalbool((Lt A1 A2), VarTable) = evalexp(A1, VarTable) < evalexp(A2, VarTable)) /\
   (evalbool((Eq A1 A2), VarTable) = (evalexp(A1, VarTable) = evalexp(A2, VarTable))) /\
   (evalbool((LtE A1 A2), VarTable) = evalexp(A1, VarTable) <= evalexp(A2, VarTable)) /\
   (evalbool((GtE A1 A2), VarTable) = evalexp(A1, VarTable) >= evalexp(A2, VarTable)) /\
   (evalbool((NEq A1 A2), VarTable) = ~((evalexp(A1, VarTable)) = (evalexp(A2, VarTable)))) /\
   (evalbool((And B1 B2), VarTable) = evalbool(B1, VarTable) /\ evalbool(B2, VarTable)) /\
   (evalbool((Or B1 B2), VarTable) = evalbool(B1, VarTable) \/ evalbool(B2, VarTable)) /\
   (evalbool((Xor B1 B2), VarTable) = ~(evalbool(B1, VarTable) = evalbool(B2, VarTable))) /\
   (evalbool((Not B), VarTable) = ~(evalbool(B, VarTable)))`;

val defn = Hol_defn "evaluate1" `
   (evaluate1(0n, _, VarTable) = VarTable) /\
   (evaluate1(_, [], VarTable) = VarTable) /\
   (evaluate1(N, ((Assign Var Exp)::Program), VarTable) = 
      evaluate1(N-1, Program, setvar(VarTable, Var, Num(evalexp(Exp, VarTable))))) /\ 
   (evaluate1(N, ((If_Then B_exp St)::Program), VarTable) = 
      if evalbool(B_exp, VarTable) 
         then evaluate1(N-1, Program, evaluate1(N-1, St, VarTable)) 
         else evaluate1(N-1, Program, VarTable)) /\
   (evaluate1(N, ((If_Then_Else B_exp St Sf)::Program), VarTable) = 
      if evalbool(B_exp, VarTable) 
         then evaluate1(N-1, Program, evaluate1(N-1, St, VarTable)) 
         else evaluate1(N-1, Program, evaluate1(N-1, Sf, VarTable))) /\
   (evaluate1(N, ((Loop_PreTest B_exp St)::Program), VarTable) = 
      if evalbool(B_exp, VarTable) 
         then evaluate1(N-1, ((Loop_PreTest B_exp St)::Program), evaluate1(N-1, St, VarTable))
         else evaluate1(N-1, Program, VarTable)) /\
   (evaluate1(N, ((Loop_PostTest St B_exp)::Program), VarTable) =
      let VarTable = evaluate1(N-1, St, VarTable) in
         if evalbool(B_exp, VarTable)
            then evaluate1(N-1, ((Loop_PostTest St B_exp)::Program), evaluate1(N-1, St, VarTable))
            else evaluate1(N-1, Program, VarTable)
      ) /\
   (evaluate1(N, ((Iterate Var Low High Inc St)::Program), VarTable) = 
      let VarTable = setvar(VarTable, Var, Num(evalexp(Low, VarTable))) in
      let NewLow = Term(Num(evalexp(Add Low Inc, VarTable))) in
         if evalbool(GtE Low High, VarTable)
            then evaluate1(N-1, ((Iterate Var NewLow High Inc St)::Program), evaluate1(N-1, St, VarTable))
            else evaluate1(N-1, Program, VarTable))`;
val (evaluate1_def, evaluate1_ind) = Defn.tprove(defn, WF_REL_TAC `measure FST`);

val evaluate_def = Define `
   (evaluate(Program, State) = ?n. evaluate1(n, Program, []) = State)`;

val compexp_def = Define `
   (compexp(Term(Empty)) = [opPush(Empty)]) /\
   (compexp(Term(Num(r))) = [opPush(Num(r))]) /\
   (compexp(Term(VarName(v))) = [opPush(VarName(v))]) /\
   (compexp(Add A B) = compexp(A) ++ compexp(B) ++ [opAdd]) /\
   (compexp(Subtract A B) = compexp(A) ++ compexp(B) ++ [opSub]) /\
   (compexp(Multiply A B) = compexp(A) ++ compexp(B) ++ [opMul]) /\
   (compexp(Divide A B) = compexp(A) ++ compexp(B) ++ [opDiv]) /\
   (compexp(Negate A) = compexp(A) ++ [opNeg])`;

val compbool_def = Define `
   (compbool(Gt A1 A2) = compexp(A1) ++ compexp(A2) ++ [opGt]) /\
   (compbool(Lt A1 A2) = compexp(A1) ++ compexp(A2) ++ [opLt]) /\
   (compbool(Eq A1 A2) = compexp(A1) ++ compexp(A2) ++ [opEq]) /\
   (compbool(LtE A1 A2) = compexp(A1) ++ compexp(A2) ++ [opLtEq]) /\
   (compbool(GtE A1 A2) = compexp(A1) ++ compexp(A2) ++ [opGtEq]) /\
   (compbool(NEq A1 A2) = compexp(A1) ++ compexp(A2) ++ [opNEq]) /\
   (compbool(And B1 B2) = compbool(B1) ++ compbool(B2) ++ [opAnd]) /\
   (compbool(Or B1 B2) = compbool(B1) ++ compbool(B2) ++ [opOr]) /\
   (compbool(Xor B1 B2) = compbool(B1) ++ compbool(B2) ++ [opXor]) /\
   (compbool(Not B) = compbool(B) ++ [opNot])`;

val defn = Hol_defn "compile1" `
   (compile1([], label) = ([], label)) /\
   (compile1(((Assign Var Exp)::Program), label) = 
	   let (prog_ops, label) = compile1(Program, label) in
          ( compexp(Exp) ++
           [opPop Var] ++
           prog_ops, label )) /\
   (compile1(((If_Then B_exp St)::Program), label) = 
       let DoneLabel = label in
       let (stmt_ops, label) = compile1(St, label+1) in
       let (prog_ops, label) = compile1(Program, label) in
          ( compbool(B_exp) ++
           [opBrF DoneLabel] ++
           stmt_ops ++
           [Label DoneLabel] ++
           prog_ops, label )) /\
   (compile1(((If_Then_Else B_exp St Sf)::Program), label) = 
       let ElseLabel = label in
       let DoneLabel = label+1 in
       let (stmtT_ops, label) = compile1(St, label+2) in
       let (stmtF_ops, label) = compile1(Sf, label) in
       let (prog_ops, label) = compile1(Program, label) in
          ( compbool(B_exp) ++
           [opBrF ElseLabel] ++
           stmtT_ops ++
           [opJmp DoneLabel] ++
           [Label ElseLabel] ++
           stmtF_ops ++
           [Label DoneLabel] ++
           prog_ops, label)) /\
   (compile1(((Loop_PreTest B_exp St)::Program), label) =
       let TestLabel = label in
       let DoneLabel = label+1 in
       let (stmt_ops, label) = compile1(St, label+2) in
       let (prog_ops, label) = compile1(Program, label) in
          ( [Label TestLabel] ++
           compbool(B_exp) ++
           [opBrF DoneLabel] ++
           stmt_ops ++
           [opJmp TestLabel] ++
           [Label DoneLabel] ++
           prog_ops, label )) /\
   (compile1(((Loop_PostTest St B_exp)::Program), label) =
       let TestLabel = label in
       let (stmt_ops, label) = compile1(St, label+1) in
       let (prog_ops, label) = compile1(Program, label) in
          ( [Label TestLabel] ++
           stmt_ops ++
           compbool(B_exp) ++
           [opBrT TestLabel] ++
           prog_ops, label )) /\
   (compile1(((Iterate Var El Eh Ei St)::Program), label) = 
       let AssignLabel = label in
       let DoneLabel = label+1 in
       let (stmt_ops, label) = compile1(St, label+2) in
       let (prog_ops, label) = compile1(Program, label) in
          (  compexp(El) ++
           [Label AssignLabel] ++
           [opPop(Var)] ++
           compexp(Eh) ++
           [opPush (VarName Var)] ++
           [opGt] ++
           [opBrT DoneLabel] ++
           stmt_ops ++
           compexp(Ei) ++
           [opPush (VarName Var)] ++
           [opAdd] ++
           [opJmp AssignLabel] ++
           [Label DoneLabel] ++
           prog_ops, label ))`;

val statement_size_def = fetch "-" "statement_size_def";
val list_size_def = listTheory.list_size_def;
val list_size_eq_statement1_size = 
   Q.prove (`!sl. list_size statement_size sl = statement1_size sl`, Induct 
      THEN RW_TAC list_ss [statement_size_def,list_size_def]);
val (compile1_def, compile1_ind) = 
   Defn.tprove (defn, WF_REL_TAC `measure (list_size statement_size o FST)` 
      THEN RW_TAC arith_ss [list_size_eq_statement1_size]); 

val compile_def = Define `
   (compile(Program) = 
       let (oplist, lbl) = compile1(Program, 1) in
          oplist)`;

val findlabel_def = Define `
   (findlabel([], L) = []) /\
   (findlabel((Label(l)::P), L) = if l = L then P else findlabel(P, L)) /\
   (findlabel((_::P), L) = findlabel(P, L))`;

val defn = Hol_defn "interpret1" `
   (interpret1(0n, _, _, VarTable, _) = VarTable) /\
   (interpret1(_, _, [], VarTable, _) = VarTable) /\
   (interpret1(N, WOpcodes, (opPush(Empty)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, Q)) /\
   (interpret1(N, WOpcodes, (opPush(Num Val)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [(Num Val)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opPush(VarName Var)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [getvar(VarTable, Var)] ++ Q)) /\ 
   (interpret1(N, WOpcodes, ((opPop Var)::Opcodes), VarTable, (op1::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, setvar(VarTable, Var, op1), Q)) /\ 
   (interpret1(N, WOpcodes, (opAdd::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1+val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opSub::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1-val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opDiv::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1/val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opMul::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1*val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opGt::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opLtEq::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1<=val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opEq::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1=val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opNEq::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=val2) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opNeg::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(~val1)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opNot::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=0) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opAnd::Opcodes), VarTable, (Num(val1)::Num(val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=0) /\ ~(val2=0) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opOr::Opcodes), VarTable, (Num(val1)::Num(val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=0) \/ ~(val2=0) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opXor::Opcodes), VarTable, (Num(val1)::Num(val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=val2) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, ((opBrT L)::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, (if ~(val1=0) then findlabel(WOpcodes,L) else Opcodes), VarTable, Q)) /\
   (interpret1(N, WOpcodes, ((opBrF L)::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, (if val1=0 then findlabel(WOpcodes,L) else Opcodes), VarTable, Q)) /\
   (interpret1(N, WOpcodes, ((opJmp L)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, findlabel(WOpcodes,L), VarTable, Q)) /\
   (interpret1(N, WOpcodes, ((Label _)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, Q))`;
val (interpret1_def, interpret1_ind) = Defn.tprove(defn, WF_REL_TAC `measure FST`);

val interpret_def = Define `
   (interpret(Opcodes, State) = ?n. interpret1(n, Opcodes, Opcodes, [], []) = State)`;

val statesEqual_def = Define `
   (statesEqual([], []) = T) /\
   (statesEqual([], _) = F) /\
   (statesEqual(_, []) = F) /\
   (statesEqual(((N1:ID,V1:operand)::L1),((N2:ID,V2:operand)::L2)) = 
      (N1=N2) /\ (V1=V2) /\ statesEqual(L1,L2))`;

(*-----------------------------------------PROOF------------------------------------------*)
g `!n p1 p2 st stk prog m state1 state2.
       (p1 = compile prog) /\ (p1=p2) /\ (st=[]) /\ (stk=[]) /\
       (interpret1(n,p1,p2,st,stk) = state1) /\
       (evaluate1(m,prog,st) = state2)
        ==>
       (state1 = state2)`;

e (recInduct interpret1_ind);
e (REPEAT CONJ_TAC THEN REPEAT GEN_TAC);
e (SIMP_TAC std_ss [interpret1_def]);

Then, I tried a smaller ML program to a HOL program.

(***************************************HOL PROGRAM***************************************)
load "intLib";
load "stringLib";
type_abbrev("ID", Type`:string`);
Hol_datatype `operand = Num of num | VarName of ID | Empty`;
Hol_datatype `opcode = opPush of operand | opAdd | opPop of ID `;

Hol_datatype `arith_exp =
     Term     of operand
    |Add      of arith_exp => arith_exp`;

Hol_datatype `statement =
     Assign        of ID => arith_exp`;

val getnum_def = Define `
   (getnum(Num(i)) = i)`;

val STRLT_def = Define `
   (STRLT "" s = T) /\
   (STRLT (STRING c s) "" = F) /\
   (STRLT (STRING c1 t1) (STRING c2 t2) = ORD c1 < ORD c2 /\ STRLT t1 t2)`;

val setvar_def = Define `
   (setvar(a, _, VarName(_)) = a) /\
   (setvar([], n:ID, v:operand) = [(n,v)]) /\
   (setvar(((N, V)::List), n, v) =
      if STRLT N n then (N,V)::setvar(List, n, v)
      else if N = n then (N, v)::List
      else (n,v)::(N,V)::List)`;

val getvar_def = Define ` 
   (getvar([], n:ID) = Empty) /\
   (getvar(((N, V)::List), n) =
      if STRLT N n then getvar(List, n)
      else if N = n then V
      else Empty)`;

val evaladd_def = Define `
	(evaladd(Num(x), Num(y)) = Num(x+y)) /\
	(evaladd(_, _) = Empty)`;

val evalexp_def = Define `
   (evalexp(Term(Empty), _) = Empty) /\
   (evalexp(Term(Num(r)), _) = Num(r)) /\
   (evalexp(Add A B, VarTable) = evaladd(evalexp(A, VarTable), evalexp(B, VarTable))) /\
   (evalexp(Term(VarName(v)), VarTable) = getvar(VarTable, v))`;

val evaluate1_def = Define `
   (evaluate1([], VarTable) = VarTable) /\
   (evaluate1(((Assign Var Exp)::Program), VarTable) = 
      evaluate1(Program, setvar(VarTable, Var, evalexp(Exp, VarTable))))`; 
val evaluate1_ind = fetch "-" "evaluate1_ind";

val evaluate_def = Define `
   (evaluate(Program) = evaluate1(Program, []))`;

val compexp_def = Define `
   (compexp(Term(Empty)) = [opPush(Empty)]) /\
   (compexp(Term(Num(r))) = [opPush(Num(r))]) /\
   (compexp(Term(VarName(v))) = [opPush(VarName(v))]) /\
   (compexp(Add A B) = compexp(A) ++ compexp(B) ++ [opAdd])`;

val compile1_def = Define `
   (compile1([]) = ([])) /\
   (compile1(((Assign Var Exp)::Program)) = 
          compexp(Exp) ++
           [opPop Var] ++
           compile1(Program) )`;
val compile1_ind = fetch "-" "compile1_ind";

val compile_def = Define `
   (compile(Program) = compile1(Program))`;

val interpret1_def = Define `
   (interpret1(((opPop Var)::Opcodes), VarTable, []) = 
               interpret1(Opcodes, setvar(VarTable, Var, Empty), [])) /\
   (interpret1([], VarTable, _) = VarTable) /\
   (interpret1((opPush(Empty)::Opcodes), VarTable, Q) = 
               interpret1(Opcodes, VarTable, Q)) /\
   (interpret1((opPush(Num Val)::Opcodes), VarTable, Q) = 
               interpret1(Opcodes, VarTable, [(Num Val)] ++ Q)) /\
   (interpret1((opPush(VarName Var)::Opcodes), VarTable, Q) = 
               interpret1(Opcodes, VarTable, [getvar(VarTable, Var)] ++ Q)) /\ 
   (interpret1(((opPop Var)::Opcodes), VarTable, (op1::Q)) = 
               interpret1(Opcodes, setvar(VarTable, Var, op1), Q)) /\ 
   (interpret1((opAdd::Opcodes), VarTable, []) = 
               interpret1(Opcodes, VarTable, [Empty])) /\
   (interpret1((opAdd::Opcodes), VarTable, [_]) = 
               interpret1(Opcodes, VarTable, [Empty])) /\
   (interpret1((opAdd::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(Opcodes, VarTable, [Num(val1+val2)] ++ Q)) /\
   (interpret1((opAdd::Opcodes), VarTable, (_::_::Q)) = 
               interpret1(Opcodes, VarTable, [Empty] ++ Q))`;
val interpret1_ind = fetch "-" "interpret1_ind";

val interpret_def = Define `
   (interpret(Opcodes) = interpret1(Opcodes, [], []))`;


(*******************************************PROOF*******************************************)
g `!prog p state1 state2.
(p = compile prog) /\ (interpret(p) = state1) /\ (evaluate(prog) = state2) ==> (state1 = state2)`;
e (SIMP_TAC std_ss [compile_def, interpret_def, evaluate_def]);
e (recInduct compile1_ind);
e (FULL_SIMP_TAC std_ss [compile1_def, interpret1_def, evaluate1_def]);
e (GEN_TAC);
e (Induct_on `Program`);
e (RW_TAC std_ss [compile1_def, evaluate1_def, interpret1_def]);
e (Induct_on `Exp`);
e (GEN_TAC);
e (SIMP_TAC list_ss [setvar_def]);
Parse.hide "o";
e (Cases_on `$o` THEN RW_TAC list_ss [evalexp_def, compexp_def, setvar_def, getvar_def, interpret1_def]);
e (RW_TAC list_ss [compexp_def, evalexp_def, evaladd_def]);
e (FULL_SIMP_TAC list_ss []);
e (Induct_on `Exp`);
e GEN_TAC;
e (Induct_on `Exp'`);
e GEN_TAC;
e (RW_TAC list_ss [evalexp_def]);
e (Cases_on `$o`);
e (Cases_on `o'` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (RW_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `$o` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `Exp'`);
e (Cases_on `Exp''`);
e (Cases_on `o'`);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'`);
e (Cases_on `a`);
e (Cases_on `a0`);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'`);
e (Cases_on `a`);
e (Cases_on `a0'`);
e (Cases_on `o'`);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'`);
e (Cases_on `a`);
e (Cases_on `a0`);






(*--------------------------Lemma: recursive proof of interpret1()--------------------------*)
g `!X Y V Q. interpret1(X ++ Y::Prog, V, Q) = interpret1(Y::Prog,interpret1(X, V, Q), Q)`;
e (RW_TAC list_ss []);
e (Induct_on `X`);
e (RW_TAC list_ss [interpret1_def]);
e (Cases_on `h`);
e (Cases_on `o'` THEN RW_TAC list_ss [interpret1_def, getvar_def, setvar_def]);

My effort was to convert the tiny ML program to a HOL program.

Parse.hide "o";
load "stringLib";
type_abbrev("ID", Type`:string`);
Hol_datatype `operand = Num of num | Empty`;
Hol_datatype `opcode = opAdd | opPush of operand`;
Hol_datatype `arith_exp = Term of operand |Add of arith_exp => arith_exp`;
Hol_datatype `statement = Assign of ID => arith_exp`;

val interpAdd_def = Define `
    (interpAdd(Num(x), Num(y)) = Num(x+y)) /\
    (interpAdd(_, _) = Empty)`;
val interpExp_def = Define `
    (interpExp(Term(Empty)) = Empty) /\
    (interpExp(Term(Num(r))) = Num(r)) /\
    (interpExp(Add A B) = interpAdd(interpExp(A), interpExp(B)))`;
val interpExp_ind = fetch "-" "interpExp_ind";

val compExp_def = Define `
    (compExp(Term(Empty)) = [opPush(Empty)]) /\
    (compExp(Term(Num(r))) = [opPush(Num(r))]) /\
    (compExp(Add A B) = compExp(A) ++ compExp(B) ++ [opAdd])`;
    
val evaluate_def = Define `
    (evaluate((opPush(Empty)::Opcodes), Q) = evaluate(Opcodes, Q)) /\
    (evaluate((opPush(Num Val)::Opcodes), Q) = evaluate(Opcodes, [(Num Val)] ++ Q)) /\
    (evaluate((opAdd::Opcodes), val1::val2::Q) = evaluate(Opcodes, [interpAdd(val1, val2)] ++ Q)) /\
(*    (evaluate((opAdd::Opcodes), ((Num val1)::(Num val2)::Q)) = evaluate(Opcodes, [Num(val1+val2)] ++ Q)) /\*)
(*    (evaluate((_::Opcodes), (_::_::Q)) = evaluate(Opcodes, [Empty] ++ Q)) /\*)
    (evaluate((_::Opcodes), [_]) = evaluate(Opcodes, [Empty])) /\
    (evaluate((_::Opcodes), []) = evaluate(Opcodes, [Empty])) /\
    (evaluate([], top::Q) = top) /\
    (evaluate([], []) = Empty)`;
val evaluate_ind = fetch "-" "evaluate_ind";


(*----------------------------------------------------------------------------*)
val comp_ss = list_ss ++ rewrites [interpAdd_def, interpExp_def, compExp_def, evaluate_def];
g `!oplist prog. (oplist = compExp prog) ==> (evaluate(oplist, []) = interpExp(prog))`;
e (FULL_SIMP_TAC comp_ss []);
e Induct;
e (Cases_on `$o` THEN FULL_SIMP_TAC comp_ss []);
e (RW_TAC comp_ss []);
g `evaluate(A ++ [opAdd], []) = evaluate([opAdd] ++ [evaluate(A, [])], [])`;

g `!prog oplist op. (oplist = compExp prog) /\ (op::L = oplist) ==> ~(op = opAdd)`;
e (Induct_on `prog` THEN FULL_SIMP_TAC comp_ss []);
e (Cases_on `$o` THEN RW_TAC comp_ss []);

g `!p p'. Add(p p') ==>

With Konrad's significant help, we came up with this final tiny ML program HOL program.

Parse.hide "o";
load "stringLib";

type_abbrev("ID", Type`:string`);
Hol_datatype `operand = Num of num | Empty`;
Hol_datatype `opcode = opAdd | opPush of operand`;
Hol_datatype `arith_exp = Term of operand | Add of arith_exp => arith_exp`;

Hol_datatype `statement = Assign of ID => arith_exp`;

val interpAdd_def = Define `
    (interpAdd(Num(x), Num(y)) = Num(x+y)) /\
    (interpAdd(_, _) = Empty)`;
val interpExp_def = Define `
    (interpExp(Term(Empty)) = Empty) /\
    (interpExp(Term(Num(r))) = Num(r)) /\
    (interpExp(Add A B) = interpAdd(interpExp(A), interpExp(B)))`;
val interpExp_ind = fetch "-" "interpExp_ind";

val compExp_def = Define `
    (compExp(Term(Empty)) = [opPush(Empty)]) /\
    (compExp(Term(Num(r))) = [opPush(Num(r))]) /\
    (compExp(Add A B) = compExp(A) ++ compExp(B) ++ [opAdd])`;
    
val evaluate_def = Define `
    (evaluate((opPush(Empty)::Opcodes), Q) = evaluate(Opcodes, Q)) /\
    (evaluate((opPush(Num Val)::Opcodes), Q) = evaluate(Opcodes, [(Num Val)] ++ Q)) /\
    (evaluate((opAdd::Opcodes), val1::val2::Q) = evaluate(Opcodes, [interpAdd(val1, val2)] ++ Q)) /\
(*    (evaluate((opAdd::Opcodes), ((Num val1)::(Num val2)::Q)) = evaluate(Opcodes, [Num(val1+val2)] ++ Q)) /\*)
(*    (evaluate((_::Opcodes), (_::_::Q)) = evaluate(Opcodes, [Empty] ++ Q)) /\*)
    (evaluate((_::Opcodes), [_]) = evaluate(Opcodes, [Empty])) /\
    (evaluate((_::Opcodes), []) = evaluate(Opcodes, [Empty])) /\
    (evaluate([], top::Q) = top) /\
    (evaluate([], []) = Empty)`;
val evaluate_ind = fetch "-" "evaluate_ind";


(*----------------------------------------------------------------------------*)
val comp_ss = list_ss ++ rewrites [interpAdd_def, interpExp_def, compExp_def, evaluate_def];
g `!oplist prog. (oplist = compExp prog) ==> (evaluate(oplist, []) = interpExp(prog))`;
e (FULL_SIMP_TAC comp_ss []);
e Induct;
e (Cases_on `$o` THEN FULL_SIMP_TAC comp_ss []);
e (RW_TAC comp_ss []);
g `evaluate(A ++ [opAdd], []) = evaluate([opAdd] ++ [evaluate(A, [])], [])`;

g `!prog oplist op. (oplist = compExp prog) /\ (op::L = oplist) ==> ~(op = opAdd)`;
e (Induct_on `prog` THEN FULL_SIMP_TAC comp_ss []);
e (Cases_on `$o` THEN RW_TAC comp_ss []);


load "stringLib";
open listTheory;

map hide ["o", "C"];

Hol_datatype `aexp = Var of string | Const of num | Add of aexp => aexp`;

Hol_datatype `atom = V of string | C of num`;

Hol_datatype `opcode = opAdd | opPush of atom`;

val evalExp_def =
 Define 
    `(evalExp env (Var s) = env s :num) /\
     (evalExp env (Const n) = n) /\
     (evalExp env (Add e1 e2) = evalExp env e1 + evalExp env e2)`;

val compExp_def =
 Define 
    `(compExp (Var s) = [opPush (V s)]) /\
     (compExp (Const n) = [opPush (C n)]) /\
     (compExp (Add e1 e2) = compExp e2 ++ compExp e1 ++ [opAdd])`;

val Int_def = 
 Define
  `(Int env [] stk = stk) /\
   (Int env (opPush(V s)::opcodes) stk = Int env opcodes (env s :: stk)) /\
   (Int env (opPush(C n)::opcodes) stk = Int env opcodes (n :: stk)) /\
   (Int env (opAdd::opcodes) (v1::v2::stk) = Int env opcodes (v1+v2::stk))`;

val Int_ind = fetch "-" "Int_ind";
val comp_ss = list_ss ++ rewrites [evalExp_def, compExp_def, Int_def];

(*---------------------------------------------------------------------------*)
(* Lemmas                                                                    *)
(*---------------------------------------------------------------------------*)
 
val compExp_not_empty = Q.prove
(`!e. ~NULL (compExp e)`,
 Induct THEN RW_TAC comp_ss [] THEN 
 Cases_on `compExp e'` THEN FULL_SIMP_TAC comp_ss []);

val NOT_NULL = Q.prove
(`!l. ~NULL l ==> ?h t. l = h::t`,
Cases THEN RW_TAC list_ss []);

val NULL_EMPTY_LEM = Q.prove
(`!l. NULL l = (l=[])`,
Cases THEN RW_TAC list_ss []);

val compExp_hd_not_Add = Q.prove
(`!e. ~(HD (compExp e) = opAdd)`,
 Induct THEN RW_TAC comp_ss [] THEN 
 `?h t. compExp e' = h::t` by METIS_TAC [compExp_not_empty, NOT_NULL] THEN
 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC comp_ss []);

val THE_LEMMA = Q.prove
(`!e env stk rst.
      Int env (compExp e ++ rst) stk = 
      Int env rst (evalExp env e::stk)`,
 Induct THEN RW_TAC comp_ss [] THEN
 ASM_REWRITE_TAC [GSYM APPEND_ASSOC] THEN
 RW_TAC comp_ss []);

val Correctness = Q.prove
(`!e env stk h stk'. 
    (Int env (compExp e) stk = h::stk') ==> (h = evalExp env e)`,
 Induct THEN RW_TAC comp_ss [] 
   THEN RULE_ASSUM_TAC (REWRITE_RULE [GSYM APPEND_ASSOC]) 
   THEN FULL_SIMP_TAC comp_ss [THE_LEMMA]);


Copyright © 2001-2006 Intelligent Algorithmic Solutions and Sean Walton	eMail