lemmafit-dafny

分类: 数据与AI | 上传者: midspiral | 下载: 0 | 版本: v1.0（最新）

Dafny 代码模式和 lemmafit 应用程序参考。在编写或编辑 .dfy 文件、定义状态机（Model、Action、Inv、Init、Step）或 Dafny 验证失败且需要修复错误时使用。涵盖 AppCore 模块模式和常见错误。

更新日志: Source: GitHub https://github.com/midspiral/lemmafit

目录结构

当前层级: tree/main/skills/lemmafit-dafny/

📄 SKILL.md 2.8 KB

SKILL.md

---
name: lemmafit-dafny
description: Dafny code patterns and reference for lemmafit apps. Use when writing or editing .dfy files, defining state machines (Model, Action, Inv, Init, Step), or when Dafny verification fails and you need to fix errors. Covers the AppCore module pattern and common mistakes.
---

# Lemmafit Dafny

## When to Write Code in Dafny
- ALL `verifiable:true` entries in the spec MUST be written in Dafny (do not write verifiable code directly in JavaScript or TypeScript)

## Dafny Pattern Example

Given the `Replay` kernel, a simple counter app with inherited undo/redo could be written like this

```dafny
include "Replay.dfy"

module CounterDomain refines Domain {
  // The model is the state of your application
  type Model = int

  // Actions are the ways the state can change
  datatype Action = Inc | Dec

  // Invariant: what must always be true about the state
  predicate Inv(m: Model) {
    m >= 0
  }

  // Initial state
  function Init(): Model {
    0
  }

  // How actions transform the state
  function Apply(m: Model, a: Action): Model {
    match a
    case Inc => m + 1
    case Dec => m - 1
  }

  // Normalization: fix invalid states (called after Apply)
  function Normalize(m: Model): Model {
    if m < 0 then 0 else m
  }

  // Proof that Init satisfies the invariant
  lemma InitSatisfiesInv()
    ensures Inv(Init())
  {
  }

  // Proof that every step preserves the invariant
  lemma StepPreservesInv(m: Model, a: Action)
    // requires Inv(m) is inherited and should not be repeated
    ensures Inv(Normalize(Apply(m, a)))
  {
  }
}

module CounterKernel refines Kernel {
  import D = CounterDomain
}

module AppCore {
  import K = CounterKernel
  import D = CounterDomain

  function Init(): K.History { K.InitHistory() }

  function Inc(): D.Action { D.Inc }
  function Dec(): D.Action { D.Dec }

  function Dispatch(h: K.History, a: D.Action): K.History requires K.HistInv(h) { K.Do(h, a) }
  function Undo(h: K.History): K.History { K.Undo(h) }
  function Redo(h: K.History): K.History { K.Redo(h) }

  function Present(h: K.History): D.Model { h.present }
  function CanUndo(h: K.History): bool { |h.past| > 0 }
  function CanRedo(h: K.History): bool { |h.future| > 0 }
}
```


## Common Mistakes to Avoid

- It is an error to repeat inherited `requires` clauses.
- It is OK to have `assume {:axiom} false` in _proofs_, temporarily, as the pieces are put together. Strive for zero such axioms eventually.
- Nested pattern matching _is_ allowed, but needs to be properly parenthesized. Example (out of context):
```
function optimize(e: exp): exp
{
    match e
    case EInt(v) => e
    case EVar(x) => e
    case EAdd(e1, e2) => (match (optimize(e1), optimize(e2))
        case (EInt(0), e2) => e2
        case (e1, EInt(0)) => e1
        case (e1, e2) => EAdd(e1, e2))
}
```

登录后下载/点赞/收藏 ❤ 37 | ★ 0

lemmafit-dafny

目录结构

SKILL.md

举报内容

提示