feat(rust): Rust port of DialCache with formal conformance replay

.github/actions/setup-validation/action.yml

@@ -10,6 +10,9 @@ inputs:
   java:
     description: Install Java 21 for bounded symbolic model checking.
     default: "false"
+  rust:
+    description: Install the pinned Rust toolchain (rust/rust-toolchain.toml) with clippy and rustfmt.
+    default: "false"
 runs:
   using: composite
   steps:
@@ -35,3 +38,14 @@ runs:
       with:
         distribution: temurin
         java-version: "21"
+    # The toolchain pin matches rust/rust-toolchain.toml and the cargo 1.98.1
+    # prerequisite probe in formal/validation.mjs.
+    - uses: dtolnay/rust-toolchain@02cb101ec7c40f2c49e1d9714d64511d8e1b74de # master 2026-09-12
+      if: inputs.rust == 'true'
+      with:
+        toolchain: 1.98.1
+        components: clippy, rustfmt
+    - uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2
+      if: inputs.rust == 'true'
+      with:
+        workspaces: rust

.github/workflows/ci.yaml

@@ -67,17 +67,32 @@ jobs:
           retention-days: 14
           if-no-files-found: warn
 
-  # The existing required `test` status now requires both native language jobs.
+  rust:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
+      - uses: ./.github/actions/setup-validation
+        with:
+          rust: "true"
+      - name: Check Rust formatting, clippy and native tests including the smoke conformance run
+        run: make check-rust
+      - name: Check real Redis, Valkey and Cluster integrations and invalidation vectors
+        run: make integration-rust
+
+  # The existing required `test` status now requires every native language job.
   test:
-    needs: [typescript, go]
+    needs: [typescript, go, rust]
     if: always()
     runs-on: ubuntu-latest
     timeout-minutes: 5
     steps:
-      - name: Require successful TypeScript and Go checks
+      - name: Require successful TypeScript, Go and Rust checks
         env:
           TYPESCRIPT_RESULT: ${{ needs.typescript.result }}
           GO_RESULT: ${{ needs.go.result }}
+          RUST_RESULT: ${{ needs.rust.result }}
         run: |
           test "$TYPESCRIPT_RESULT" = success
           test "$GO_RESULT" = success
+          test "$RUST_RESULT" = success

.github/workflows/formal-full.yaml

@@ -4,7 +4,7 @@ on:
   workflow_dispatch:
     inputs:
       exploration:
-        description: Explore a fresh seed in both ports in addition to pinned acceptance.
+        description: Explore a fresh seed in every port in addition to pinned acceptance.
         type: boolean
         default: false
   schedule:
@@ -23,7 +23,7 @@ jobs:
     runs-on: ubuntu-latest
     # Run 35568655690 exhausted the old hour inside the expanded challenge
     # campaign, before generation or native replay. Allow the model job's
-    # budget below plus time for the fresh corpus and both ports; individual
+    # budget below plus time for the fresh corpus and every port; individual
     # evaluator and replay commands retain their own hang bounds.
     timeout-minutes: 180
     steps:
@@ -32,7 +32,8 @@ jobs:
         with:
           quint: "true"
           go: "true"
-      - name: Explore a fresh recorded seed and replay both ports
+          rust: "true"
+      - name: Explore a fresh recorded seed and replay every port
         run: make explore
       - name: Preserve exploratory sources, seed and counterexamples
         if: always()
@@ -77,8 +78,8 @@ jobs:
           retention-days: 14
 
   # The single producer for every downstream lane: corpus generation, fixture
-  # recomputation and the shared witness evidence. Both port replays and both
-  # mutation measurements depend only on this job's artifact and run in parallel.
+  # recomputation and the shared witness evidence. Every port replay and mutation
+  # measurement depend only on this job's artifact and run in parallel.
   generate:
     # Scheduled workflows run the default branch; keep the intended main scope explicit.
     if: github.event_name != 'schedule' || github.ref == 'refs/heads/main'
@@ -256,6 +257,37 @@ jobs:
           if-no-files-found: warn
           retention-days: 14
 
+  rust-parity:
+    needs: generate
+    runs-on: ubuntu-latest
+    # The Rust replay compiles the crate in release mode before replaying the
+    # same corpus Go completes in about 4.5 minutes; the budget mirrors go-parity.
+    timeout-minutes: 40
+    steps:
+      - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
+      - uses: ./.github/actions/setup-validation
+        with:
+          rust: "true"
+      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          name: formal-traces
+          path: .formal-traces
+      - name: Require Rust replay of the complete corpus
+        run: make formal-rust
+      - name: Preserve Rust parity completion evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: rust-parity-evidence
+          path: |
+            .formal-traces/rust-replay.jsonl
+            .formal-traces/rust-replay-summary.json
+            .formal-traces/rust-context.json
+            .formal-traces/rust-completion.json
+          include-hidden-files: true
+          if-no-files-found: warn
+          retention-days: 14
+
   # The Go lane bounds the whole workflow: every mutant replays the generated
   # cohort, about 1.6 minutes per mutant on a fast runner and about 3 on the
   # slow class (13 mutants took 25 minutes in run 34660598461 and 47-48 in
