-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.VM
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Correctness of a simple interpreter vs virtual-machine interpretation of a language.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE OverloadedLists     #-}
{-# LANGUAGE QuasiQuotes         #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.VM
#ifndef DOCTEST
 (   -- * Language
     Expr(..), SExpr, size


     -- * Symbolic accessors
   , sCaseExpr
   , isVar, sVar, getVar_1,                     svar
   , isCon, sCon, getCon_1,                     scon
   , isSqr, sSqr, getSqr_1,                     ssqrVal
   , isInc, sInc, getInc_1,                     sincVal
   , isAdd, sAdd, getAdd_1, getAdd_2,           sadd1, sadd2
   , isMul, sMul, getMul_1, getMul_2,           smul1, smul2
   , isLet, sLet, getLet_1, getLet_2, getLet_3, slvar, slval, slbody

     -- * Environment and the stack
   , Env, Stack

     -- * Interpretation
   , interpInEnv, interp

     -- * Virtual machine
   , Instr(..), SInstr

     -- * Compilation
   , compile, compileAndRun

     -- * Correctness of the compiler
   , correctness)
#endif
where

import Data.SBV
import Data.SBV.Tuple as ST
import Data.SBV.List  as SL

import Data.SBV.TP

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV.TP
-- >>> :set -XTypeApplications
#endif

-- * Language

-- | Basic expression language.
data Expr nm val = Var {forall nm val. Expr nm val -> nm
var    :: nm                                            } -- ^ Variables
                 | Con {forall nm val. Expr nm val -> val
con    :: val                                           } -- ^ Constants
                 | Sqr {forall nm val. Expr nm val -> Expr nm val
sqrVal :: Expr nm val                                   } -- ^ Squaring
                 | Inc {forall nm val. Expr nm val -> Expr nm val
incVal :: Expr nm val                                   } -- ^ Increment
                 | Add {forall nm val. Expr nm val -> Expr nm val
add1   :: Expr nm val, forall nm val. Expr nm val -> Expr nm val
add2 :: Expr nm val              } -- ^ Addition
                 | Mul {forall nm val. Expr nm val -> Expr nm val
mul1   :: Expr nm val, forall nm val. Expr nm val -> Expr nm val
mul2 :: Expr nm val              } -- ^ Addition
                 | Let {forall nm val. Expr nm val -> nm
lvar   :: nm, forall nm val. Expr nm val -> Expr nm val
lval ::  Expr nm val, forall nm val. Expr nm val -> Expr nm val
lbody :: Expr nm val} -- ^ Let expression

-- | Create symbolic version of expressions
mkSymbolic [''Expr]

-- | Size of an expression. Used in strong induction.
size :: (SymVal nm, SymVal val) => SExpr nm val -> SInteger
size :: forall nm val.
(SymVal nm, SymVal val) =>
SExpr nm val -> SBV Integer
size = String
-> (SExpr nm val -> SBV Integer) -> SExpr nm val -> SBV Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"exprSize" ((SExpr nm val -> SBV Integer) -> SExpr nm val -> SBV Integer)
-> (SExpr nm val -> SBV Integer) -> SExpr nm val -> SBV Integer
forall a b. (a -> b) -> a -> b
$ \SExpr nm val
expr -> [sCase|Expr expr of
                                            Var _     -> 0
                                            Con _     -> 0
                                            Sqr a     -> 1 + size a
                                            Inc a     -> 1 + size a
                                            Add a b   -> 1 + size a `smax` size b
                                            Mul a b   -> 1 + size a `smax` size b
                                            Let _ a b -> 1 + size a `smax` size b
                                         |]

-- | Environment, binding names to values
type Env nm val = SList (nm, val)

-- * Functional interpretation

-- | Interpreter, in the usual functional style, taking an arbitrary environment.
interpInEnv :: (SymVal nm, SymVal val, Num (SBV val)) => Env nm val -> SExpr nm val -> SBV val
interpInEnv :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
Env nm val -> SExpr nm val -> SBV val
interpInEnv = String
-> (Env nm val -> SExpr nm val -> SBV val)
-> Env nm val
-> SExpr nm val
-> SBV val
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"interpInEnv" ((Env nm val -> SExpr nm val -> SBV val)
 -> Env nm val -> SExpr nm val -> SBV val)
-> (Env nm val -> SExpr nm val -> SBV val)
-> Env nm val
-> SExpr nm val
-> SBV val
forall a b. (a -> b) -> a -> b
$ \Env nm val
env SExpr nm val
expr ->
                 [sCase|Expr expr of
                    Var nm    -> nm `SL.lookup` env
                    Con v     -> v
                    Sqr a     -> let av = interpInEnv env a in av * av
                    Inc a     -> let av = interpInEnv env a in av + 1
                    Add a b   -> let av = interpInEnv env a; bv = interpInEnv env b in av + bv
                    Mul a b   -> let av = interpInEnv env a; bv = interpInEnv env b in av * bv
                    Let v a b -> let av = interpInEnv env a in interpInEnv (tuple (v, av) .: env) b
                 |]

-- | Interpret starting from empty environment.
interp :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val
interp :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
interp = Env nm val -> SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
Env nm val -> SExpr nm val -> SBV val
interpInEnv []

-- * Virtual machine

-- | Instructions
data Instr nm val = IPushN { forall nm val. Instr nm val -> nm
ivar :: nm  } -- ^ Push the value of nm from the environment on to the stack
                  | IPushV { forall nm val. Instr nm val -> val
ival :: val } -- ^ Push a value on to the stack
                  | IDup                   -- ^ Duplicate the top of the stack
                  | IAdd                   -- ^ Add      the top two elements and push back
                  | IMul                   -- ^ Multiply the top two elements and push back
                  | IBind nm               -- ^ Bind the value on top of stack to name
                  | IForget                -- ^ Pop and ignore the binding on the environment

-- | Create symbolic version of instructions
mkSymbolic [''Instr]

-- | Stack of values.
type Stack val = SList val

-- | Pushing on to the stack.
push :: SymVal val => SBV val -> Stack val  -> Stack val
push :: forall a. SymVal a => SBV a -> SList a -> SList a
push = SBV val -> SList val -> SList val
forall a. SymVal a => SBV a -> SList a -> SList a
(SL..:)

-- | Top of the stack. If the stack is empty, the result is underspecified.
top :: SymVal val => Stack val  -> SBV val
top :: forall val. SymVal val => Stack val -> SBV val
top = SList val -> SBV val
forall val. SymVal val => Stack val -> SBV val
SL.head

-- | Popping from the stack. If the stack is empty, the result is underspecified.
pop :: SymVal val => Stack val  -> Stack val
pop :: forall val. SymVal val => Stack val -> Stack val
pop = SList val -> SList val
forall val. SymVal val => Stack val -> Stack val
SL.tail

-- | A pair containing an environment and a stack
type EnvStack nm val = SBV ([(nm, val)], [val])

-- | Executing a single instruction in a given environment and the instruction stack.
-- We produce the new environment, and the new stack.
execute :: (SymVal nm, SymVal val, Num (SBV val)) => EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute EnvStack nm val
envStk SInstr nm val
instr = let (SBV [(nm, val)]
env, Stack val
stk) = EnvStack nm val -> (SBV [(nm, val)], Stack val)
forall tup a. Tuple tup a => SBV tup -> a
untuple EnvStack nm val
envStk
                       in (SBV [(nm, val)], Stack val) -> EnvStack nm val
forall tup a. Tuple tup a => a -> SBV tup
tuple [sCase|Instr instr of
                                   IPushN nm   -> (env, push (nm `SL.lookup` env) stk)
                                   IPushV v    -> (env, push v stk)
                                   IDup        -> (env, push (top stk) stk)
                                   IAdd        -> (env, let a = top stk; b = top (pop stk) in push (a + b) (pop (pop stk)))
                                   IMul        -> (env, let a = top stk; b = top (pop stk) in push (a * b) (pop (pop stk)))
                                   IBind nm    -> (push (tuple (nm, top stk)) env, pop stk)
                                   IForget     -> (pop env, stk)
                                |]

-- | Execute a sequence of instructions, in a given stack and env. Returnsg the final environment and the stack. This is a
-- simple fold-left.
run :: (SymVal nm, SymVal val, Num (SBV val)) => EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run = (EnvStack nm val -> SInstr nm val -> EnvStack nm val)
-> EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
forall func a b.
(SFoldL func a b, SymVal a, SymVal b) =>
func -> SBV b -> SList a -> SBV b
SL.foldl EnvStack nm val -> SInstr nm val -> EnvStack nm val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute

-- * Compiler

-- | Convert an expression to a sequence of instructions for our virtual machine.
compile :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SList (Instr nm val)
compile :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SList (Instr nm val)
compile = String
-> (SExpr nm val -> SList (Instr nm val))
-> SExpr nm val
-> SList (Instr nm val)
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"compile" ((SExpr nm val -> SList (Instr nm val))
 -> SExpr nm val -> SList (Instr nm val))
-> (SExpr nm val -> SList (Instr nm val))
-> SExpr nm val
-> SList (Instr nm val)
forall a b. (a -> b) -> a -> b
$ \SExpr nm val
expr ->
                [sCase|Expr expr of
                   Var nm    -> [sIPushN nm]
                   Con v     -> [sIPushV v]
                   Sqr a     -> compile a SL.++ [sIDup,     sIMul]
                   Inc a     -> compile a SL.++ [sIPushV 1, sIAdd]
                   Add a b   -> compile a SL.++ compile b  SL.++ [sIAdd]
                   Mul a b   -> compile a SL.++ compile b  SL.++ [sIMul]
                   Let v a b -> compile a SL.++ [sIBind v] SL.++ compile b SL.++ [sIForget]
                |]

-- | Compile and run an expression.
compileAndRun :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val
compileAndRun :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
compileAndRun = SBV [val] -> SBV val
forall val. SymVal val => Stack val -> SBV val
top (SBV [val] -> SBV val)
-> (SExpr nm val -> SBV [val]) -> SExpr nm val -> SBV val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STuple [(nm, val)] [val] -> SBV [val]
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
ST.snd (STuple [(nm, val)] [val] -> SBV [val])
-> (SExpr nm val -> STuple [(nm, val)] [val])
-> SExpr nm val
-> SBV [val]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STuple [(nm, val)] [val]
-> SList (Instr nm val) -> STuple [(nm, val)] [val]
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run ((SBV [(nm, val)], SBV [val]) -> STuple [(nm, val)] [val]
forall tup a. Tuple tup a => a -> SBV tup
tuple ([], [])) (SList (Instr nm val) -> STuple [(nm, val)] [val])
-> (SExpr nm val -> SList (Instr nm val))
-> SExpr nm val
-> STuple [(nm, val)] [val]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr nm val -> SList (Instr nm val)
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SList (Instr nm val)
compile

-- * Correctness

-- | The property we're after is that interpreting an expression is the same as
-- first compiling it to virtual-machine instructions, and then running them.
--
-- >>> runTP (correctness @String @Integer)
-- Inductive lemma: runSeq
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: runOne                           Q.E.D.
-- Lemma: runTwo
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: runMul                           Q.E.D.
-- Lemma: measureNonNeg                    Q.E.D.
-- Inductive lemma (strong): helper
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (7 way case split)
--     Step: 1.1.1 (case Var)              Q.E.D.
--     Step: 1.1.2                         Q.E.D.
--     Step: 1.2.1 (case Con)              Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--     Step: 1.3.1 (case Sqr)              Q.E.D.
--     Step: 1.3.2                         Q.E.D.
--     Step: 1.3.3                         Q.E.D.
--     Step: 1.3.4                         Q.E.D.
--     Step: 1.3.5                         Q.E.D.
--     Step: 1.3.6                         Q.E.D.
--     Step: 1.3.7                         Q.E.D.
--     Step: 1.4.1 (case Inc)              Q.E.D.
--     Step: 1.4.2                         Q.E.D.
--     Step: 1.4.3                         Q.E.D.
--     Step: 1.4.4                         Q.E.D.
--     Step: 1.4.5                         Q.E.D.
--     Step: 1.4.6                         Q.E.D.
--     Step: 1.4.7                         Q.E.D.
--     Step: 1.5.1 (case sAdd)             Q.E.D.
--     Step: 1.5.2                         Q.E.D.
--     Step: 1.5.3                         Q.E.D.
--     Step: 1.5.4                         Q.E.D.
--     Step: 1.5.5                         Q.E.D.
--     Step: 1.5.6                         Q.E.D.
--     Step: 1.5.7                         Q.E.D.
--     Step: 1.5.8                         Q.E.D.
--     Step: 1.5.9                         Q.E.D.
--     Step: 1.6.1 (case sMul)             Q.E.D.
--     Step: 1.6.2                         Q.E.D.
--     Step: 1.6.3                         Q.E.D.
--     Step: 1.6.4                         Q.E.D.
--     Step: 1.6.5                         Q.E.D.
--     Step: 1.6.6                         Q.E.D.
--     Step: 1.6.7                         Q.E.D.
--     Step: 1.6.8                         Q.E.D.
--     Step: 1.6.9                         Q.E.D.
--     Step: 1.7.1 (case Let)              Q.E.D.
--     Step: 1.7.2                         Q.E.D.
--     Step: 1.7.3                         Q.E.D.
--     Step: 1.7.4                         Q.E.D.
--     Step: 1.7.5                         Q.E.D.
--     Step: 1.7.6                         Q.E.D.
--     Step: 1.7.7                         Q.E.D.
--     Step: 1.7.8                         Q.E.D.
--     Step: 1.7.9                         Q.E.D.
--     Step: 1.7.10                        Q.E.D.
--     Step: 1.7.11                        Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: correctness
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] correctness :: Ɐexpr ∷ (Expr [Char] Integer) → Bool
correctness :: forall nm val. (SymVal nm, SymVal val, Num (SBV val)) => TP (Proof (Forall "expr" (Expr nm val) -> SBool))
correctness :: forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
TP (Proof (Forall "expr" (Expr nm val) -> SBool))
correctness = do

   -- Running a sequence of instructions that are appended is equivalent to running them in sequence:
   Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq <- String
-> (Forall "xs" [Instr nm val]
    -> Forall "ys" [Instr nm val]
    -> Forall "es" ([(nm, val)], [val])
    -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool))
    -> IHArg
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool)
    -> IStepArgs
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool)
         ([(nm, val)], [val]))
-> TP
     (Proof
        (Forall "xs" [Instr nm val]
         -> Forall "ys" [Instr nm val]
         -> Forall "es" ([(nm, val)], [val])
         -> SBool))
forall t.
(Proposition
   (Forall "xs" [Instr nm val]
    -> Forall "ys" [Instr nm val]
    -> Forall "es" ([(nm, val)], [val])
    -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [Instr nm val]
    -> Forall "ys" [Instr nm val]
    -> Forall "es" ([(nm, val)], [val])
    -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool))
    -> IHArg
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool)
    -> IStepArgs
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool)
         t)
-> TP
     (Proof
        (Forall "xs" [Instr nm val]
         -> Forall "ys" [Instr nm val]
         -> Forall "es" ([(nm, val)], [val])
         -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"runSeq"
                    (\(Forall @"xs" SList (Instr nm val)
xs) (Forall @"ys" SList (Instr nm val)
ys) (Forall @"es" (SBV ([(nm, val)], [val])
es :: EnvStack nm val))
                         -> SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es (SList (Instr nm val)
xs SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ SList (Instr nm val)
ys) SBV ([(nm, val)], [val]) -> SBV ([(nm, val)], [val]) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run (SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es SList (Instr nm val)
xs) SList (Instr nm val)
ys) ((Proof
    (IHType
       (Forall "xs" [Instr nm val]
        -> Forall "ys" [Instr nm val]
        -> Forall "es" ([(nm, val)], [val])
        -> SBool))
  -> IHArg
       (Forall "xs" [Instr nm val]
        -> Forall "ys" [Instr nm val]
        -> Forall "es" ([(nm, val)], [val])
        -> SBool)
  -> IStepArgs
       (Forall "xs" [Instr nm val]
        -> Forall "ys" [Instr nm val]
        -> Forall "es" ([(nm, val)], [val])
        -> SBool)
       ([(nm, val)], [val]))
 -> TP
      (Proof
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool)))
-> (Proof
      (IHType
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool))
    -> IHArg
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool)
    -> IStepArgs
         (Forall "xs" [Instr nm val]
          -> Forall "ys" [Instr nm val]
          -> Forall "es" ([(nm, val)], [val])
          -> SBool)
         ([(nm, val)], [val]))
