Dafny–Clojure JVM Interop: Verified Transforms on the JVM

The fourth layer closes the gap between proof and execution. Where Lean 4 proves Codec.roundtrip : forall a, decode (encode a) = a as a dependent record that never runs, the Dafny layer compiles the same statement into Java bytecode where decode and encode are real methods with the proof erased at compile time.

Defines the four codec patterns as a discriminated union:

datatype CodecEntry =
  | CInvolution(inv: Involution)
  | CBijection(bij: Bijection)
  | CParameterized(par: Parameterized)
  | CSurjection(sur: Surjection)

The Involution record carries a single function fn: String -> String and the property IsInvolution(inv) : forall x :: inv.fn(inv.fn(x)) = x. The Bijection carries encode and decode with RoundTrip(b) : forall x | ValidEncodeDomain(b, x) :: b.decode(b.encode(x)) = x.

Concrete implementations and proofs for identity, reverse, and rot13 are included. The ReverseConcat lemma proves the anti-homomorphism property: Reverse(a + b) = Reverse(b) + Reverse(a)=.

Models the pipeline as a sequence of Step records threaded left-to-right. Key definitions:

• ResolveStep: pattern-matches on CodecEntry to select the correct function for a given direction
• Execute: recursive pipeline execution with halt-on-first-error semantics
• PipelineIsReversible: every step's codec is reversible and both directions resolve
• ReversePipelineCorrect: reverses step order and flips directions, with involutions keeping Encode (direction irrelevant)

The core round-trip theorem is stated but not yet proved:

lemma RoundTripTheorem(
  registry: Registry, steps: seq<Step>, input: String
)
  requires PipelineIsReversible(registry, steps)
  requires RegistrySemanticallCorrect(registry)
  ensures Execute(registry, ReversePipelineCorrect(registry, steps),
    Execute(registry, steps, input).finalValue).finalValue == input
{
  assume false; // placeholder --- marks an open obligation
}

The assume false is honest: it marks the proof as incomplete. The theorem is blocked on resolving spec gaps SG-2 (domain predicates) and SG-7 (structural vs. semantic reversibility).

Three claims proved:

1. Decode is shift (26-N): CaesarDecode(x, n) = RotN(x, (26-n) % 26)= — by definition, but the proof exposes an edge case at N=0 where (26-0) % 26 = 0, not 26.
2. N=13 is the unique fixed point: For N in [1,25], N=13 is the only value where CaesarEncode(x, N) = CaesarDecode(x, N)= for all x. FixedPointCharacterization proves EncodeSameAsDecode(n) <==> (n = 0 || n = 13). The spec's claim of "uniqueness" is imprecise about N=0.
3. Round-trip: CaesarDecode(CaesarEncode(x, N), N) = x= for all x and all N in [0,25]. The proof reduces to the modular arithmetic lemma ShiftAndUnshift(a, n): (a + n + (26-n)) % 26 = a=.

Test vector verification: the spec's caesar:3:d on "HW WX EUXWH" decodes to "ET TU BRUTE". Each character shift is checked individually.

The external Dafny verification identified nine specification gaps. These are the boundary of what can be formally proved without spec clarification:

SG-7 is the most architecturally significant. The Clojure registry uses a structural flag (:inverse? true) that says nothing about whether decode actually inverts encode. A codec could pass the structural check and still have a broken implementation. The Dafny model separates these:

predicate IsReversible(e: CodecEntry)        // structural: has the fields
predicate SemanticallReversible(e: CodecEntry) // semantic: round-trip holds

The pipeline round-trip theorem requires both.

Proofs.dfy establishes that the composition of two involutions is an involution if and only if they commute. This is a result the Lean 4 specs do not prove (they prove pipeline composition via Equiv.symm.trans but do not address commutativity).

The CommutingInvolutionsCompose lemma:

f(g(f(g(x))))
  = f(f(g(g(x))))   [by commutativity: g(f(y)) = f(g(y))]
  = g(g(x))          [by f involution]
  = x                [by g involution]

In the codec pipeline, this means rot13+atbash+rot13+atbash is identity if and only if rot13 and atbash commute. They do not in general (both operate on letters but with different mappings), so the composition is not an involution — it is a bijection whose inverse is atbash+rot13+atbash+rot13 (reverse the chain).

dafny build --target:java produces Java source files and a Gradle build script. The output directory contains:

