Основная проблема заключается в том, что вы смешиваете логики последовательностей SMTLib c и квантификаторы. И проблема оказывается слишком сложной для решения SMT. Подобный синтез функций действительно возможен, если вы ограничиваете себя основами c логики. (Битвекторы, целые числа, вещественные числа.) Но добавление последовательностей в микс помещает его в неразрешимый фрагмент.
Это не означает, что 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, а затем докажите, что какая-то программа правильно «скомпилирована» с использованием стратегии Хаттона. Обратите внимание, что я явно говорю «данная» программа: было бы очень сложно смоделировать и доказать это для произвольной программы, но вы можете сделать это довольно легко для данной фиксированной программы. Если вы заинтересованы в проверке соответствия для произвольных программ, вам действительно следует обратить внимание на теоремовщиков, таких как Изабель, Coq, ACL2 и др. c .; которая может иметь дело с индукцией, техникой доказательства, которая вам, несомненно, понадобится для решения подобных проблем. Обратите внимание, что 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 обычно используются на практике.)