-> TP
     (Proof
        (Forall "xs" [Instr nm val]
         -> Forall "ys" [Instr nm val]
         -> Forall "es" ([(nm, val)], [val])
         -> SBool))
forall a b. (a -> b) -> a -> b
$
                    \Proof
  (IHType
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool))
ih (SBV (Instr nm val)
x, SList (Instr nm val)
xs) SList (Instr nm val)
ys SBV ([(nm, val)], [val])
es -> [] [SBool]
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es ((SBV (Instr nm val)
x SBV (Instr nm val) -> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList (Instr nm val)
xs) SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ SList (Instr nm val)
ys)
                                            SBV ([(nm, val)], [val])
-> ChainsTo (SBV ([(nm, val)], [val]))
-> ChainsTo (SBV ([(nm, val)], [val]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es (SBV (Instr nm val)
x SBV (Instr nm val) -> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList (Instr nm val)
xs SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ SList (Instr nm val)
ys))
                                            SBV ([(nm, val)], [val])
-> ChainsTo (SBV ([(nm, val)], [val]))
-> ChainsTo (SBV ([(nm, val)], [val]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run (SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute SBV ([(nm, val)], [val])
es SBV (Instr nm val)
x) (SList (Instr nm val)
xs SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ SList (Instr nm val)
ys)
                                            SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool))
Proof
  (Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val]) -> SBool)
