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

     -- * 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 nm                             -- ^ Variables
                 | Con val                            -- ^ Constants
                 | Sqr (Expr nm val)                  -- ^ Squaring
                 | Inc (Expr nm val)                  -- ^ Increment
                 | Add (Expr nm val) (Expr nm val)    -- ^ Addition
                 | Mul (Expr nm val) (Expr nm val)    -- ^ Multiplication
                 | Let nm (Expr nm val) (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 nm   -- ^ Push the value of nm from the environment on to the stack
                  | IPushV 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 val  -> (env, push val 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)
|- [(SBool, TPProofRaw (SBV ([(nm, val)], [val])))]
-> TPProofRaw (SBV ([(nm, val)], [val]))
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SExpr nm val -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isVar SExpr nm val
e SBool
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let nm :: SBV nm
nm = SExpr nm val -> SBV nm
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV nm
getVar_1 SExpr nm val
e
                                     in 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 (SBV nm -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Expr nm val)
sVar SBV nm
nm))
                                     SBV ([(nm, val)], [val])
-> String -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case Var"
                                     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 ((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)) [SBV nm -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Instr nm val)
sIPushN SBV nm
nm]
                                     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
=: (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 (SBV nm -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Expr nm val)
sVar SBV nm
nm)) Stack val
stk)
                                     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

                          , SExpr nm val -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isCon SExpr nm val
e SBool
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let v :: SBV val
v = SExpr nm val -> SBV val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV val
getCon_1 SExpr nm val
e
                                     in 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 (SBV val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Expr nm val)
sCon SBV val
v))
                                     SBV ([(nm, val)], [val])
-> String -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case Con"
                                     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 ((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)) [SBV val -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Instr nm val)
sIPushV SBV val
v]
                                     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
=: (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
v Stack val
stk)
                                     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
=: (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 (SBV val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Expr nm val)
sCon SBV val
v)) Stack val
stk)
                                     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

                          , SExpr nm val -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isSqr SExpr nm val
e SBool
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let a :: SExpr nm val
a = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getSqr_1 SExpr nm val
e
                                     in 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 -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
sSqr SExpr nm val
a))
                                     SBV ([(nm, val)], [val])
-> String -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case Sqr"
                                     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 ((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
a SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIDup, Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
a)) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIDup, Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk)
                                     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
=: let stk' :: Stack val
stk' = 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
a) Stack val
stk
                                     in 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')) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIDup, Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
runTwo Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
-> IArgs
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm 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 @"es" ((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')), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIDup, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"j" SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul)
                                     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])
-> 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 ((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')) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIDup) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul
                                     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
=: let stk'' :: Stack val
stk'' = 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
a) Stack val
stk'
                                     in 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, Stack val
stk'')) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul
                                     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
=: (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
a SBV val -> SBV val -> SBV val
forall a. Num a => a -> a -> 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 Env nm val
env SExpr nm val
a) Stack val
stk)
                                     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
=: (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 -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
sSqr SExpr nm val
a)) Stack val
stk)
                                     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

                          , SExpr nm val -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isInc SExpr nm val
e SBool
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let a :: SExpr nm val
a = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getInc_1 SExpr nm val
e
                                     in 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 -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
sInc SExpr nm val
a))
                                     SBV ([(nm, val)], [val])
-> String -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case Inc"
                                     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 ((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
a SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [SBV val -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Instr nm val)
sIPushV SBV val
1, Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
a)) [SBV val -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Instr nm val)
sIPushV SBV val
1, Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk)
                                     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
=: let stk' :: Stack val
stk' = 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
a) Stack val
stk
                                     in 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')) [SBV val -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Instr nm val)
sIPushV SBV val
1, Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
runTwo Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm val) -> SBool)
-> IArgs
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm val) -> Forall "j" (Instr nm 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 @"es" ((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')), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" (SBV val -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Instr nm val)
sIPushV SBV val
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"j" SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd)
                                     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])
-> 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 ((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')) (SBV val -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV val -> SBV (Instr nm val)
sIPushV SBV val
1)) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd
                                     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
=: let stk'' :: Stack val
stk'' = SBV val -> Stack val -> Stack val
forall a. SymVal a => SBV a -> SList a -> SList a
push SBV val
1 Stack val
stk'
                                     in 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, Stack val
stk'')) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd
                                     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
=: (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
1 SBV val -> SBV val -> SBV val
forall a. Num a => a -> a -> 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 Env nm val
env SExpr nm val
a) Stack val
stk)
                                     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
=: (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 -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
sInc SExpr nm val
a)) Stack val
stk)
                                     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

                          , SExpr nm val -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isAdd SExpr nm val
e SBool
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let a :: SExpr nm val
a = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getAdd_1 SExpr nm val
e
                                            b :: SExpr nm val
b = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getAdd_2 SExpr nm val
e
                                     in 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 -> SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
sAdd SExpr nm val
a SExpr nm val
b))
                                     SBV ([(nm, val)], [val])
-> String -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case sAdd"
                                     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 ((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
a SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
a)) (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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd])
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk)
                                     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
=: let stk' :: Stack val
stk' = 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
a) Stack val
stk
                                     in 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
b)) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk')
                                     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
=: let stk'' :: Stack val
stk'' = 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
b) Stack val
stk'
                                     in 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'')) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> SBool)
runOne Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> SBool)
-> IArgs
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm 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 @"es" ((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'')), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd)
                                     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])
-> 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, Stack val
stk'')) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIAdd
                                     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
=: (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
b SBV val -> SBV val -> SBV val
forall a. Num a => a -> a -> 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 Env nm val
env SExpr nm val
a) Stack val
stk)
                                     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
=: (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
a SBV val -> SBV val -> SBV val
forall a. Num a => a -> a -> 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 Env nm val
env SExpr nm val
b) Stack val
stk)
                                     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
