Add generic Unlink audit readiness helpers by Th0rgal · Pull Request #1795 · lfglabs-dev/verity

Th0rgal · 2026-05-01T20:26:17Z

Summary

This PR adds generic Verity-core surfaces needed for line-by-line Unlink audit modeling without adding Unlink-specific protocol semantics:

Adds Compiler.Modules.Calls.bubblingValueCall for Solidity-style arbitrary call{value: v}(data) over explicit memory slices, including exact revert-returndata bubbling.
Adds SHA-256 precompile helpers: Compiler.Modules.Precompiles.sha256Memory and sha256.
Adds static packed hashing helpers in Compiler.Modules.Hashing:
- abiEncodePackedWords / abiEncodePacked
- sha256PackedWords / sha256Packed
- abiEncodePackedStaticSegments
- sha256PackedStaticSegments
Adds Verity.Stdlib.Math.SNARK_SCALAR_FIELD and modField.
Adds focused feature and smoke coverage for mutable Stmt.assignVar inside Stmt.forEach, multi-value internal helper returns, ECM lowering, invalid arity, mutability rejection, and trust-report assumptions.

Trust Boundaries

bubblingValueCall models generic EVM call choreography only: gas forwarding, target/value/input/output operands, success check, and revert-returndata bubbling. Calldata meaning, callee behavior, and protocol postconditions remain package-local assumptions.
SHA-256 helpers assume the EVM precompile 0x02 semantics under the explicit evm_sha256_precompile ECM axiom.
Packed hashing helpers assume their documented static packed layout under abi_packed_static_word_layout or abi_packed_static_segment_layout; they do not claim full Solidity dynamic abi.encodePacked support.
Poseidon, Permit2, Lazy-IMT, Groth16, and the full Unlink contract model remain outside Verity core and belong in unlink-verity with explicit package-local assumptions/proof-status tags.

Docs Changed

docs/EXTERNAL_CALL_MODULES.md
docs/INTERPRETER_FEATURE_MATRIX.md
docs/ROADMAP.md
docs/UNLINK_AUDIT_VERITY_CORE_PROMPT.md
Compiler/Modules/README.md
docs-site/content/edsl-api-reference.mdx

Tests Run

lake build Compiler.Modules.Hashing Compiler.Modules.Precompiles Compiler.Modules.Calls Compiler.CompilationModelFeatureTest Contracts.Smoke Contracts.MacroTranslateInvariantTest Verity.Stdlib.Math
lake build Compiler
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check

lake build Compiler still reports pre-existing Compiler/Proofs/IRGeneration/ContractFeatureTest.lean unnecessary simpa linter warnings; this PR does not touch that file.

Note

Medium Risk
Adds new external-call and hashing ECMs (including low-level call{value:…} and SHA-256 precompile usage) plus new math primitives; incorrect lowering or assumptions could affect contract correctness and audit boundaries, though changes are largely additive with extensive feature tests.

Overview
Adds new Verity-core ECM surfaces for audit-oriented modeling: a generic low-level bubblingValueCall/bubblingValueCallNoOutput that lowers to Yul call with exact revert-returndata bubbling, and a sha256Memory (alias sha256) precompile helper for hashing existing memory slices.

Introduces Compiler.Modules.Hashing packed-hash helpers for static preimages (abiEncodePackedWords/abiEncodePacked, sha256PackedWords/sha256Packed, plus mixed-width abiEncodePackedStaticSegments/sha256PackedStaticSegments with width validation), and wires the new module into Compiler/Modules.lean and docs.

Expands test and smoke coverage to validate Yul lowering, arity/mutability rejection, and trust-report assumptions (including new smoke contracts for packed hashing and value-call ECMs), adds a multi-return helper smoke contract, documents forEach accumulator limitations, and adds BN254 field helpers (SNARK_SCALAR_FIELD, modField) with accompanying proof lemmas and documentation updates.

^{Reviewed by Cursor Bugbot for commit bbeb9c8. Bugbot is set up for automated code reviews on this repo. Configure here.}

github-actions · 2026-05-01T20:27:06Z

\n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

Th0rgal · 2026-05-02T01:47:14Z

Added a no-output convenience wrapper for the common adapter/router call shape:

