在Haskell中证明"没有腐败"

Question

我在安全关键行业工作,我们的软件项目通常都有安全要求; 我们必须证明该软件具有高度确定性.通常这些都是消极的,例如"不应该比1更频繁地腐败".(我应补充一点,这些要求来自统计系统安全要求).

腐败的一个来源显然是编码错误,我想使用Haskell类型系统来排除这些错误中的至少一些类.像这样的东西:

首先,这是我们的关键数据项,不能被破坏.

newtype Critical = Critical String

现在我想将这个项目存储在其他一些结构中.

data Foo = Foo Integer Critical
data Bar = Bar String Critical

现在我想编写一个从Foo到Bar的转换函数,保证不会弄乱关键数据.

goodConvert, badConvert :: Foo -> Bar

goodConvert (Foo n c) = Bar (show n) c

badConvert (Foo n (Critical s)) = Bar (show n) (Critical $ "Bzzt - " ++ s)

我希望"goodConvert"键入check,但"badConvert"键入失败类型检查.

显然,我可以小心地不将Critical构造函数导入到进行转换的模块中.但是如果我能在类型中表达这个属性会好得多,因为那时我可以编写保证保留这个属性的函数.

我尝试在各个地方添加幻像类型和"forall",但这没有用.

可行的一件事是不导出Critical构造函数,然后具有

mkCritical :: String -> IO Critical

由于创建这些关键数据项的唯一位置是在输入函数中,这是有道理的.但我更喜欢更优雅和通用的解决方案.

编辑

在评论中,FUZxxl建议看一下Safe Haskell.这看起来是最好的解决方案.而不是像我原来想要的那样在类型级别添加"无损坏"修饰符,看起来你可以在模块级别执行它,如下所示:

1:创建一个模块"Critical",导出Critical数据类型的所有功能,包括其构造函数.通过在标题中添加"{ - #LANGUAGE Unsafe# - }"将此模块标记为"不安全".

2:创建一个"SafeCritical"模块,重新导出除构造函数和可能用于破坏临界值的任何其他函数之外的所有内容.将此模块标记为"值得信赖".

3:将处理临界值所需的任何模块标记为"安全"而不会损坏.然后使用它来演示导入为"safe"的任何函数都不会导致损坏到Critical值.

这将留下较少的代码,例如解析关键值的输入代码,需要进一步验证.我们无法消除此代码,但减少需要详细验证的数量仍然是一个重大的胜利.

该方法基于以下事实:除非函数返回,否则函数不能创建新值.如果一个函数只获得一个临界值(如上面的"转换"函数),那么它就是唯一可以返回的值.

当函数具有两个或更多相同类型的临界值时,问题就会出现更难的变化; 它必须保证不要混淆它们.例如,

swapFooBar :: (Foo, Bar) -> (Bar, Foo)
swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2)

然而,这可以通过对包含的数据结构给予相同的处理来处理.

Answer 1

您可以使用参数化来获得中途

data Foo c = Foo Integer c
data Bar c = Bar String c

goodConvert :: Foo c -> Bar c
goodConvert (Foo n c) = Bar (show n) c

由于c是一个无约束的类型变量,您知道该函数goodConvert无法知道任何内容c,因此无法构造该类型的不同值.它必须使用输入中提供的那个.

好吧,差不多.底值允许您打破此保证.但是,您至少知道如果您尝试使用"损坏"值,则会导致异常(或非终止).

badConvert :: Foo c -> Bar c
badConvert (Foo n c) = Bar (show n) undefined

Answer 2

虽然hammar的解决方案非常出色,我通常建议使用智能构造函数/不导出构造函数,但今天我决定尝试在Coq校对助手中解决这个问题并提取到Haskell.

做记录!我不太熟悉Coq /提取.有些人在证明和提取Haskell代码方面做得很好,所以请向他们寻找高质量的例子 - 我只是在玩弄!

首先,我们要定义您的数据类型.在Coq中,这看起来很像Haskell GADT:

Require Import String.
Require Import ZArith.

Inductive Critical :=
  Crit : string -> Critical.

Inductive FooT :=
  Foo : Z -> Critical -> FooT.

Inductive BarT :=
  Bar : string -> Critical -> BarT.

可以将这些Inductive行Inductive FooT := Foo : ... .视为数据类型声明:data FooT = Foo Integer Critical

为了便于使用,让我们获取一些字段访问器:

Definition critF f := match f with Foo _ c => c end.
Definition critB b := match b with Bar _ c => c end.

由于Coq没有定义很多"show"样式函数,我将使用占位符来显示整数.

Definition ascii_of_Z (z : Z) : string := EmptyString. (* FIXME *)

现在我们已经掌握了基础,让我们定义goodConvert功能!

Definition goodConvert (foo : FooT) : BarT :=
  match foo with
    Foo n c => Bar (ascii_of_Z n) c
  end.

这一切都很明显 - 它是你的转换函数,但在Coq中使用caselike语句而不是顶级模式匹配.但是我们怎么知道这个函数实际上是要保持不变量呢？我们证明了!

Lemma convertIsGood : forall (f : FooT) (b : BarT),
  goodConvert f = b -> critF f = critB b.
Proof.
  intros. 
  destruct f. destruct b.
  unfold goodConvert in H. simpl.
  inversion H. reflexivity.
Qed.

这就是说,如果转换f结果,b那么关键字段f必须与关键字段相同b(假设一些小问题,例如你不搞乱字段访问器实现).

现在让我们把它提取到Haskell!

Extraction Language Haskell.
Extract Constant ascii_of_Z => "Prelude.show".  (* obviously, all sorts of unsafe and incorrect behavior can be introduced by your extraction *)
Extract Inductive string => "Prelude.String" ["[]" ":"]. Print positive.
Extract Inductive positive => "Prelude.Integer" ["`Data.Bits.shiftL` 1 + 1" "`Data.Bits.shiftL` 1" "1"].
Extract Inductive Z => "Prelude.Integer" ["0" "" ""].

Extraction "so.hs" goodConvert critF critB.

生产:

module So where

import qualified Prelude

data Bool =
   True
 | False

data Ascii0 =
   Ascii Bool Bool Bool Bool Bool Bool Bool Bool

type Critical =
  Prelude.String
  -- singleton inductive, whose constructor was crit

data FooT =
   Foo Prelude.Integer Critical

data BarT =
   Bar Prelude.String Critical

critF :: FooT -> Critical
critF f =
  case f of {
   Foo z c -> c}

critB :: BarT -> Critical
critB b =
  case b of {
   Bar s c -> c}

ascii_of_Z :: Prelude.Integer -> Prelude.String
ascii_of_Z z =
  []

goodConvert :: FooT -> BarT
goodConvert foo =
  case foo of {
   Foo n c -> Bar (ascii_of_Z n) c}

我们可以运行吗？它有用吗？

> critB $ goodConvert (Foo 32 "hi")
"hi"

大!如果有人对我有任何建议,即使这是一个"答案",我也全都听见了.我不知道如何删除的东西死代码像Ascii0或者Bool,更何况让好戏实例.如果有人好奇,我认为如果我使用a Record而不是a,字段名称可以自动完成Inductive,但这可能会使这个帖子在语法上更加丑陋.