Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.TP.VM

Contents

Language
Environment and the stack
Interpretation
Virtual machine
Compilation
Correctness of the compiler

Description

Correctness of a simple interpreter vs virtual-machine interpretation of a language.

Synopsis

data Expr nm val
- = Var nm
- | Con val
- | Sqr (Expr nm val)
- | Inc (Expr nm val)
- | Add (Expr nm val) (Expr nm val)
- | Mul (Expr nm val) (Expr nm val)
- | Let nm (Expr nm val) (Expr nm val)
type SExpr nm val = SBV (Expr nm val)
size :: (SymVal nm, SymVal val) => SExpr nm val -> SInteger
type Env nm val = SList (nm, val)
type Stack val = SList val
interpInEnv :: (SymVal nm, SymVal val, Num (SBV val)) => Env nm val -> SExpr nm val -> SBV val
interp :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val
data Instr nm val
- = IPushN nm
- | IPushV val
- | IDup
- | IAdd
- | IMul
- | IBind nm
- | IForget
type SInstr nm val = SBV (Instr nm val)
compile :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SList (Instr nm val)
compileAndRun :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val
correctness :: (SymVal nm, SymVal val, Num (SBV val)) => TP (Proof (Forall "expr" (Expr nm val) -> SBool))

Language

data Expr nm val Source #

Basic expression language.

Constructors

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

Instances

Instances details

Arbitrary (Expr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods arbitrary :: Gen (Expr nm val) # shrink :: Expr nm val -> [Expr nm val] #
(SymVal nm, SymVal val) => SymVal (Expr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV (Expr nm val)) Source # mkSymValInit :: State -> SBV (Expr nm val) -> IO () Source # literal :: Expr nm val -> SBV (Expr nm val) Source # fromCV :: CV -> Expr nm val Source # isConcretely :: SBV (Expr nm val) -> (Expr nm val -> Bool) -> Bool Source # minMaxBound :: Maybe (Expr nm val, Expr nm val) Source # free :: MonadSymbolic m => String -> m (SBV (Expr nm val)) Source # free_ :: MonadSymbolic m => m (SBV (Expr nm val)) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV (Expr nm val)] Source # symbolic :: MonadSymbolic m => String -> m (SBV (Expr nm val)) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV (Expr nm val)] Source # unliteral :: SBV (Expr nm val) -> Maybe (Expr nm val) Source # unlitCV :: SBV (Expr nm val) -> Maybe (Kind, CVal) Source # isConcrete :: SBV (Expr nm val) -> Bool Source # isSymbolic :: SBV (Expr nm val) -> Bool Source #
(HasKind nm, HasKind val) => HasKind (Expr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods kindOf :: Expr nm val -> Kind Source # hasSign :: Expr nm val -> Bool Source # intSizeOf :: Expr nm val -> Int Source # isBoolean :: Expr nm val -> Bool Source # isBounded :: Expr nm val -> Bool Source # isReal :: Expr nm val -> Bool Source # isFloat :: Expr nm val -> Bool Source # isDouble :: Expr nm val -> Bool Source # isRational :: Expr nm val -> Bool Source # isFP :: Expr nm val -> Bool Source # isUnbounded :: Expr nm val -> Bool Source # isADT :: Expr nm val -> Bool Source # isChar :: Expr nm val -> Bool Source # isString :: Expr nm val -> Bool Source # isList :: Expr nm val -> Bool Source # isSet :: Expr nm val -> Bool Source # isTuple :: Expr nm val -> Bool Source # isArray :: Expr nm val -> Bool Source # isRoundingMode :: Expr nm val -> Bool Source # isUninterpreted :: Expr nm val -> Bool Source # showType :: Expr nm val -> String Source #
(SymVal nm, SymVal val) => HasInductionSchema (Forall ta (Expr nm val) -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Expr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

type SExpr nm val = SBV (Expr nm val) Source #

Symbolic version of the type Expr.

size :: (SymVal nm, SymVal val) => SExpr nm val -> SInteger Source #

Size of an expression. Used in strong induction.

Environment and the stack

type Env nm val = SList (nm, val) Source #

Environment, binding names to values

type Stack val = SList val Source #

Stack of values.

Interpretation

interpInEnv :: (SymVal nm, SymVal val, Num (SBV val)) => Env nm val -> SExpr nm val -> SBV val Source #

Interpreter, in the usual functional style, taking an arbitrary environment.

interp :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val Source #

Interpret starting from empty environment.

Virtual machine

data Instr nm val Source #

Instructions

Constructors

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

Instances

Instances details

Arbitrary (Instr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods arbitrary :: Gen (Instr nm val) # shrink :: Instr nm val -> [Instr nm val] #
(SymVal nm, SymVal val) => SymVal (Instr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV (Instr nm val)) Source # mkSymValInit :: State -> SBV (Instr nm val) -> IO () Source # literal :: Instr nm val -> SBV (Instr nm val) Source # fromCV :: CV -> Instr nm val Source # isConcretely :: SBV (Instr nm val) -> (Instr nm val -> Bool) -> Bool Source # minMaxBound :: Maybe (Instr nm val, Instr nm val) Source # free :: MonadSymbolic m => String -> m (SBV (Instr nm val)) Source # free_ :: MonadSymbolic m => m (SBV (Instr nm val)) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV (Instr nm val)] Source # symbolic :: MonadSymbolic m => String -> m (SBV (Instr nm val)) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV (Instr nm val)] Source # unliteral :: SBV (Instr nm val) -> Maybe (Instr nm val) Source # unlitCV :: SBV (Instr nm val) -> Maybe (Kind, CVal) Source # isConcrete :: SBV (Instr nm val) -> Bool Source # isSymbolic :: SBV (Instr nm val) -> Bool Source #
(HasKind nm, HasKind val) => HasKind (Instr nm val) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods kindOf :: Instr nm val -> Kind Source # hasSign :: Instr nm val -> Bool Source # intSizeOf :: Instr nm val -> Int Source # isBoolean :: Instr nm val -> Bool Source # isBounded :: Instr nm val -> Bool Source # isReal :: Instr nm val -> Bool Source # isFloat :: Instr nm val -> Bool Source # isDouble :: Instr nm val -> Bool Source # isRational :: Instr nm val -> Bool Source # isFP :: Instr nm val -> Bool Source # isUnbounded :: Instr nm val -> Bool Source # isADT :: Instr nm val -> Bool Source # isChar :: Instr nm val -> Bool Source # isString :: Instr nm val -> Bool Source # isList :: Instr nm val -> Bool Source # isSet :: Instr nm val -> Bool Source # isTuple :: Instr nm val -> Bool Source # isArray :: Instr nm val -> Bool Source # isRoundingMode :: Instr nm val -> Bool Source # isUninterpreted :: Instr nm val -> Bool Source # showType :: Instr nm val -> String Source #
(SymVal nm, SymVal val) => HasInductionSchema (Forall ta (Instr nm val) -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal nm, SymVal val, SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.VM Methods inductionSchema :: (Forall ta (Instr nm val) -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

type SInstr nm val = SBV (Instr nm val) Source #

Symbolic version of the type Instr.

Compilation

compile :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SList (Instr nm val) Source #

Convert an expression to a sequence of instructions for our virtual machine.

compileAndRun :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val Source #

Compile and run an expression.

Correctness of the compiler

correctness :: (SymVal nm, SymVal val, Num (SBV val)) => TP (Proof (Forall "expr" (Expr nm val) -> SBool)) Source #

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