out/
  src/main/java/
    Involutions_Compile/        # one Java class per Dafny module
      __default.java            # top-level functions
      Codec.java                # datatype → Java class
    dafny/                      # runtime library (always included)
      DafnySequence.java
      DafnySet.java
      DafnyMap.java
      ...
  build.gradle

The critical bridge type. Key methods from the Java runtime source:

// Factory: Java String → Dafny string
static DafnySequence<Character> asString(String s)
static DafnySequence<CodePoint> asUnicodeString(String s)

// Extraction: Dafny string → Java String
String verbatimString()

// Core operations
T select(int i)
int length()
DafnySequence<T> subsequence(int lo, int hi)
DafnySequence<T> drop(int lo)
DafnySequence<T> take(int hi)
static <T> DafnySequence<T> concatenate(
  DafnySequence<? extends T> a,
  DafnySequence<? extends T> b)

// Conversion
Array<T> toArray()
static byte[] toByteArray(DafnySequence<Byte> seq)
static int[] toIntArray(DafnySequence<Integer> seq)

// Predicates
boolean isPrefixOf(DafnySequence<U> other)
boolean contains(Object t)
Iterator<T> iterator()

The asString / verbatimString pair is the interop seam. Every codec function in the Dafny output operates on DafnySequence<Character>; the Clojure bridge converts to/from java.lang.String at the boundary.

{:extern} declares that a method or module is implemented outside Dafny. For Java targets, the arguments map to package and class names:

module {:extern "wal_sh.tools.rot13"} Rot13Bridge {
  method {:extern "wal_sh.tools.rot13.core", "rot13"}
    Rot13(s: string) returns (r: string)
    ensures |r| == |s|
    ensures forall i :: 0 <= i < |s| ==>
      (('A' <= s[i] <= 'Z' || 'a' <= s[i] <= 'z') ==>
        r[i] == RotChar(s[i], 13))
}

Dafny verifies all callers of Rot13 against the specification. The implementation itself is trusted — it comes from the Clojure AOT-compiled .class file. This is the seam where verified callers meet unverified (but tested) implementations.

Dafny distinguishes ghost code (used only in proofs) from compiled code. At the Java target:

• ghost function: erased entirely — no Java class generated
• function: compiled to a static Java method (Dafny 4.x; was function method in 3.x)
• lemma: erased — the proof obligation is discharged at verify time
• method: compiled to a Java method
• predicate: erased if ghost, compiled if used in runtime code
• requires / ensures: erased — they are checked statically, not at runtime

This means the compiled JAR contains only the executable codec functions. The proofs that those functions are correct are verified once at compile time and then gone. The JAR is as lean as hand-written Java.

The primary use case. Dafny proves the round-trip property at compile time. The compiled Java class is a normal JVM class. Clojure calls it via interop.

