Skip to content

feat: add MPF exclusion proofs with Aiken parity#150

Merged
paolino merged 2 commits intofeat/port-mpf-write-path-to-wasm-with-browser-demo-mirrfrom
feat/mpf-exclusion-proof-aiken-parity
Apr 23, 2026
Merged

feat: add MPF exclusion proofs with Aiken parity#150
paolino merged 2 commits intofeat/port-mpf-write-path-to-wasm-with-browser-demo-mirrfrom
feat/mpf-exclusion-proof-aiken-parity

Conversation

@paolino
Copy link
Copy Markdown
Collaborator

@paolino paolino commented Apr 23, 2026

Summary

Part of #149, based on the mpf-write extraction in #147.

This PR adds first-class MPF exclusion proofs and then fixes the remaining Aiken parity gap so the Haskell proof codec matches the canonical upstream off-chain implementation byte-for-byte.

What Changed

1. MPF exclusion proofs are now a first-class API

  • Added MPF.Proof.Exclusion with:
    • MPFExclusionProof
    • exclusion proof generation for absent keys
    • pure exclusion verification
    • projection back to shared proof steps for Aiken/JS transport
  • Re-exported the exclusion API from MPF.
  • Added pure test helpers in MPF.Test.Lib.

2. Property parity with CSMT

  • Added exclusion properties in MPF.Proof.ExclusionSpec:
    • absent key proves
    • present key returns Nothing
    • tampered target fails
  • Added inclusion property parity in MPF.Proof.InsertionSpec:
    • random facts in a full tree
    • random facts in a sparse tree
    • deleted facts reject verification

3. Aiken parity fix

  • Fixed fork-neighbor prefix encoding in MPF.Hashes.Aiken.
  • The bug was that fork prefixes were encoded as packed nibble pairs; upstream encodes them as one byte per nibble.
  • Added a peach[uid: 0] regression vector in MPF.ProofCompatSpec because mango and kumquat did not exercise that codec shape.
  • Kept the pinned melon exclusion parity vector there as well.

4. Spec and handoff updates

Verification

Passed locally:

  • nix develop --quiet -c just test 'MPF.Proof.Exclusion'
  • nix develop --quiet -c just test 'MPF.Proof.Insertion'
  • nix develop --quiet -c just test 'MPF.Hashes.Aiken'
  • nix develop --quiet -c just test 'MPF.ProofCompat'

I also compared our rendered CBOR against the canonical upstream off-chain implementation at aiken-lang/merkle-patricia-forestry HEAD (5ca6f3feaf9ab1e20007f164882dae3d2359745e) for 31 cases:

  • 30 fruit inclusion proofs
  • 1 melon exclusion proof

After the fork-prefix fix, that external comparison reported checked: 31, mismatches: [].

Reviewer Focus

Follow-up

This does not yet wire MPF exclusion through MTS.Interface / MPF.MTS or the browser ptype = 1 path from #146. This PR is the proof-layer blocker removal needed before that routing work.

@paolino paolino added the feat New feature label Apr 23, 2026
@paolino paolino self-assigned this Apr 23, 2026
@paolino paolino merged commit d5f4674 into feat/port-mpf-write-path-to-wasm-with-browser-demo-mirr Apr 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

feat New feature

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant