

theory Expr

  use int.Int

  type expr = Cte int | Plus expr expr | Minus expr expr | Mult expr expr

  function eval_expr (e:expr) : int =
    match e with
    | Cte n -> n
    | Plus e1 e2 -> eval_expr e1 + eval_expr e2
    | Minus e1 e2 -> eval_expr e1 - eval_expr e2
    | Mult e1 e2 -> eval_expr e1 * eval_expr e2
    end

end

theory StackMachine

  type asm = Push int | Add | Sub | Mul

  use export int.Int
  use export list.List

  function compute (s:list int) (a:list asm) : list int =
    match a with
    | Nil -> s
    | Cons a r ->
      match a,s with
      | Push n, _                  -> compute (Cons n s) r
      | Add, (Cons n1 (Cons n2 s)) -> compute (Cons (n2+n1) s) r
      | Sub, (Cons n1 (Cons n2 s)) -> compute (Cons (n2-n1) s) r
      | Mul, (Cons n1 (Cons n2 s)) -> compute (Cons (n2*n1) s) r
      | _ -> s
      end
    end

end


module Compiler
  
  use export list.Append
  use Expr
  use StackMachine
  
  function compile (e:expr) : list asm =
    match e with
    | Cte n -> Cons (Push n) Nil
    | Plus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Add Nil)
    | Minus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Sub Nil)
    | Mult e1 e2 -> compile e1 ++ (compile e2 ++ Cons Mul Nil)
    end

  let rec lemma soundness_gen (e:expr) (s:list int) (r:list asm)
    variant { e }
    ensures { compute s (compile e ++ r) = compute (Cons (eval_expr e) s) r }
  = match e with
    | Cte n -> 
      assert { compile e ++ r = Cons (Push n) r }
    | Plus e1 e2 ->
      soundness_gen e1 s (compile e2 ++ Cons Add r);
      soundness_gen e2 (Cons (eval_expr e1) s) (Cons Add r)
    | Minus e1 e2 ->
      soundness_gen e1 s (compile e2 ++ Cons Sub r);
      soundness_gen e2 (Cons (eval_expr e1) s) (Cons Sub r)
    | Mult e1 e2 ->
      soundness_gen e1 s (compile e2 ++ Cons Mul r);
      soundness_gen e2 (Cons (eval_expr e1) s) (Cons Mul r)
    end
  
  let lemma soundness (e:expr)
    ensures { compute Nil (compile e) = (Cons (eval_expr e) Nil) }
  =
    assert { compute Nil (compile e) = compute Nil (compile e ++ Nil) }

end
