Asi dafny-zig

Name: dafny-zig
Author: plurigrid

Dafny-to-Zig compiler backend development skill with verified runtime safety ("Zig-syrup")

install

source · Clone the upstream repo

git clone https://github.com/plurigrid/asi

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/plurigrid/asi "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/dafny-zig" ~/.claude/skills/plurigrid-asi-dafny-zig && rm -rf "$T"

manifest: skills/dafny-zig/SKILL.md

source content

Dafny-Zig Compiler Backend

Title: Performant, Readable and Interoperable Zig from Dafny

Specialized skill for developing

dafny-zig

, a backend compiling Dafny's intermediate representation (DAST) to safe, idiomatic Zig code.

Core Philosophy: "Zig-Syrup"

This project bridges Dafny's infinite assumptions (unbounded ints, memory, termination) with Zig's finite reality (systems programming). The binding agent ("syrup") is Runtime Safety.

Abstract

We bridge the gap between Dafny's verification guarantees and Zig's explicit resource management through "Zig-Syrup" (

runtime.zig

), a lightweight runtime layer.

Safety First:
```
rt.BigInt
```
and
```
rt.RcSlice
```
provide Dafny-like semantics with Zig safety.
Explicit Allocation: Use
```
std.ArrayListUnmanaged
```
and pass allocators explicitly.
Formal Verification: Respect DAST semantics. If Dafny verified it, Zig must implement it faithfully or trap safely.

Workflow (Tweag Standard)

Follow the Three Experts Method for all significant changes:

Verifier (Dafny Expert): Analyze DAST requirements (infinite ints, immutability).
Systems Engineer (Zig Expert): Propose safe implementation (
```
RcSlice
```
,
```
Unmanaged
```
).
Compiler Dev: Bridge the two in
```
compiler.zig
```
.

Validation Loop:

```
zig build test
```
(Must pass)
```
dafny verify
```
(on source
```
.dfy
```
if available)
Review
```
src/runtime.zig
```
for memory leaks (use
```
std.testing.allocator
```
).

Key Components

1. DAST (Dafny AST)

src/dast.zig
: Accurate reflection of Dafny's JSON IR.
Rules: Immutable by default. Use
```
parseModuleJson
```
.

2. ZAST (Zig AST)

src/zast.zig
: Generates idiomatic Zig source.
Rules: Supports
```
StructDecl
```
,
```
UnionDecl
```
(for Datatypes),
```
FnDecl
```
.

3. Runtime Library (

rt

)

src/runtime.zig
: The "Syrup" (Sticky Binding Agent).
BigInt
: Uses
```
std.ArrayListUnmanaged(u64)
```
. Handles OOM.
RcSlice(T)
: O(1) slicing and safe sharing for
```
Seq<T>
```
.
Set/Map
:
```
std.AutoHashMap
```
wrappers with value semantics.

Readability & Interoperability

Generated code should not look like "compiler vomit." It should look like Zig.

Structs & Unions: Dafny
```
datatype
```
maps cleanly to Zig
```
union(enum)
```
.
Modules: Dafny modules map to Zig files/structs.
Native Types: Where Dafny proves bounds, we emit native
```
u8
```
/
```
u64
```
.

Scientific Skill Interleaving

Plurigrid ASI Integration

Role:
```
dafny-zig
```
acts as a Verifier (MINUS -1) in the Plurigrid ecosystem.
Connection: Consumes
```
acsets
```
(via DAST) and produces
```
zig
```
(systems).

SDF Interleaving

Chapter: 5. Evaluation (Compiler as Evaluator).
Pattern:
```
compileModule
```
is a recursive evaluator transforming DAST -> ZAST.

Commands

# Build and test compiler
zig build test

# Compile a DAST file
zig build run -- compile module.dast.json output.zig

References

Mathpix: Used for OCR of formal specs (
```
mathpix-gem/
```
).
Research: See
```
.topos/
```
for bibliography (CakeML, Verified VCG).