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

Open

murbard wants to merge 80 commits into

mainfrom

Commits on May 1, 2026

coq: scaffolding for Cairo↔Coq circuit model + drift detection

Arthur Breitman
and
claude
committed
coq: extract xmss_chain_step to OCaml end-to-end

Arthur Breitman
and
claude
committed
coq: restructure to Spec/Common/Impl per expert recommendation; STATUS.md

Arthur Breitman
and
claude
committed
coq: prove iter_succ + iter_compose in Spec.Wots; add Impl.Wots refinement

Arthur Breitman
and
claude
committed

Commits on May 2, 2026

Merge branch 'main' into coq-model
Arthur Breitman
committed

Commits on May 3, 2026

coq: re-port Rocq -> OCaml extraction onto Spec/Impl/Common layout

Arthur Breitman
and
claude
committed
coq: fix Spec.Wots iter proofs for Rocq 9, switch to From Stdlib

Arthur Breitman
and
claude
committed
coq: set extraction output dir to Impl/ explicitly

Arthur Breitman
and
claude
committed

Commits on May 4, 2026

coq: wire Hash3/pack_adrs_chain to real OCaml port via dune driver

Arthur Breitman
and
claude
committed
coq: add HANDOFF.md — narrative companion to STATUS.md

Arthur Breitman
and
claude
committed
coq: Merkle verification, L-tree, WOTS recovery, XMSS verifier skeleton

Arthur Breitman
and
claude
committed
coq: L-tree totality, auth-tree walk bridge, idx range check

Arthur Breitman
and
claude
committed
coq: WOTS+ completeness and full XMSS completeness theorem

Arthur Breitman
and
claude
committed
coq: sighash fold, nullifier spec, WOTS completeness

Arthur Breitman
and
claude
committed
coq: soundness — CR axioms, Merkle binding, unique-leaf theorem

Arthur Breitman
and
claude
committed
coq: update STATUS.md with soundness and completeness work

Arthur Breitman
and
claude
committed
coq: XMSS soundness reduction — verified signatures imply same endpoints

Arthur Breitman
and
claude
committed
coq: chain injectivity, per-chain binding, transfer safety predicate

Arthur Breitman
and
claude
committed
coq: Cairo-faithful verification predicates with all three assertions

Arthur Breitman
and
claude
committed
coq: add QCheck2 differential fuzzer for extracted chain_step

Arthur Breitman
and
claude
committed
coq: WOTS+ unforgeability — checksum argument mechanized

Arthur Breitman
and
claude
committed
coq: formalize safety predicates for all three circuits

Arthur Breitman
and
claude
committed

Commits on May 5, 2026

coq: gitignore .Makefile.d build artifact
Arthur Breitman
committed

Commits on May 27, 2026

multiasset: spec — H_commit gains asset arg, N→4 transfer, per-asset balance
Arthur Breitman
committed
multiasset spec: add phi_input_wellformed and phi_output_lists_parallel
Arthur Breitman
committed
multiasset spec: assemble Phi_{transfer,shield,unshield} + sanity lemmas
Arthur Breitman
committed
multiasset Phase A: thread asset arg through commit() (Cairo + Rust)
Arthur Breitman
committed
multiasset Phase A: regenerate fixtures for new commit() arity
Arthur Breitman
committed
multiasset Phase B: per-asset balance + asset witness fields (transfer)
Arthur Breitman
committed
multiasset Phase B: per-asset balance + asset witness fields (shield)
Arthur Breitman
committed
multiasset Phase B: per-asset balance + asset witness fields (unshield)
Arthur Breitman
committed
multiasset Phase D: whitepaper §Multiasset + per-section updates
Arthur Breitman
committed
multiasset Phase C: N→4 transfer layout (Cairo + Rust sighash)
Arthur Breitman
committed
multiasset Phase C: 2 change slots in unshield (Cairo + Rust sighash)
Arthur Breitman
committed
multiasset Phase C: wire cm_4 / change_2 through TransferReq, UnshieldReq, kernel wire
Arthur Breitman
committed

Commits on May 28, 2026

multiasset Phase C: get all tests green — verifier path + fixture regen
Arthur Breitman
committed
multiasset Phase C: gen_rollup_verified_bridge_fixture refactor for N→4 output
Arthur Breitman
committed
multiasset: 15 new Cairo mutation tests for Phase B/C invariants
Arthur Breitman
committed
multiasset Phase C complete: bridge fixture regenerated, all tests pass
Arthur Breitman
committed

Commits on May 29, 2026