Compiler.Modules.Calls.bubblingValueCallNoOutput target value inputOffset inputSize
Lowers through the existing audited bubblingValueCall ECM with outputOffset = 0 and outputSize = 0
Preserves the same generic_low_level_value_call_interface trust-report surface
Added Yul lowering and trust-report regression coverage plus docs updates

Validation passed locally:

lake build Compiler.Modules.Calls Compiler.CompilationModelFeatureTest
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T01:51:34Z

Added a focused regression for the no-output value-call convenience wrapper:

bubblingValueCallNoOutput is now covered as rejected from view functions, matching the underlying state-changing bubblingValueCall ECM.

Validation passed locally:

lake build Compiler.CompilationModelFeatureTest
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T02:02:03Z

Added one more pass on the value-call surface:

bubblingValueCallNoOutput is now backed by a first-class bubblingValueCallNoOutputModule with 4 arguments, so macro contracts can use it directly through ecmDo.
Shared the Yul lowering with bubblingValueCall, preserving exact revert-returndata bubbling and the same generic_low_level_value_call_interface assumption.
Added BubblingValueCallECMSmoke macro coverage plus invariant/round-trip coverage.
Added no-output bad-arity/trust-report regression coverage.
Excluded the new value-forwarding smoke from generated no-revert Foundry stubs because those stubs do not fund the deployed contract before making value calls.

Validation passed locally:

lake build Compiler.Modules.Calls Compiler.CompilationModelFeatureTest Contracts.Smoke Contracts.MacroTranslateInvariantTest Contracts.MacroTranslateRoundTripFuzz
lake build
python3 scripts/check_macro_property_test_generation.py --check
python3 scripts/check_macro_health.py
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T02:10:55Z

Added a correctness pass for the packed static-segment hashing helpers:

Sub-word abiEncodePackedStaticSegments / sha256PackedStaticSegments values are now masked to their explicit byte width before being left-aligned into memory.
This prevents high bits from leaking into packed preimages when callers pass a wider word than the segment width.
Updated Yul lowering assertions and docs to pin the truncation behavior.

Validation passed locally:

lake build Compiler.CompilationModelFeatureTest
lake build Compiler.Modules.Hashing Compiler.CompilationModelFeatureTest
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T02:25:17Z

Added macro-surface coverage for the packed static hash ECMs:

New Contracts.Smoke.PackedHashECMSmoke exercises abiEncodePackedStaticSegments for [20, 32] address+word packing and [1, 32] low-byte truncating packing.
The smoke also exercises sha256PackedStaticSegments for the [20, 32] SHA-256 precompile path.
Added pinned macro model-body assertions, selector/signature coverage, and round-trip fuzz coverage.
Excluded the new ECM smoke from generated no-revert property stubs, matching the existing ECM smoke treatment; this surface is covered by Lean macro/model tests rather than standalone generated Foundry stubs.

Validation passed locally:

lake build Contracts.Smoke.PackedHashECMSmoke Contracts.MacroTranslateInvariantTest Contracts.MacroTranslateRoundTripFuzz
python3 scripts/check_macro_property_test_generation.py --check
python3 scripts/check_macro_health.py
python3 scripts/generate_print_axioms.py --check
git diff --check
lake build
make check

Th0rgal · 2026-05-02T02:31:25Z

Added a small regression pass for the packed static-segment ECMs:

abiEncodePackedStaticSegmentsModule now has direct bad-arity coverage.
sha256PackedStaticSegmentsModule now has direct bad-arity coverage.
This complements the existing invalid-width tests and pins the direct Stmt.ecm diagnostics for macro/lower-level callers.

Validation passed locally:

lake build Compiler.CompilationModelFeatureTest
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T02:39:38Z

Added a BN254 proof-helper pass for the modField surface:

SNARK_SCALAR_FIELD_ne_zero
SNARK_SCALAR_FIELD_lt_modulus
modField_nat_eq
modField_lt
modField_eq_self_of_lt

These make the Unlink/Groth16 public-input reduction helper directly usable in downstream range and already-reduced-value proofs.

Validation passed locally:

lake build Verity.Proofs.Stdlib.Math
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T02:44:27Z

Added a small BN254 proof-helper pass for the modField surface:

modField_nat_mod_eq
modField_idempotent

These make repeated Groth16/public-input reduction proofs easier by exposing that modField values are already reduced and that applying modField twice is a no-op.