@@ -324,11 +356,72 @@ jobs:
           if-no-files-found: warn
           retention-days: 14
 
+  # The Rust lane compiles the crate and its test binaries in release mode
+  # once per mutant (dependencies are cached across mutants) and replays the
+  # generated cohort in about a minute; the budget mirrors go-mutations.
+  rust-mutations:
+    needs: generate
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        shard: [1, 2, 3]
+    env:
+      MUTATION_SHARD: ${{ matrix.shard }}/3
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
+      - uses: ./.github/actions/setup-validation
+        with:
+          rust: "true"
+      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          name: formal-traces
+          path: .formal-traces
+      - name: Measure one shard of Rust assertion-based fault detection
+        run: make mutations-rust
+      - name: Preserve this shard's Rust mutation evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: rust-semantic-shard-${{ matrix.shard }}
+          path: .formal-traces/rust-semantic/shards/
+          include-hidden-files: true
+          if-no-files-found: warn
+          retention-days: 14
+
+  rust-mutations-merge:
+    needs: rust-mutations
+    # Run after the shards regardless of their result so a missing shard is
+    # diagnosed by the merge; skip only when the matrix itself never ran.
+    if: always() && needs.rust-mutations.result != 'skipped'
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6.1.0
+      - uses: ./.github/actions/setup-validation
+      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          pattern: rust-semantic-shard-*
+          path: .formal-traces/rust-semantic/shards
+          merge-multiple: true
+      - name: Require every Rust shard and merge the complete report
+        run: make mutations-merge-rust
+      - name: Preserve Rust mutation evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: rust-semantic-evidence
+          path: .formal-traces/rust-semantic/
+          include-hidden-files: true
+          if-no-files-found: warn
+          retention-days: 14
+
   # A failed or skipped dependency cannot turn smoke evidence into full acceptance.
   # The mutation lanes count through their merge jobs: a merge succeeds only
   # when every shard's report is present, consistent and free of lost detections.
   formal-full:
-    needs: [check-models, generate, typescript-parity, symbolic, typescript-mutations-merge, go-parity, go-mutations-merge, exploration]
+    needs: [check-models, generate, typescript-parity, symbolic, typescript-mutations-merge, go-parity, go-mutations-merge, rust-parity, rust-mutations-merge, exploration]
     if: always()
     runs-on: ubuntu-latest
     timeout-minutes: 5
@@ -351,6 +444,13 @@ jobs:
         with:
           name: go-parity-evidence
           path: formal-summary/go
+      - name: Collect Rust completion evidence
+        if: always()
+        continue-on-error: true
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          name: rust-parity-evidence
+          path: formal-summary/rust
       - name: Collect model check report
         if: always()
         continue-on-error: true
@@ -383,20 +483,25 @@ jobs:
             formal-summary/go/go-completion.json
             formal-summary/go/go-context.json
             formal-summary/go/go-replay-summary.json