multiasset Phase C: wallet emits real cm_3 / cm_4 / enc_3 / enc_4
Arthur Breitman
committed
multiasset Phase C: wallet's unshield emits Phase B+C wire layout
Arthur Breitman
committed
multiasset Phase B: wallet's shield emits asset_new + asset_producer
Arthur Breitman
committed
multiasset Phase C: align proof bench witnesses with 4-output transfer / 2-change unshield
Arthur Breitman
committed

Commits on May 30, 2026

multiasset Phase B: positive non-tez coverage (14 Cairo + 6 Rust tests)
Arthur Breitman
committed
multiasset Phase E.1: AssetEntry / derive_asset_id primitives
Arthur Breitman
committed
multiasset Phase E.2: per-(asset, pubkey) deposit pools + per-asset withdrawals
Arthur Breitman
committed
multiasset Phase E.3 + E.4: lift Cairo v1 pins, add kernel registry, route outbox by asset
Arthur Breitman
committed
multiasset Phase E.5: FA2 ticketer scaffold + asset routing tests
Arthur Breitman
committed
multiasset Phase E.6: wallet --asset selection for shield
Arthur Breitman
committed

Commits on May 31, 2026

fa2_bridge_ticketer.tz: replace sketch with real annotated Michelson
Arthur Breitman
committed

Commits on Jun 8, 2026

multiasset Phase E.7a: Note.asset_id + per-asset cmd_balance
Arthur Breitman
committed
multiasset Phase E.7b: wallet transfer + unshield --asset selection
Arthur Breitman
committed
multiasset Phase E.8: per-asset deposit-recovery scan + pool tracking
Arthur Breitman
committed
bridge: thorough test suite — Michelson structural + kernel routing + end-to-end FA2
Arthur Breitman
committed
fa2_bridge_ticketer.tz: typechecks under octez-client v24.4
Arthur Breitman
committed
multiasset: address all five FA2 deployment blockers
Arthur Breitman
committed
multiasset: thorough property + edge-case coverage
Arthur Breitman
committed
multiasset: live-network FA2 bridge deployed + registered
Arthur Breitman
committed
multiasset: real shadownet round-trip of fa2_bridge_ticketer's %mint
Arthur Breitman
committed
multiasset: full FA2 mint→burn round-trip on shadownet with balance verification
Arthur Breitman
committed
gitignore: ignore .gh_token / gh_token
Arthur Breitman
committed
multiasset: CRITICAL fix — unshield asset_pub balance bypass
Arthur Breitman
committed
multiasset: CRITICAL fix — FA2 shield mints producer-fee tez out of thin air

Arthur Breitman
and
claude
committed
multiasset: CRITICAL fix — FA2 bridge bricked for any non-zero token_id

Arthur Breitman
and
claude
committed
multiasset: fix — watch-only wallets blind to FA2 notes (W1, W2)

Arthur Breitman
and
claude
committed
multiasset: harden remaining audit findings (W3, W4, X4, Michelson nit)

Arthur Breitman
and
claude
committed

Commits on Jun 9, 2026

multiasset: second-pass audit fixes (operator liveness, wire-v4 bump, Coq drift, test hardening)

Arthur Breitman
and
claude
committed
multiasset: third-pass audit fixes (HTTP OOM cap, watcher silent-failure, FA2 demo-scan, deposit-lookup asset filter)

Arthur Breitman
and
claude
committed
multiasset: address remaining audit hardening items (1, 3-8, 10-13)

Arthur Breitman
and
claude
committed
multiasset: sync specs, docs, and whitepaper with the multiasset implementation

Arthur Breitman
and
claude
committed
multiasset: final-sweep inconsistency fixes (Coq spec, stale docstrings, top-level README)

Arthur Breitman
and
claude
committed
multiasset: comprehensive end-to-end verification + final docstring sync

Arthur Breitman
and
claude
committed
multiasset: wire validate_l1_ticketer_canonical into the CLI + regenerate protocol_v1.json

Arthur Breitman
and
claude
committed
multiasset: sync OCaml port with 5-ary commit() + restore outgoing_ct in vectors

Arthur Breitman
and
claude
committed

Commits on Jun 10, 2026

fix(wallet): report producer note commitment in transfer producer_cm (#35)

denver-s
and
claude
authored
Merge origin/main into multiasset

Arthur Breitman
and
claude
committed

Commits on Jun 11, 2026

fix(ocaml): sync the OCaml port's transaction layer with multiasset (+ de-mask the interop test)

Arthur Breitman
and
claude
committed
test: add per-flow sighash conformance test (OCaml <-> Rust core), the guard that should have caught it

Arthur Breitman
and
claude
committed
multiasset: make the OCaml port actually implement multiasset (FA2), not just the wire shape

Arthur Breitman
and
claude
committed
multiasset: extend the interop scenario with an end-to-end FA2 round-trip

Arthur Breitman
and
claude
committed