=: (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 -> SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
sAdd SExpr nm val
a SExpr nm val
b)) Stack val
stk)
                                     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

                          , SExpr nm val -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isMul SExpr nm val
e SBool
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let a :: SExpr nm val
a = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getMul_1 SExpr nm val
e
                                            b :: SExpr nm val
b = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getMul_2 SExpr nm val
e
                                     in 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 -> SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
sMul SExpr nm val
a SExpr nm val
b))
                                     SBV ([(nm, val)], [val])
-> String -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case sMul"
                                     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 ((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
a SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
a)) (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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul])
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk)
                                     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
=: let stk' :: Stack val
stk' = 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
a) Stack val
stk
                                     in 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
b)) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk')
                                     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
=: let stk'' :: Stack val
stk'' = 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
b) Stack val
stk'
                                     in 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'')) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> SBool)
runOne Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> SBool)
-> IArgs
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm 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 @"es" ((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'')), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul)
                                     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])
-> 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, Stack val
stk'')) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIMul
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "a" val
   -> Forall "b" val
   -> Forall "env" [(nm, val)]
   -> Forall "stk" [val]
   -> SBool)
runMul Proof
  (Forall "a" val
   -> Forall "b" val
   -> Forall "env" [(nm, val)]
   -> Forall "stk" [val]
   -> SBool)
-> IArgs
     (Forall "a" val
      -> Forall "b" 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 @"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 Env nm val
env SExpr nm val
b)
                                                    , forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"b"   (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
a)
                                                    , forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env
                                                    , forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk)
                                     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
=: (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
b SBV val -> SBV val -> SBV val
forall a. Num a => a -> a -> 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 Env nm val
env SExpr nm val
a) Stack val
stk)
                                     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
=: (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
a SBV val -> SBV val -> SBV val
forall a. Num a => a -> a -> 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 Env nm val
env SExpr nm val
b) Stack val
stk)
                                     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
=: (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 -> SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
sMul SExpr nm val
a SExpr nm val
b)) Stack val
stk)
                                     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

                          , SExpr nm val -> SBool
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBool
isLet SExpr nm val
e SBool
-> TPProofRaw (SBV ([(nm, val)], [val]))
-> (SBool, TPProofRaw (SBV ([(nm, val)], [val])))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> let nm :: SBV nm
nm = SExpr nm val -> SBV nm
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV nm
getLet_1 SExpr nm val
e
                                            a :: SExpr nm val
a  = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getLet_2 SExpr nm val
e
                                            b :: SExpr nm val
b  = SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV (Expr nm val) -> SBV (Expr nm val)
getLet_3 SExpr nm val
e
                                     in 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 (SBV nm -> SExpr nm val -> SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm
-> SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
sLet SBV nm
nm SExpr nm val
a SExpr nm val
b))
                                     SBV ([(nm, val)], [val])
-> String -> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case Let"
                                     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 ((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
a SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [SBV nm -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Instr nm val)
sIBind SBV nm
nm] SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
a)) ([SBV nm -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Instr nm val)
sIBind SBV nm
nm] SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget])
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk)
                                     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
=: let stk' :: Stack val
stk' = 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
a) Stack val
stk
                                     in 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')) ([SBV nm -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Instr nm val)
sIBind SBV nm
nm] SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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')) [SBV nm -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Instr nm val)
sIBind SBV nm
nm]) (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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm val) -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> SBool)
runOne
                                     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])
-> 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, Stack val
stk')) (SBV nm -> SBV (Instr nm val)
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm -> SBV (Instr nm val)
sIBind SBV nm
nm)) (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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget])
                                     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
=: let env' :: Env nm val
env' = SBV (nm, val) -> Env nm val -> Env nm val
forall a. SymVal a => SBV a -> SList a -> SList a
push ((SBV nm, SBV val) -> SBV (nm, val)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV nm
nm, 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
a)) Env nm val
env
                                     in 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
b SList (Instr nm val)
-> SList (Instr nm val) -> SList (Instr nm val)
forall a. SymVal a => SList a -> SList a -> SList a
SL.++ [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget])
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "xs" [Instr nm val]
      -> Forall "ys" [Instr nm val]
      -> Forall "es" ([(nm, val)], [val])
      -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [Instr nm val]
   -> Forall "ys" [Instr nm val]
   -> Forall "es" ([(nm, val)], [val])
   -> SBool)
runSeq
                                     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 ((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
b)) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget]
                                     SBV ([(nm, val)], [val])
-> Proof Bool -> Hinted (SBV ([(nm, val)], [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)
ih 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
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"env" Env nm val
env', forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"stk" Stack val
stk)
                                     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
=: let stk'' :: Stack val
stk'' = 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
b) Stack val
stk
                                     in 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'')) [Item (SList (Instr nm val))
SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget]
                                     SBV ([(nm, val)], [val])
-> Proof
     (Forall "es" ([(nm, val)], [val])
      -> Forall "i" (Instr nm val) -> SBool)
-> Hinted (SBV ([(nm, val)], [val]))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "es" ([(nm, val)], [val])
   -> Forall "i" (Instr nm val) -> SBool)
runOne
                                     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])
-> 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', Stack val
stk'')) SBV (Instr nm val)
forall nm val. (SymVal nm, SymVal val) => SBV (Instr nm val)
sIForget
                                     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
=: (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'')
                                     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
=: (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 (SBV nm -> SExpr nm val -> SExpr nm val -> SExpr nm val
forall nm val.
(SymVal nm, SymVal val) =>
SBV nm
-> SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val)
sLet SBV nm
nm SExpr nm val
a SExpr nm val
b)) Stack val
stk)
                                     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
                          ]

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