Validation passed locally:

lake build Verity.Proofs.Stdlib.Math
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T02:51:04Z

Added a small BN254 proof-helper pass for modField:

modField_zero
modField_SNARK_SCALAR_FIELD
modField_eq_of_nat_mod_eq

These avoid reopening the Nat modulo definition in downstream Groth16/public-input proofs when proving zero reductions or congruent public inputs reduce to the same field element.

Validation passed locally:

lake build Verity.Proofs.Stdlib.Math
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T02:55:35Z

Added a small BN254 proof-helper pass for modField:

modField_eq_zero_iff exposes zero reductions as an iff against the underlying natural-number modulo.
Updated arithmetic/API docs and regenerated PrintAxioms.lean.

Validation passed locally:

lake build Verity.Proofs.Stdlib.Math
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T03:10:33Z

Follow-up validation after the latest review pass:

Added modField_eq_iff_nat_mod_eq for rewriting BN254 field-reduction equality goals in either direction.
Fixed the Bugbot-reported sha256MemoryModule double evaluation of outputOffset by binding it once to __sha256_output_offset before the staticcall, then reusing the same temp for mload.
Added Yul regression assertions for the single-evaluation SHA-256 output offset shape.

Local validation passed:

lake build Verity.Proofs.Stdlib.Math
python3 scripts/generate_print_axioms.py
lake build Compiler.Modules.Precompiles Compiler.CompilationModelFeatureTest
lake build
python3 scripts/generate_print_axioms.py --check
git diff --check
make check

Th0rgal · 2026-05-02T03:12:49Z

Small docs consistency follow-up after the modField_eq_iff_nat_mod_eq proof-helper addition:

Added modField_eq_iff_nat_mod_eq to the docs-site EDSL API reference BN254 lemma list, matching docs/ARITHMETIC_PROFILE.md.

Validation passed locally:

git diff --check

…diness # Conflicts: # PrintAxioms.lean

cursor

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit dcd73c0. Configure here.}

…diness # Conflicts: # PrintAxioms.lean

Add generic Unlink audit readiness helpers

2afdfbd

Th0rgal added 2 commits May 1, 2026 22:33

Add missing macro smoke generated coverage

723fbbb

Add no-output bubbling value call helper

a81ed12

Cover no-output value call view rejection

157741f

Expose no-output value call module

94b5d54

Mask packed static segment values

f409b32

Cover packed hash ECM macro surface

d502b3f

Cover packed segment ECM arity errors

e342f31

Add modField proof lemmas

543d174

Add modField idempotence lemmas

4057f8d

Add modField zero congruence lemmas

7d2a1f4

Add modField zero iff lemma

7cb4176

cursor Bot reviewed May 2, 2026

View reviewed changes

Comment thread Compiler/Modules/Precompiles.lean Outdated

Th0rgal added 2 commits May 2, 2026 05:03

Add modField equality iff lemma

b9c4c46

Bind sha256 output offset once

63927f4

Document modField equality iff lemma

a61257b

cursor Bot reviewed May 2, 2026

View reviewed changes

Comment thread Compiler/Modules/Precompiles.lean Outdated

Th0rgal added 2 commits May 3, 2026 09:27

Fix sha256Memory temp scope

acd4a84

Merge remote-tracking branch 'origin/main' into unlink-audit-core-rea…

dcd73c0

…diness # Conflicts: # PrintAxioms.lean

cursor Bot reviewed May 3, 2026

View reviewed changes

Comment thread Compiler/Modules/Precompiles.lean

Th0rgal added 2 commits May 3, 2026 10:07

Scope sha256Memory internals across repeated calls

9040098

Merge remote-tracking branch 'origin/main' into unlink-audit-core-rea…

bbeb9c8

…diness # Conflicts: # PrintAxioms.lean

Th0rgal merged commit bfe702c into main May 3, 2026
6 of 7 checks passed

Th0rgal deleted the unlink-audit-core-readiness branch May 3, 2026 08:48

Conversation

Th0rgal commented May 1, 2026 • edited by cursor Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Trust Boundaries

Docs Changed

Tests Run

Uh oh!

github-actions Bot commented May 1, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Th0rgal commented May 2, 2026

Uh oh!

Uh oh!

cursor Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Th0rgal commented May 1, 2026 •

edited by cursor Bot

Loading