Correct by construction stack compiler in LH

ExprCompiler.hs

{-# LANGUAGE GADTs #-}

{-@ LIQUID "--ple"           @-}
{-@ LIQUID "--etabeta"       @-}
{-@ LIQUID "--reflection"    @-}
{-@ LIQUID "--dependantcase" @-}

module ExprCompiler where

import Language.Haskell.Liquid.ProofCombinators

{-@ reflect id @-}
{-@ reflect .  @-}
{-@ infix .    @-}
{-@ infix $    @-}

data Expr where
  EConst :: Int -> Expr
  EAdd :: Expr -> Expr -> Expr
  EMul :: Expr -> Expr -> Expr
  ENeg :: Expr -> Expr
  deriving Show

{-@ reflect eval @-}
eval :: Expr -> Int
eval (EConst x) = x
eval (EAdd e1 e2) = eval e1 + eval e2
eval (EMul e1 e2) = eval e1 * eval e2
eval (ENeg e)     = - (eval e)

type Stack = [Int]

{-@ reflect push @-}
push :: Int -> Stack -> Stack
push v s = v : s

{-@ reflect opAdd @-}
{-@ opAdd :: { s:Stack | len s >= 2 } -> Stack @-}
opAdd :: Stack -> Stack
opAdd (x : y : xs) = (y + x) : xs

{-@ reflect opMul @-}
{-@ opMul :: { s:Stack | len s >= 2 } -> Stack @-}
opMul :: Stack -> Stack
opMul (x : y : xs) = (x * y) : xs

data OpCode where
  OpPush :: Int -> OpCode
  OpAdd :: OpCode
  OpMul :: OpCode
  deriving Show

{-@ reflect execOpCode @-}
{-@ execOpCode :: o:OpCode -> { v:Stack | len v >= minStackSize o } -> Stack @-}
execOpCode :: OpCode -> Stack -> Stack
execOpCode (OpPush x) = push x
execOpCode OpAdd      = opAdd
execOpCode OpMul      = opMul

{-@ reflect minStackSize @-}
minStackSize :: OpCode -> Int
minStackSize (OpPush x) = 0
minStackSize _          = 2

data Program where
{-@ PNil :: Prop (Program id) @-}
  PNil :: Program
{-@ PCons :: op:OpCode
          -> p:(Stack -> { v:Stack | len v >= minStackSize op }) -> Prop (Program p)
          -> Prop (Program (execOpCode op . p)) @-}
  PCons :: OpCode -> (Stack -> Stack) -> Program -> Program
data PROGRAM = Program (Stack -> Stack)

{-@ reflect compose @-}
{-@ compose :: p1:(Stack -> Stack) -> p2:(Stack -> Stack)  
            -> Prop (Program p1) -> Prop (Program p2)
            -> Prop (Program (p2 . p1)) @-}
compose :: (Stack -> Stack) -> (Stack -> Stack) -> Program -> Program -> Program
compose s1 s2 p1 PNil                        = p1
compose s1 s2 p1 (PCons cmd srest rest) =
  PCons cmd (srest . s1) (compose s1 srest p1 rest)

{-@ compile :: e:Expr -> Prop (Program (push $ eval e)) @-}
compile :: Expr -> Program
compile (EConst x)   = PCons (OpPush x) id PNil
compile (EAdd e1 e2) =
  PCons
    OpAdd
    ((push $ eval e1) . (push $ eval e2))
    (compose (push $ eval e2) (push $ eval e1) (compile e2) (compile e1))
compile (EMul e1 e2) =
  PCons
    OpMul
    ((push $ eval e1) . (push $ eval e2))
    (compose (push $ eval e2) (push $ eval e1) (compile e2) (compile e1))
compile (ENeg e)     =
  PCons
    OpMul
    ((push $ -1) . (push $ eval e))
    (PCons (OpPush $ -1) (push $ eval e) (compile e))