Multiasset: FA2 token bridging support (REQUIRES THOROUGH AUDIT BEFORE MERGE)

.github/workflows/coq.yml

@@ -0,0 +1,119 @@
+name: rocq model
+
+# Drift-checks the Cairo↔Impl manifest and builds the Rocq theory under
+# coq/. The build job uses Rocq 9 via opam (same opam-via-setup-ocaml
+# pattern as the OCaml unit tests workflow) so the dependency surface
+# stays inside actions/* + opam packages, no third-party Docker
+# images.
+#
+# Triggers:
+# - any push to main affecting coq/** or cairo/src/**.cairo (Cairo
+#   edits drive drift detection)
+# - same-paths PRs
+# - the coq-model branch (so the model can iterate independently of
+#   main while it's under development)
+# - workflow_dispatch
+#
+# Extraction wires through ocaml/coq_driver/ — `make` builds the
+# theory and side-effects writing tzel_wots.{ml,mli} into coq/Impl/.
+# coq/Extracted/build.sh copies those into ocaml/coq_driver/ and runs
+# `dune build` against the OCaml workspace, so the realizations for
+# Hash3 and pack_adrs_chain in Impl/Extraction.v resolve to the real
+# Tzel.Hash.hash3 / Tzel.Wots.pack_adrs from the protocol port. The
+# smoke step asserts a known reference vector (the all-zero input
+# hashes to a fixed felt under the OCaml port; the extracted driver
+# must produce the same byte-for-byte). Cairo-side run_chain_step
+# runner + QCheck2 differential land next — see coq/STATUS.md.
+
+on:
+  push:
+    branches: [main, coq-model]
+    paths:
+      - "coq/**"
+      - "cairo/src/**.cairo"
+      - "ocaml/coq_driver/**"
+      - ".github/workflows/coq.yml"
+  pull_request:
+    paths:
+      - "coq/**"
+      - "cairo/src/**.cairo"
+      - "ocaml/coq_driver/**"
+      - ".github/workflows/coq.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: rocq-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  drift:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+
+      - name: Drift check (Cairo SHAs vs MANIFEST.toml)
+        run: ./coq/Drift/check.sh
+
+  build:
+    runs-on: ubuntu-latest
+    needs: drift
+    env:
+      LIBRARY_PATH: ${{ github.workspace }}/ocaml/vendor/mlkem-native/test/build
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+
+      - name: Install OCaml system prerequisites
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y libgmp-dev pkg-config
+
+      - name: Set up OCaml + opam
+        uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014  # v3
+        with:
+          ocaml-compiler: "5.2.0"
+
+      - name: Install OCaml dependencies (tzel library + Rocq prover)
+        # Same opam package list as the unit-tests workflow's ocaml
+        # job — tzel links against these and the extracted driver
+        # links tzel. rocq-prover provides Rocq 9 and the extraction
+        # plugin.
+        run: |
+          opam install -y dune alcotest cstruct ctypes ctypes-foreign hex \
+                          mirage-crypto yojson digestif rocq-prover
+
+      - name: Build ML-KEM native library
+        # tzel transitively links libmlkem768 via foreign stubs.
+        run: make -C ocaml/vendor/mlkem-native lib
+
+      - name: Build Rocq theory (compiles modules and extracts to OCaml)
+        working-directory: coq
+        run: |
+          opam exec -- rocq makefile -f _CoqProject -o Makefile
+          opam exec -- make -j2
+
+      - name: Build extracted-Rocq OCaml driver
+        run: opam exec -- ./coq/Extracted/build.sh
+
+      - name: Smoke run extracted driver (zero-input reference vector)
+        # With the real Tzel.Hash.hash3 / Tzel.Wots.pack_adrs
+        # realizations, hashing 96 zero bytes (x || pack_adrs(...) ||
+        # pub_seed where pack_adrs of all-zero indices is just the
+        # 8-byte little-endian TAG_XMSS_CHAIN followed by zeros) under
+        # BLAKE2s-251 produces this fixed felt. Computed once via the
+        # OCaml port; the extracted driver must match byte-for-byte.
+        run: |
+          out=$(./coq/Extracted/chain_step \
+            "0000000000000000000000000000000000000000000000000000000000000000" \
+            "0000000000000000000000000000000000000000000000000000000000000000" \
+            0 0 0)
+          echo "extracted xmss_chain_step output: $out"
+          expected="5ca134c7d8b26856b4dc9c748905318c23da49cac0fd56cc26c7885155466807"
+          if [[ "$out" != "$expected" ]]; then
+            echo "::error::expected $expected, got $out"
+            exit 1
+          fi

.gitignore

@@ -2,6 +2,10 @@ target/
 .codex
 .codex/
 ocaml/_build/