;; After adding the Dafny-compiled JAR to the classpath:
(import '[dafny DafnySequence])

;; Bridge: String <-> DafnySequence<Character>
(defn ->dafny-string [^String s]
  (DafnySequence/asString s))

(defn <-dafny-string [dseq]
  (.verbatimString dseq))

;; Dafny `function Rot13(s: string): string` compiles to:
;;   public static DafnySequence<Character> Rot13(DafnySequence<Character> s)
;; in the class Involutions_Compile.__default

(defn verified-rot13 [s]
  (-> s
      ->dafny-string
      Involutions_Compile.__default/Rot13
      <-dafny-string))

;;=> (verified-rot13 "hello")
;;=> "uryyb"
;;=> (verified-rot13 (verified-rot13 "hello"))
;;=> "hello"  ; involution — proved by Rot13StringInvolutive lemma

The threading macro mirrors the pipeline's own threading model. Each codec call is ->dafny-string -> Dafny_method -> <-dafny-string.

The inverse direction. Dafny declares a specification with {:extern}. Clojure AOT-compiles its codec namespace to .class files. Those classes go on the classpath and satisfy the extern declaration.

;; AOT-compile the codec namespace to .class files
(binding [*compile-path* "target/classes"]
  (compile 'wal-sh.tools.rot13.core))

Dafny verifies callers against the declared spec:

method {:extern "wal_sh.tools.rot13.core", "rot13"}
  ClojureRot13(s: string) returns (r: string)
  ensures |r| == |s|
  ensures forall i :: 0 <= i < |s| ==>
    r[i] == Rot13Char(s[i])

// Dafny can now use ClojureRot13 in other verified code:
method Pipeline(input: string) returns (output: string)
  ensures output == Rot13(Rot13(input))  // proved via the spec
{
  var mid := ClojureRot13(input);
  output := ClojureRot13(mid);
}

This is more fragile than Direction 1 because Dafny trusts the extern. If the Clojure implementation has a bug, the proof is unsound. The value is in verifying composition: callers of the extern are checked against the declared contract.

Both implementations run on the same JVM. A test.check property asserts they produce identical output:

(ns wal-sh.tools.transform.dafny-equiv-test
  (:require [clojure.test.check.clojure-test :refer [defspec]]
            [clojure.test.check.generators :as gen]
            [clojure.test.check.properties :as prop]
            [wal-sh.tools.transform.core :as core]
            [wal-sh.tools.transform.dafny-bridge :as bridge]))

(defspec rot13-equivalence 1000
  (prop/for-all [s gen/string-ascii]
    (= (core/rot13 s)
       (bridge/verified-rot13 s))))

(defspec jump5-equivalence 1000
  (prop/for-all [s gen/string-ascii]
    (= ((:fn (core/codec-by-id :jump5)) s)
       (bridge/verified-jump5 s))))

(defspec atbash-equivalence 1000
  (prop/for-all [s gen/string-ascii]
    (= ((:fn (core/codec-by-id :atbash)) s)
       (bridge/verified-atbash s))))

The Dafny version carries a proof. The Clojure version carries 1000 sampled witnesses. Any divergence is a bug in the bridge layer, not in either implementation. This is the strongest assurance: proof AND empirical testing AND cross-implementation agreement.

DafnySequence is immutable and backed by an array. asString copies the input string's char[] into a new array. verbatimString copies back. For a pipeline of N steps, the naive bridge performs 2N copies.

Optimization: keep the value in DafnySequence form throughout the pipeline and convert only at the boundary:

(defn thread-verified [input steps]
  (let [dafny-input (->dafny-string input)]
    (<-dafny-string
      (reduce (fn [acc step-fn] (step-fn acc))
              dafny-input
              steps))))

This reduces to 2 copies total regardless of pipeline length.

Dafny 4.11.0 runs natively on FreeBSD 15.0. See Dafny on FreeBSD 15.0 for the full installation walkthrough and toolchain verification.

pkg install dotnet-sdk z3
dotnet tool install --global dafny
export PATH="$HOME/.dotnet/tools:$PATH"
dafny --version   # 4.11.0

Merge the local spec/dafny/Involutions.dfy (which has jump5 and atbash, absent from the external repo) with aygp-dr/transform-tool-dafny's Codec.dfy, Pipeline.dfy, Proofs.dfy, and CaesarProof.dfy.

Target structure:

spec/dafny/
  Codec.dfy          # algebraic model (from aygp-dr, extended)
  Involutions.dfy    # 5 involutions + proofs (local, all 5 codecs)
  Bijections.dfy     # encode/decode pairs (hex, base64, xor, etc.)
  Pipeline.dfy       # composition and reversal (from aygp-dr)
  Proofs.dfy         # collected theorems (from aygp-dr, extended)
  CaesarProof.dfy    # parameterized codec (from aygp-dr)

dafny build --target:java spec/dafny/Involutions.dfy -o spec/dafny/out
cd spec/dafny/out && gradle jar

Add a deps.edn alias for the compiled JAR:

{:aliases
 {:dafny {:extra-paths ["spec/dafny/out/build/libs"]
          :extra-deps  {}}}}

Create src/wal_sh/tools/transform/dafny_bridge.clj as described in 7.

test/wal_sh/tools/transform/dafny_equiv_test.clj runs both implementations side-by-side and asserts identical output for 1000 random ASCII strings per codec.

dafny build --target:js emits CommonJS modules. The output uses a _dafny runtime with types like _dafny.Seq and _dafny.CodePoint.

Integration with shadow-cljs:

;; shadow-cljs.edn
{:builds
 {:transform
  {:js-options
   {:resolve {"dafny-runtime" {:target :npm-module
                                :require "spec/dafny/js-out/dafny/dafny.js"}}}}}}

Lower priority than the JVM path. The browser tool already works; the JS target adds verified browser codecs.

With GraalVM 21.0.8 on this host:

native-image -jar spec/dafny/out/build/libs/Involutions.jar \
  --no-fallback -o verified-codecs

This produces a static binary with verified codecs. No JVM startup. Sub- millisecond invocation. Useful for CLI tools or CGI endpoints.