Skip to content

Model UnlinkPool hashNote via PoseidonT4 boundary #65

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Th0rgal merged 1 commit into from
May 14, 2026
Merged

Model UnlinkPool hashNote via PoseidonT4 boundary #65

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 2 additions & 6 deletions Benchmark/Cases/UnlinkXyz/Pool/Contract.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -379,6 +379,7 @@ verity_contract UnlinkPool where
Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256, Uint256,
Uint256, Uint256, Uint256, Array Uint256, Array Uint256) -> (Bool)
external poseidonT3(Uint256, Uint256) -> (Uint256)
external poseidonT4(Uint256, Uint256, Uint256) -> (Uint256)
external permitWitnessTransferFrom(
Address, Address, Uint256, Uint256, Uint256, Address, Uint256, Address,
Uint256, Bytes) -> (Bool)
Expand Down Expand Up @@ -494,14 +495,9 @@ verity_contract UnlinkPool where

/- `function hashNote(Note calldata _note) public pure returns (uint256)`
(UnlinkPool.sol:212-215). Pure Poseidon-T4 boundary call. -/
-- BLOCKED(verity#1003): qualified Lean helper calls (`PoseidonT4.hash`)
-- are not yet supported inside `verity_contract` function bodies. The
-- pure spec lives in `Specs.lean` (assumed boundary). Once verity#1003
-- lifts, replace with `let h ← PoseidonT4.hash (npk, ...)` (the same
-- shape the scratchpad uses).
function view hashNote (npk : Uint256, _token : Address, amount : Uint256)
: Uint256 := do
return (add npk amount)
return externalCall "poseidonT4" [npk, addressToWord _token, amount]

function poseidon2 (lhs : Uint256, rhs : Uint256) : Uint256 := do
return externalCall "poseidonT3" [lhs, rhs]
Expand Down
2 changes: 1 addition & 1 deletion Benchmark/Generated/UnlinkXyz/Pool/Tasks/BuildGreen.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
Editable task template for `unlink_xyz/pool/build_green`.

The case is currently `stage: scoped` with `translation_status:
in_progress`. The promotion path to `build_green` is documented in
scoped`. The promotion path to `build_green` is documented in
`cases/unlink_xyz/pool/review/spec-review.md`. The reference solution
lives in `Benchmark.Cases.UnlinkXyz.Pool.Proofs`.
-/
Expand Down
13 changes: 8 additions & 5 deletions cases/unlink_xyz/pool/tasks/build_green.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,12 @@ abstraction_level: protocol_slice
abstraction_notes: >
First buildable target for the case: the `verity_contract UnlinkPool`
declaration in `Contract.lean` must elaborate cleanly through `lake build`
on the lakefile-pinned Verity revision. The three nested-dynamic-struct-
array entry points (`transfer`, `withdraw`, `adapterWithdraw`) are stubbed
with `BLOCKED(#1760-nested-dynamic):` markers until the Verity macro
surface gains struct-parameter projection from an ABI-dynamic root.
on the lakefile-pinned Verity revision. The pool entry points now elaborate
with source-shaped dynamic-array projections, LazyIMT insertion, and
PoseidonT3/T4 routed through explicit linked-external cryptographic
boundaries. Remaining blockers are tracked in the case manifest.
unsupported_feature_codes:
- nested_dynamic_struct_array_param
- uups_proxy_storage_rotation_not_modeled
- poseidon_assumed_axiom
- permit2_assumed_axiom
- groth16_verifier_assumed_axiom
Loading