如何使用Data.SBV帮助导出正确的堆栈机器实现？

Question

格雷厄姆·赫顿( Graham )在Haskell的第二版编程中，花了最后2章讨论基于堆栈机器的AST实现问题。最后，他展示了如何从AST的语义模型推导出该机器的正确实现。

我正试图在派生过程中寻求Data.SBV 的帮助，但是失败了.

我希望有人能帮我理解我是不是：

1. 要求Data.SBV不能做的事情，或者
2. 要求Data.SBV做它能做的事情，但是请
3. 去做

-- test/sbv-stack.lhs - Data.SBV assisted stack machine implementation derivation.

{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import qualified Data.SBV.List as L
import           Data.SBV.List ((.:), (.++))  -- Since they don't collide w/ any existing list functions.

-- AST Definition
data Exp = Val SWord8
         | Sum Exp Exp

-- Our "Meaning" Function
eval :: Exp -> SWord8
eval (Val x)   = x
eval (Sum x y) = eval x + eval y

type Stack  = SList Word8

-- Our "Operational" Definition.
--
-- This function attempts to implement the *specification* provided by our
-- "meaning" function, above, in a way that is more conducive to
-- implementation in our available (and, perhaps, quite primitive)
-- computational machinery.
--
-- Note that we've (temporarily) assumed that this machinery will consist
-- of some form of *stack-based computation engine* (because we're
-- following Hutton's example).
--
-- Note that we give the *specification* of the function in the first
-- (commented out) line of the definition. The derivation of the actual
-- correct definition from this specification is detailed in Ch. 17 of
-- Hutton's book.
eval' :: Exp -> Stack -> Stack
-- eval' e s = eval e : s         -- our "specification"
eval' (Val n) s = push n s        -- We're defining this one manually.
 where
  push :: SWord8 -> Stack -> Stack
  push n s = n .: s
eval' (Sum x y) s = add (eval' y (eval' x s))
 where
  add :: Stack -> Stack
  add = uninterpret "add" s       -- This is the function we're asking to be derived.

-- Now, let's just ask SBV to "solve" our specification of `eval'`:
spec :: Goal
spec = do x :: SWord8 <- forall "x"
          y :: SWord8 <- forall "y"
          -- Our spec., from above, specialized to the `Sum` case:
          constrain $ eval' (Sum (Val x) (Val y)) L.nil .== eval (Sum (Val x) (Val y)) .: L.nil

我们得到：

λ> :l test/sbv-stack.lhs
[1 of 1] Compiling Main             ( test/sbv-stack.lhs, interpreted )
Ok, one module loaded.
Collecting type info for 1 module(s) ... 
λ> sat spec
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)

发生了什么？!

那么，也许，要求SBV来解决除谓词(即- a -> Bool)之外的任何问题都是无效的吗？

Answer 1

这里的基本问题是，您正在混合SMTLib的序列逻辑和量词。这个问题对SMT解决者来说太难了。如果你把自己限制在基本逻辑上，这种函数的合成是可能的。(位向量、整数、实数)但是把序列加到混合物中就会把它变成无法分辨的片段。

这并不意味着z3不能合成您的add函数。也许未来的版本可能能够处理它。但在这一点上，你要听命于试探法。要了解原因，请注意，您要求求解者综合以下定义：

        add :: Stack -> Stack
        add s = v .: s''
          where (a, s')  = L.uncons s
                (b, s'') = L.uncons s'
                v        = a + b

虽然这看起来相当天真和简单，但它需要超出z3当前能力的功能。一般来说，z3目前可以合成只对具体元素进行有限选择的函数。但是，如果输出依赖于每个输入选择的输入，则无法做到这一点。(把它看作一个生成引擎的案例分析:它可以使一个函数将某些输入映射到其他输入，但不能确定是否应该增加一些东西，或者必须添加两件东西。这是从有限模型发现理论的工作中得出的，远远超出了这个答案的范围！详见此处：https://arxiv.org/abs/1706.00096)

解决这类问题的一个更好的用例是告诉它add函数是什么，然后用Hutton的策略证明给出的程序是正确的“编译”。请注意，我明确地说的是“给定”程序:对于任意程序来说，建模和证明这一点也是非常困难的，但是对于给定的固定程序，您可以很容易地做到这一点。如果你对证明任意程序的对应感兴趣，你真的应该看看定理证明，比如伊莎贝尔，柯克，ACL2等，它可以处理归纳，这是你毫无疑问需要的证明技巧。请注意，SMT解决程序一般不能执行归纳。(您可以使用电子匹配来模拟一些类似于证明的归纳，但它充其量不过是一种传说，而且通常是不可维护的。)

下面是您的示例，编码以证明\x -> \y -> x + y程序在引用语义方面“正确地”编译和执行：

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import qualified Data.SBV.List as L
import           Data.SBV.List ((.:))

-- AST Definition
data Exp = Val SWord8
         | Sum Exp Exp

-- Our "Meaning" Function
eval :: Exp -> SWord8
eval (Val x)   = x
eval (Sum x y) = eval x + eval y

-- Evaluation by "execution"
type Stack  = SList Word8

run :: Exp -> SWord8
run e = L.head (eval' e L.nil)
  where eval' :: Exp -> Stack -> Stack
        eval' (Val n)   s = n .: s
        eval' (Sum x y) s = add (eval' y (eval' x s))

        add :: Stack -> Stack
        add s = v .: s''
          where (a, s')  = L.uncons s
                (b, s'') = L.uncons s'
                v        = a + b

correct :: IO ThmResult
correct = prove $ do x :: SWord8 <- forall "x"
                     y :: SWord8 <- forall "y"


                     let pgm = Sum (Val x) (Val y)

                         spec    = eval pgm
                         machine = run  pgm

                     return $ spec .== machine

当我运行这个时，我得到：

*Main> correct
Q.E.D.

证据几乎不需要花时间。您可以通过添加其他运算符、绑定表单、函数调用和整个工作(如果您愿意)来轻松地扩展这一点。只要你坚持一个固定的“程序”进行验证，它就应该工作得很好。

如果您犯了一个错误，假设通过减法来定义add (将其最后一行修改为就绪v = a - b)，您将得到：

*Main> correct
Falsifiable. Counter-example:
  x = 32 :: Word8
  y =  0 :: Word8

我希望这能给出SMT解决程序当前的功能，以及如何通过SBV在Haskell中使用它们。

程序综合是一个活跃的研究领域，有许多定制的技术和工具。一次开箱即用的SMT解算器不会让你到达那里.但是，如果您确实在Haskell中构建了这样一个自定义系统，则可以使用SBV访问底层SMT解决程序，以解决过程中必须处理的许多约束。

(旁白:一个扩展的示例，在精神上相似，但目标不同，随SBV包：https://hackage.haskell.org/package/sbv-8.5/docs/Documentation-SBV-Examples-Strings-SQLInjection.html一起提供。此程序演示如何使用SBV和SMT解决程序查找理想化SQL实现中的SQL注入漏洞。这可能会在这里引起一些兴趣，并将与SMT求解器在实践中的使用方式更加一致。)