ih Proof
  (Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val]) -> SBool)
-> IArgs
     (Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val]) -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList (Instr nm val)
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"es" (SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute SBV ([(nm, val)], [val])
es SBV (Instr nm val)
x))
                                            TPProofRaw (SBV ([(nm, val)], [val]))
-> ChainsTo (TPProofRaw (SBV ([(nm, val)], [val])))
-> ChainsTo (TPProofRaw (SBV ([(nm, val)], [val])))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run (SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es (SBV (Instr nm val)
x SBV (Instr nm val) -> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList (Instr nm val)
xs)) SList (Instr nm val)
ys
                                            SBV ([(nm, val)], [val])
-> ChainsTo (SBV ([(nm, val)], [val]))
-> ChainsTo (SBV ([(nm, val)], [val]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV ([(nm, val)], [val]))
TPProofRaw (SBV ([(nm, val)], [val]))
forall a. TPProofRaw a
qed

   -- The following few lemmas make the proof go thru faster, even though they're really easy to prove themselves.

   -- Running one instruction is equal to just executing it
   Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> SBool)
runOne <- String
-> (Forall "es" ([(nm, val)], [val])
    -> Forall "i" (Instr nm val) -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "es" ([(nm, val)], [val])
         -> Forall "i" (Instr nm val) -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"runOne"
                   (\(Forall @"es" (SBV ([(nm, val)], [val])
es :: EnvStack nm val)) (Forall @"i" SBV (Instr nm val)
i) -> SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es [Item (SList (Instr nm val))
SBV (Instr nm val)
i] SBV ([(nm, val)], [val]) -> SBV ([(nm, val)], [val]) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute SBV ([(nm, val)], [val])
es SBV (Instr nm val)
i)
                   []

   -- Same for two
   Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
runTwo <- String
-> (Forall "es" ([(nm, val)], [val])
    -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
-> StepArgs
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
     ([(nm, val)], [val])
-> TP
     (Proof
        (Forall "es" ([(nm, val)], [val])
         -> Forall "i" (Instr nm val)
         -> Forall "j" (Instr nm val)
         -> SBool))
forall t.
(Proposition
   (Forall "es" ([(nm, val)], [val])
    -> Forall "i" (Instr nm val)
    -> Forall "j" (Instr nm val)
    -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "es" ([(nm, val)], [val])
    -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
-> StepArgs
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
     t
-> TP
     (Proof
        (Forall "es" ([(nm, val)], [val])
         -> Forall "i" (Instr nm val)
         -> Forall "j" (Instr nm val)
         -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"runTwo"
                   (\(Forall @"es" (SBV ([(nm, val)], [val])
es :: EnvStack nm val)) (Forall @"i" SBV (Instr nm val)
i) (Forall @"j" SBV (Instr nm val)
j)
                             -> SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es [Item (SList (Instr nm val))
SBV (Instr nm val)
i, Item (SList (Instr nm val))
SBV (Instr nm val)
j] SBV ([(nm, val)], [val]) -> SBV ([(nm, val)], [val]) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute (SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute SBV ([(nm, val)], [val])
es SBV (Instr nm val)
i) SBV (Instr nm val)
j) (StepArgs
   (Forall "es" ([(nm, val)], [val])
    -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
   ([(nm, val)], [val])
 -> TP
      (Proof
         (Forall "es" ([(nm, val)], [val])
          -> Forall "i" (Instr nm val)
          -> Forall "j" (Instr nm val)
          -> SBool)))
-> StepArgs
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
     ([(nm, val)], [val])
-> TP
     (Proof
        (Forall "es" ([(nm, val)], [val])
         -> Forall "i" (Instr nm val)
         -> Forall "j" (Instr nm val)
         -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \SBV ([(nm, val)], [val])
es SBV (Instr nm val)
i SBV (Instr nm val)
j -> [] [SBool]
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run SBV ([(nm, val)], [val])
es [Item (SList (Instr nm val))
SBV (Instr nm val)
i, Item (SList (Instr nm val))
SBV (Instr nm val)
j]
                                 SBV ([(nm, val)], [val])
-> ChainsTo (SBV ([(nm, val)], [val]))
-> ChainsTo (SBV ([(nm, val)], [val]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run (SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute SBV ([(nm, val)], [val])
es SBV (Instr nm val)
i) [Item (SList (Instr nm val))
SBV (Instr nm val)
j]
                                 SBV ([(nm, val)], [val])
-> ChainsTo (SBV ([(nm, val)], [val]))
-> ChainsTo (SBV ([(nm, val)], [val]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute (SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute SBV ([(nm, val)], [val])
es SBV (Instr nm val)
i) SBV (Instr nm val)
j
                                 SBV ([(nm, val)], [val])
-> ChainsTo (SBV ([(nm, val)], [val]))
-> ChainsTo (SBV ([(nm, val)], [val]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV ([(nm, val)], [val]))
TPProofRaw (SBV ([(nm, val)], [val]))
forall a. TPProofRaw a
qed

   -- Provers struggle with multiplication, so help them a bit here even though this is really
   -- a trivial proof. What's hard is the correct instantiation of it, so abstracting it away helps
   -- us speed up the solver.
   Proof
  (Forall "a" val
   -> Forall "b" val
   -> Forall "env" [(nm, val)]
   -> Forall "stk" [val]
   -> SBool)
runMul <- String
-> (Forall "a" val
    -> Forall "b" val
    -> Forall "env" [(nm, val)]
    -> Forall "stk" [val]
    -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" val
         -> Forall "b" val
         -> Forall "env" [(nm, val)]
         -> Forall "stk" [val]
         -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"runMul"
                    (\(Forall @"a" SBV val
a) (Forall @"b" SBV val
b) (Forall  @"env" (Env nm val
env :: Env nm val)) (Forall @"stk" Stack val
stk)
                                 ->   SBV ([(nm, val)], [val])
-> SBV (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SInstr nm val -> EnvStack nm val
execute ((Env nm val, Stack val) -> SBV ([(nm, val)], [val])
forall tup a. Tuple tup a => a -> SBV tup
tuple (Env nm val
env, SBV val -> Stack val -> Stack val
forall a. SymVal a => SBV a -> SList a -> SList a
push SBV val
a (SBV val -> Stack val -> Stack val
forall a. SymVal a => SBV a -> SList a -> SList a
push SBV val
b Stack val
stk))) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul
                                 SBV ([(nm, val)], [val]) -> SBV ([(nm, val)], [val]) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==  (Env nm val, Stack val) -> SBV ([(nm, val)], [val])
forall tup a. Tuple tup a => a -> SBV tup
tuple (Env nm val
env, SBV val -> Stack val -> Stack val
forall a. SymVal a => SBV a -> SList a -> SList a
push (SBV val
a SBV val -> SBV val -> SBV val
forall a. Num a => a -> a -> a
* SBV val
b) Stack val
stk))
                   []

   -- We will use the size of the expression as the measure. We need to show that it is
   -- always positive for the inductive proof to go thru.
   Proof (Forall "e" (Expr nm val) -> SBool)
measureNonNeg <- String
-> (Forall "e" (Expr nm val) -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "e" (Expr nm val) -> SBool))
forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
"measureNonNeg"
                                   (\(Forall @"e" (SExpr nm val
e :: SExpr nm val)) -> SExpr nm val -> SBV Integer
forall nm val.
(SymVal nm, SymVal val) =>
SExpr nm val -> SBV Integer
size SExpr nm val
e SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0)
                                   []

   -- A more general version of the theorem, starting with an arbitrary env and stack.
   -- We prove this using the induction principle for expressions.
   Proof
  (Forall "e" (Expr nm val)
   -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
helper <- SMTConfig
-> String
-> (Forall "e" (Expr nm val)
    -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
-> (MeasureArgs
      (Forall "e" (Expr nm val)
       -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
      Integer,
    [ProofObj])
-> (Proof
      (Forall "e" (Expr nm val)
       -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
    -> StepArgs
         (Forall "e" (Expr nm val)
          -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
         ([(nm, val)], [val]))
-> TP
     (Proof
        (Forall "e" (Expr nm val)
         -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "e" (Expr nm val)
    -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "e" (Expr nm val)
    -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
-> (MeasureArgs
      (Forall "e" (Expr nm val)
       -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
      m,
    [ProofObj])
-> (Proof
      (Forall "e" (Expr nm val)
       -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
    -> StepArgs
         (Forall "e" (Expr nm val)
          -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
         t)
-> TP
     (Proof
        (Forall "e" (Expr nm val)
         -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool))
sInductWith SMTConfig
cvc5 String
"helper"
               (\(Forall @"e" SExpr nm val
e) (Forall @"env" (Env nm val
env :: Env nm val)) (Forall @"stk" Stack val
stk) ->
                             SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run ((Env nm val, Stack val) -> SBV ([(nm, val)], [val])
forall tup a. Tuple tup a => a -> SBV tup
tuple (Env nm val
env, Stack val
stk)) (SExpr nm val -> SList (Instr nm val)
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SList (Instr nm val)
compile SExpr nm val
e)
                         SBV ([(nm, val)], [val]) -> SBV ([(nm, val)], [val]) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Env nm val, Stack val) -> SBV ([(nm, val)], [val])
forall tup a. Tuple tup a => a -> SBV tup
tuple (Env nm val
env, SBV val -> Stack val -> Stack val
forall a. SymVal a => SBV a -> SList a -> SList a
push (Env nm val -> SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
Env nm val -> SExpr nm val -> SBV val
interpInEnv Env nm val
env SExpr nm val
e) Stack val
stk))
               (\SExpr nm val
e Env nm val
_ Stack val
_  -> SExpr nm val -> SBV Integer
forall nm val.
(SymVal nm, SymVal val) =>
SExpr nm val -> SBV Integer
size SExpr nm val
e, [Proof (Forall "e" (Expr nm val) -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "e" (Expr nm val) -> SBool)
measureNonNeg]) ((Proof
    (Forall "e" (Expr nm val)
     -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
  -> StepArgs
       (Forall "e" (Expr nm val)
        -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
       ([(nm, val)], [val]))
 -> TP
      (Proof
         (Forall "e" (Expr nm val)
          -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)))
-> (Proof
      (Forall "e" (Expr nm val)
       -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
    -> StepArgs
         (Forall "e" (Expr nm val)
          -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
         ([(nm, val)], [val]))
-> TP
     (Proof
        (Forall "e" (Expr nm val)
         -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool))
forall a b. (a -> b) -> a -> b
$
               \Proof
  (Forall "e" (Expr nm val)
   -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
ih SExpr nm val
e Env nm val
env Stack val
stk -> []
                 [SBool]
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [pCase|Expr e of
                      Var nm     -> run (tuple (env, stk)) (compile (sVar nm))
                                 ?? "case Var"
                                 =: run (tuple (env, stk)) [sIPushN nm]
                                 =: tuple (env, push (interpInEnv env (sVar nm)) stk)
                                 =: qed

                      Con v      -> run (tuple (env, stk)) (compile (sCon v))
                                 ?? "case Con"
                                 =: run (tuple (env, stk)) [sIPushV v]
                                 =: tuple (env, push v stk)
                                 =: tuple (env, push (interpInEnv env (sCon v)) stk)
                                 =: qed

                      Sqr a      -> run (tuple (env, stk)) (compile (sSqr a))
                                 ?? "case Sqr"
                                 =: run (tuple (env, stk)) (compile a SL.++ [sIDup, sIMul])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk)) (compile a)) [sIDup, sIMul]
                                 ?? ih `at` (Inst @"e" a, Inst @"env" env, Inst @"stk" stk)
                                 =: let stk' = push (interpInEnv env a) stk
                                 in run (tuple (env, stk')) [sIDup, sIMul]
                                 ?? runTwo `at` (Inst @"es" (tuple (env, stk')), Inst @"i" sIDup, Inst @"j" sIMul)
                                 =: execute (execute (tuple (env, stk')) sIDup) sIMul
                                 =: let stk'' = push (interpInEnv env a) stk'
                                 in execute (tuple (env, stk'')) sIMul
                                 =: tuple (env, push (interpInEnv env a * interpInEnv env a) stk)
                                 =: tuple (env, push (interpInEnv env (sSqr a)) stk)
                                 =: qed

                      Inc a      -> run (tuple (env, stk)) (compile (sInc a))
                                 ?? "case Inc"
                                 =: run (tuple (env, stk)) (compile a SL.++ [sIPushV 1, sIAdd])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk)) (compile a)) [sIPushV 1, sIAdd]
                                 ?? ih `at` (Inst @"e" a, Inst @"env" env, Inst @"stk" stk)
                                 =: let stk' = push (interpInEnv env a) stk
                                 in run (tuple (env, stk')) [sIPushV 1, sIAdd]
                                 ?? runTwo `at` (Inst @"es" (tuple (env, stk')), Inst @"i" (sIPushV 1), Inst @"j" sIAdd)
                                 =: execute (execute (tuple (env, stk')) (sIPushV 1)) sIAdd
                                 =: let stk'' = push 1 stk'
                                 in execute (tuple (env, stk'')) sIAdd
                                 =: tuple (env, push (1 + interpInEnv env a) stk)
                                 =: tuple (env, push (interpInEnv env (sInc a)) stk)
                                 =: qed

                      Add a b    -> run (tuple (env, stk)) (compile (sAdd a b))
                                 ?? "case sAdd"
                                 =: run (tuple (env, stk)) (compile a SL.++ compile b SL.++ [sIAdd])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk)) (compile a)) (compile b SL.++ [sIAdd])
                                 ?? ih `at` (Inst @"e" a, Inst @"env" env, Inst @"stk" stk)
                                 =: let stk' = push (interpInEnv env a) stk
                                 in run (tuple (env, stk')) (compile b SL.++ [sIAdd])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk')) (compile b)) [sIAdd]
                                 ?? ih `at` (Inst @"e" b, Inst @"env" env, Inst @"stk" stk')
                                 =: let stk'' = push (interpInEnv env b) stk'
                                 in run (tuple (env, stk'')) [sIAdd]
                                 ?? runOne `at` (Inst @"es" (tuple (env, stk'')), Inst @"i" sIAdd)
                                 =: execute (tuple (env, stk'')) sIAdd
                                 =: tuple (env, push (interpInEnv env b + interpInEnv env a) stk)
                                 =: tuple (env, push (interpInEnv env a + interpInEnv env b) stk)
                                 =: tuple (env, push (interpInEnv env (sAdd a b)) stk)
                                 =: qed

                      Mul a b    -> run (tuple (env, stk)) (compile (sMul a b))
                                 ?? "case sMul"
                                 =: run (tuple (env, stk)) (compile a SL.++ compile b SL.++ [sIMul])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk)) (compile a)) (compile b SL.++ [sIMul])
                                 ?? ih `at` (Inst @"e" a, Inst @"env" env, Inst @"stk" stk)
                                 =: let stk' = push (interpInEnv env a) stk
                                 in run (tuple (env, stk')) (compile b SL.++ [sIMul])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk')) (compile b)) [sIMul]
                                 ?? ih `at` (Inst @"e" b, Inst @"env" env, Inst @"stk" stk')
                                 =: let stk'' = push (interpInEnv env b) stk'
                                 in run (tuple (env, stk'')) [sIMul]
                                 ?? runOne `at` (Inst @"es" (tuple (env, stk'')), Inst @"i" sIMul)
                                 =: execute (tuple (env, stk'')) sIMul
                                 ?? runMul `at` ( Inst @"a"   (interpInEnv env b)
                                                , Inst @"b"   (interpInEnv env a)
                                                , Inst @"env" env
                                                , Inst @"stk" stk)
                                 =: tuple (env, push (interpInEnv env b * interpInEnv env a) stk)
                                 =: tuple (env, push (interpInEnv env a * interpInEnv env b) stk)
                                 =: tuple (env, push (interpInEnv env (sMul a b)) stk)
                                 =: qed

                      Let nm a b -> run (tuple (env, stk)) (compile (sLet nm a b))
                                 ?? "case Let"
                                 =: run (tuple (env, stk)) (compile a SL.++ [sIBind nm] SL.++ compile b SL.++ [sIForget])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk)) (compile a)) ([sIBind nm] SL.++ compile b SL.++ [sIForget])
                                 ?? ih `at` (Inst @"e" a, Inst @"env" env, Inst @"stk" stk)
                                 =: let stk' = push (interpInEnv env a) stk
                                 in run (tuple (env, stk')) ([sIBind nm] SL.++ compile b SL.++ [sIForget])
                                 ?? runSeq
                                 =: run (run (tuple (env, stk')) [sIBind nm]) (compile b SL.++ [sIForget])
                                 ?? runOne
                                 =: run (execute (tuple (env, stk')) (sIBind nm)) (compile b SL.++ [sIForget])
                                 =: let env' = push (tuple (nm, interpInEnv env a)) env
                                 in run (tuple (env', stk)) (compile b SL.++ [sIForget])
                                 ?? runSeq
                                 =: run (run (tuple (env', stk)) (compile b)) [sIForget]
                                 ?? ih `at` (Inst @"e" b, Inst @"env" env', Inst @"stk" stk)
                                 =: let stk'' = push (interpInEnv env' b) stk
                                 in run (tuple (env', stk'')) [sIForget]
                                 ?? runOne
                                 =: execute (tuple (env', stk'')) sIForget
                                 =: tuple (env, stk'')
                                 =: tuple (env, push (interpInEnv env (sLet nm a b)) stk)
                                 =: qed
                    |]

   -- We can now prove the final correctness theorem, based on the helper.
   String
-> (Forall "expr" (Expr nm val) -> SBool)
-> StepArgs (Forall "expr" (Expr nm val) -> SBool) val
-> TP (Proof (Forall "expr" (Expr nm val) -> SBool))
forall t.
(Proposition (Forall "expr" (Expr nm val) -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "expr" (Expr nm val) -> SBool)
-> StepArgs (Forall "expr" (Expr nm val) -> SBool) t
-> TP (Proof (Forall "expr" (Expr nm val) -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"correctness"
        (\(Forall @"expr" (SExpr nm val
e :: SExpr nm val)) -> SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
compileAndRun SExpr nm val
e SBV val -> SBV val -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
interp SExpr nm val
e) (StepArgs (Forall "expr" (Expr nm val) -> SBool) val
 -> TP (Proof (Forall "expr" (Expr nm val) -> SBool)))
-> StepArgs (Forall "expr" (Expr nm val) -> SBool) val
-> TP (Proof (Forall "expr" (Expr nm val) -> SBool))
forall a b. (a -> b) -> a -> b
$
        \(SExpr nm val
e :: SExpr nm val) -> [] [SBool] -> TPProofRaw (SBV val) -> (SBool, TPProofRaw (SBV val))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
compileAndRun SExpr nm val
e
                                   SBV val -> ChainsTo (SBV val) -> ChainsTo (SBV val)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Stack val -> SBV val
forall val. SymVal val => Stack val -> SBV val
top (SBV ([(nm, val)], [val]) -> Stack val
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
ST.snd (SBV ([(nm, val)], [val])
-> SList (Instr nm val) -> SBV ([(nm, val)], [val])
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
EnvStack nm val -> SList (Instr nm val) -> EnvStack nm val
run ((Env nm val, Stack val) -> SBV ([(nm, val)], [val])
forall tup a. Tuple tup a => a -> SBV tup
tuple ([], [])) (SExpr nm val -> SList (Instr nm val)
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SList (Instr nm val)
compile SExpr nm val
e)))
                                   SBV val -> Proof Bool -> Hinted (SBV val)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "e" (Expr nm val)
   -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
helper Proof
  (Forall "e" (Expr nm val)
   -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
-> IArgs
     (Forall "e" (Expr nm val)
      -> Forall "env" [(nm, val)] -> Forall "stk" [val] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SExpr nm val
e, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" [], forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" [])
                                   TPProofRaw (SBV val)
-> ChainsTo (TPProofRaw (SBV val))
-> ChainsTo (TPProofRaw (SBV val))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Stack val -> SBV val
forall val. SymVal val => Stack val -> SBV val
top (SBV ([(nm, val)], [val]) -> Stack val
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
ST.snd ((Env nm val, Stack val) -> SBV ([(nm, val)], [val])
forall tup a. Tuple tup a => a -> SBV tup
tuple ([] :: Env nm val, SBV val -> Stack val -> Stack val
forall a. SymVal a => SBV a -> SList a -> SList a
push (Env nm val -> SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
Env nm val -> SExpr nm val -> SBV val
interpInEnv [] SExpr nm val
e) [])))
                                   SBV val -> ChainsTo (SBV val) -> ChainsTo (SBV val)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Env nm val -> SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
Env nm val -> SExpr nm val -> SBV val
interpInEnv [] SExpr nm val
e
                                   SBV val -> ChainsTo (SBV val) -> ChainsTo (SBV val)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val, Num (SBV val)) =>
SExpr nm val -> SBV val
interp SExpr nm val
e
                                   SBV val -> ChainsTo (SBV val) -> ChainsTo (SBV val)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV val)
TPProofRaw (SBV val)
forall a. TPProofRaw a
qed