Как использовать Data.SBV для правильной реализации стековой машины?

Question

Грэм Хаттон во 2-м издании " Программирование на Haskell" посвящает последние две главы теме реализации AST на основе стековых машин. И в заключение он показывает, как получить правильную реализацию этой машины из семантической модели AST.

Я пытаюсь заручиться помощью Data.SBV в этом происхождении и терпит неудачу.

И я надеюсь, что кто-нибудь поможет мне понять, что я:

1. Просить то, что Data.SBV не могу, или
2. Спрашивая Data.SBVна что-то он может, но спрашивает неправильно.

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

Лучшим вариантом использования SBV и SMT для решения такого рода проблем является на самом деле сказать, что addфункция есть, а затем доказать, что некоторая данная программа правильно "скомпилирована" с использованием стратегии Хаттона. Обратите внимание, что я прямо говорю "заданную" программу: также было бы очень сложно смоделировать и доказать это для произвольной программы, но вы можете сделать это довольно легко для данной фиксированной программы. Если вы заинтересованы в доказательстве соответствия для произвольных программ, вам действительно стоит обратить внимание на такие средства доказательства теорем, как Isabelle, Coq, 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 и о том, как их можно использовать в Haskell через SBV.

Синтез программ - это активная область исследований с множеством нестандартных методов и инструментов. Использование 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 обычно используются на практике.)