在Haskell中证明“没有腐败”-Java 学习之路

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

腐败的一个来源显然是编码错误，我想使用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

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

Edit

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

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

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

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

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

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

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

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

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

3 回答

3
您可以使用参数化来获得中途
```
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
```
回复于 2024-05-05T20:24:45+08:00

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

做记录！我不太熟悉Coq /提取 . 有些人已经通过证明和提取Haskell代码完成了good work，所以请向他们寻找质量示例 - 我只是玩弄！

首先，我们要定义您的数据类型 . 在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.

那个's all fairly obvious - it'是你的转换函数但是在Coq中使用 case like语句而不是顶级模式匹配 . 但是我们怎么知道这个函数实际上是要维持不变量呢？我们证明了！

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"

大！如果有人对我有建议，即使这是"answer"，我也不知道如何删除像 Ascii0 或 Bool 这样的死代码，更不用说制作好的节目实例了 . 如果有人好奇，我认为如果我使用 Record 而不是 Inductive ，字段名称可以自动完成，但这可能会使这个帖子在语法上更加丑陋 .

回复于 2024-05-05T20:24:45+08:00

19
我认为隐藏构造函数的解决方案是惯用的 . 您可以导出两个功能：
```
mkCritical :: String -> D Critical
extract :: Critical -> String
```
其中 D 是trivial monad，或任何其他 . 在某些时候创建 Critical 类型对象的任何函数都标有 D . 没有 D 的函数可以从 Critical 对象中提取数据，但不能创建新对象 .

或者：
```
data C a = C a Critical
modify :: (a -> String -> b) -> C a -> C b
modify f (C x (Critical y)) = C (f x y) (Critical y)
```
如果你不导出构造函数 C ，只有 modify ，你可以写：
```
goodConvert :: C Int -> C String
goodConvert = modify (\(a, _) -> show a)
```
但 badConvert 是不可能写的 .
回复于 2024-05-05T20:24:45+08:00

在Haskell中证明“没有腐败”

3 回答

相关问题