+            formal-summary/rust/rust-completion.json
+            formal-summary/rust/rust-context.json
+            formal-summary/rust/rust-replay-summary.json
             formal-summary/model-check/model-properties/report.json
             formal-summary/symbolic/report.json
             formal-summary/exploration/*/report.json
           include-hidden-files: true
           if-no-files-found: warn
           retention-days: 90
-      - name: Require the model check, the generated corpus, both port replays and both merged mutation measurements
+      - name: Require the model check, the generated corpus, every port replay and every merged mutation measurement
         env:
           CHECK_MODELS_RESULT: ${{ needs.check-models.result }}
           GENERATE_RESULT: ${{ needs.generate.result }}
           TYPESCRIPT_RESULT: ${{ needs.typescript-parity.result }}
           TYPESCRIPT_MUTATIONS_MERGE_RESULT: ${{ needs.typescript-mutations-merge.result }}
           GO_RESULT: ${{ needs.go-parity.result }}
           GO_MUTATIONS_MERGE_RESULT: ${{ needs.go-mutations-merge.result }}
+          RUST_MUTATIONS_MERGE_RESULT: ${{ needs.rust-mutations-merge.result }}
+          RUST_RESULT: ${{ needs.rust-parity.result }}
           SYMBOLIC_RESULT: ${{ needs.symbolic.result }}
           EXPLORATION_RESULT: ${{ needs.exploration.result }}
           EXPLORATION_REQUIRED: ${{ github.event_name == 'schedule' || inputs.exploration == true }}
@@ -407,6 +512,8 @@ jobs:
           test "$TYPESCRIPT_MUTATIONS_MERGE_RESULT" = success
           test "$GO_RESULT" = success
           test "$GO_MUTATIONS_MERGE_RESULT" = success
+          test "$RUST_MUTATIONS_MERGE_RESULT" = success
+          test "$RUST_RESULT" = success
           test "$SYMBOLIC_RESULT" = success
           if [ "$EXPLORATION_REQUIRED" = true ]; then
             test "$EXPLORATION_RESULT" = success

.github/workflows/formal.yaml

@@ -24,7 +24,8 @@ jobs:
       - uses: ./.github/actions/setup-validation
         with:
           go: "true"
-      - name: Audit contracts and replay committed Quint smoke in both ports
+          rust: "true"
+      - name: Audit contracts and replay committed Quint smoke in every port
         run: make audit smoke
       - name: Detect changes requiring fresh Quint artifact generation
         id: fixture-scope

.gitignore

@@ -11,3 +11,4 @@ docs/.vitepress/cache/
 .idea/
 .vscode/
 *.log
+rust/target/

AGENTS.md

@@ -2,7 +2,7 @@
 
 ## Project overview
 
-DialCache has TypeScript and Go implementations with explicit request-scoped enablement, local and Redis layers, runtime rollout controls, request coalescing, targeted invalidation, and adapter-based observability.
+DialCache has TypeScript, Go and Rust implementations with explicit request-scoped enablement, local and Redis layers, runtime rollout controls, request coalescing, targeted invalidation, and adapter-based observability.
 
 ## Structure
 
@@ -27,6 +27,7 @@ src/
   internal/             # Cache layers, runtime config, payload compression, and invalidation Lua script
 test/                   # Unit and Redis integration tests
 go/                     # Go module, public cache and adapters, shared-corpus replay
+rust/                   # Rust crate, public cache and adapters, shared-corpus replay (tests/conformance.rs)
 formal/                 # Quint behavioral source of truth, contracts and portable vectors
 ```
 
@@ -64,8 +65,8 @@ formal/                 # Quint behavioral source of truth, contracts and portab
   readable as behavior definitions, share helpers with identical meaning, retain
   independent property checks, and register executable evidence in the catalogs.
 - Define portable behavior in Quint first. Require consequential generated
-  witnesses and replay the same histories in TypeScript and Go; keep native
-  API, wire and integration tests for their explicit boundaries.
+  witnesses and replay the same histories in TypeScript, Go and Rust; keep
+  native API, wire and integration tests for their explicit boundaries.
 
 ## Validation
 
@@ -75,8 +76,10 @@ make check
 make integration
 ```
 
-Use `make formal` for complete Quint model checks, corpus generation and both
-ports' full replay, then `make mutations` for assertion-strength checks.
+`make check-rust` runs the Rust crate's fmt, clippy, unit, vector, scenario and
+smoke checks; `make formal-rust` completes its replay of the generated corpus.
+Use `make formal` for complete Quint model checks, corpus generation and every
+port's full replay, then `make mutations` for assertion-strength checks.
 `make ci` runs all validation in the required order. `make help` lists targets
 and prerequisites; `formal/README.md` documents the fast PR and full-validation
 workflows. Full behavior/model/replay changes require full validation before

Makefile

@@ -5,7 +5,7 @@
 
 NODE ?= node
 
-.PHONY: help check check-ts check-go docs audit smoke formal formal-check formal-generate formal-ts formal-go fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go integration integration-ts integration-go package-floor ci explore model-check
+.PHONY: help check check-ts check-go check-rust docs audit smoke formal formal-check formal-generate formal-ts formal-go formal-rust fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go mutations-rust mutations-merge-rust integration integration-ts integration-go integration-rust package-floor ci explore model-check
 
-help check check-ts check-go docs audit smoke formal formal-check formal-generate formal-ts formal-go fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go integration integration-ts integration-go package-floor ci explore model-check:
+help check check-ts check-go check-rust docs audit smoke formal formal-check formal-generate formal-ts formal-go formal-rust fixtures-check kernel-fixtures differential mutations mutations-ts mutations-go mutations-merge-ts mutations-merge-go mutations-rust mutations-merge-rust integration integration-ts integration-go integration-rust package-floor ci explore model-check:
 	$(NODE) formal/validation.mjs $@

README.md

@@ -132,10 +132,10 @@ for sampling and comparison behavior.
 | Recovery from selected source failures | [Stale-on-error](https://lan17.github.io/DialCache/stale-on-error.html) |
 | Shared execution and deadlines | [Coalescing and liveness](https://lan17.github.io/DialCache/coalescing.html) |
 | Methods, options, and exports | [API reference](https://lan17.github.io/DialCache/api.html) |
-| Go implementation and shared behavior contracts | [Go guide](go/README.md) · [Quint specification](formal/README.md) · [Worked walkthrough](formal/WALKTHROUGH.md) |
+| Go and Rust implementations and shared behavior contracts | [Go guide](go/README.md) · [Rust guide](rust/README.md) · [Quint specification](formal/README.md) · [Worked walkthrough](formal/WALKTHROUGH.md) |
 
-The Go port and the TypeScript library replay the same Quint-generated
-histories. Whether those histories reach every required boundary is decided by
+The Go port, the Rust port and the TypeScript library replay the same
+Quint-generated histories. Whether those histories reach every required boundary is decided by
 one language-neutral evaluator, `node formal/witnesses.mjs evaluate`, that any
 port runs over the same corpus; no port depends on another port's test suite
 for its completion evidence.