Dafny Zig

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.

1. Safety First: rt.BigInt and rt.RcSlice provide Dafny-like semantics with Zig safety.
2. Explicit Allocation: Use std.ArrayListUnmanaged and pass allocators explicitly.
3. 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:

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

Validation Loop:

1. zig build test (Must pass)
2. dafny verify (on source .dfy if available)
3. 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).