+# Extracted Rocq sources copied into the dune driver dir by
+# coq/Extracted/build.sh; the canonical copy lives in coq/Impl/.
+ocaml/coq_driver/tzel_wots.ml
+ocaml/coq_driver/tzel_wots.mli
 ocaml/vendor/mlkem-native/_build/
 ocaml/vendor/mlkem-native/test/build/config.mk
 ocaml/vendor/mlkem-native/test/build/libmlkem.a
@@ -15,6 +19,8 @@ bob.json
 mutants.out*/
 aws_creds
 .env
+.gh_token
+gh_token
 third_party/patched-git/
 
 # Generated LaTeX artifacts

README.md

@@ -16,16 +16,17 @@ Privacy on blockchains today relies on elliptic curve cryptography that quantum
 - **Fuzzy message detection.** ML-KEM-based detection keys let a lightweight indexer flag likely-incoming transactions without being able to read them.
 - **Diversified addresses.** Generate unlimited unlinkable addresses from a single master key.
 - **1 KB encrypted memos.** End-to-end encrypted with ML-KEM-768 + ChaCha20-Poly1305.
-- **Flexible N->3 transfers.** Spend up to 7 notes in a single proof and produce recipient, change, and DAL-producer fee notes without dummy notes.
+- **Flexible N->4 transfers.** Spend up to 7 notes in a single proof and produce a recipient, up to two change notes (one per asset under the multiasset 2-accumulator design), and a DAL-producer fee note without dummy notes.
+- **Multiasset.** Tez and FA2 tokens are both bridgeable; each FA2 ticketer KT1 deterministically maps to an L2 `asset_id = H("tzel:asset:" || ticketer_kt1)`. The on-chain commitment hides which asset a note carries, so rare-asset transactions blend with the common-asset crowd. See [docs/multiasset_deployment.md](./docs/multiasset_deployment.md).
 
 ### How it works
 
 A UTXO-based private transaction system where:
-- **Deposits** credit an aggregated rollup pool keyed by `pubkey_hash = H(auth_domain, auth_root, auth_pub_seed, blind)`. Multiple L1 tickets to `deposit:<hex(pubkey_hash)>` add to the same balance. `shield` debits the pool by `v + fee + producer_fee` and mints recipient + producer-fee notes; the proof's in-circuit WOTS+ signature, verified under the recipient's auth tree, binds the entire request payload so a delegated prover cannot redirect funds.
-- **Transfers** spend 1-7 private notes and create recipient, change, and DAL-producer fee notes
-- **Withdrawals** (unshield) destroy private notes, emit an L1 outbox transfer to a tz/KT1 recipient, and create a DAL-producer fee note plus optional change
+- **Deposits** credit an aggregated rollup pool keyed by `(asset_id, pubkey_hash)` where `pubkey_hash = H(auth_domain, auth_root, auth_pub_seed, blind)` and `asset_id` is determined by the L1 ticketer that emitted the deposit (tez or any registered FA2). Multiple L1 tickets from the same ticketer to `deposit:<hex(pubkey_hash)>` add to the same balance. `shield` debits the asset pool by `v + fee` (or `v + fee + producer_fee` for tez shields) and mints recipient + producer-fee notes (the producer fee is always tez; for FA2 shields the kernel separately debits `producer_fee` from the user's tez pool at the same `pubkey_hash`). The proof's in-circuit WOTS+ signature, verified under the recipient's auth tree, binds the entire request payload — including the chosen asset — so a delegated prover cannot redirect funds.
+- **Transfers** spend 1-7 private notes and create a recipient, up to two change notes, and a DAL-producer fee note (always tez)
+- **Withdrawals** (unshield) destroy private notes, emit an L1 outbox transfer through the bridge ticketer registered for the unshielded asset (`tz1/tz2/tz3` or `KT1` recipient), and create a DAL-producer fee note plus optional change notes
 - **Every shield / transfer / unshield burns at least 100000 mutez (0.1 tez)**, with a simple per-level stepped fee under congestion in the current rollup deployment
-- **Every shield / transfer / unshield also creates a separate private DAL-producer fee note**
+- **Every shield / transfer / unshield also creates a separate private DAL-producer fee note** (permanently tez, regardless of the transaction's primary asset)
 - Every spend is proven with a **zero-knowledge STARK** that verifies the **WOTS+ signature inside the circuit** — the proof itself proves spend authorization
 
 ## Quick start

apps/demo/Cargo.toml

@@ -8,4 +8,4 @@ blake2s_simd = "1.0"
 rand = "0.9"
 hex = "0.4"
 chacha20poly1305 = "0.10"
-ml-kem = { version = "=0.3.0-rc.2", features = ["getrandom"] }
+ml-kem = { version = "=0.3.2", features = ["getrandom"] }