Model keccak256 opcode, unaligned calldata, and SHA-256 engine in executable semantics#1943
Merged
Conversation
Surface declared raw-Yul storage writes in the modifies() write-set, flag computed-slot writes as untrackable, and treat fragment call mechanics as external interactions for CEI ordering and external-call detection.
…ntics Make evalExpr/evalExprWithHelpers evaluate Expr.keccak256 via the in-tree KeccakEngine over a word-aligned RuntimeState memory slice, instead of returning none (revert). Adds keccakMemorySlice/memorySliceBytesBE/wordToBytesBE helpers; updates evalExpr_keccak256 and the helper-surface equivalence case. No new axiom or sorry: reuses the CI-cross-checked kernel Keccak. Trust docs (AXIOMS.md, TRUST_ASSUMPTIONS.md) updated to record the word-aligned-access faithfulness assumption (keccak256_memory_slice_matches_evm). Builds green: SourceSemantics + 8 reverse-dependency importers + SphincsMinusVerifiers.
Pure-Lean, axiom-free SHA-256 over ByteArray (Sha256Engine.sha256), mirroring KeccakEngine's role: prerequisite for modeling the EVM SHA-256 precompile (0x02) in the executable source semantics with a computed 32-byte digest. Verified against reference vectors (empty, "abc", quick-brown-fox, and the 56-byte padding-boundary case). UInt32 wrapping matches spec add-mod-2^32.
calldataloadWord now returns the EVM-faithful byte-addressed 32-byte window for unaligned offsets (r != 0), composing the hi/lo words with big-endian zero-padding. Aligned reads (r = 0) reduce to the prior single-word behaviour exactly. Needed for the C13 auth-path sibling reads at 16-byte-strided offsets in the Merkle-climb correspondence.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
2 tasks
Member
Author
|
@codex review |
|
To use Codex here, create a Codex account and connect to github. |
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…pport # Conflicts: # Compiler/CompilationModel/Types.lean # Compiler/CompilationModel/Validation.lean # Compiler/CompilationModelFeatureTest.lean
…e-Yul review invariants ff6c9c0 swapped calldataloadWord's aligned/unaligned branches (r = 0 now selects the aligned word) but left calldataloadWord_lt_evmModulus expecting the old layout, breaking the build at FunctionBody.lean:1969. Both branches now reduce mod evmModulus, so each discharges via Nat.mod_lt. Also document two invariants raised in the PR #1943 review: - LogicalPurity: raw Yul is emitted verbatim, so the logicalAnd/logicalOr/ite operand-duplication predicate correctly returns false; fragment external calls are caught in Validation, not here. - SourceSemantics: the keccak256 arm must evaluate offset/size with evalExpr to stay definitionally equal to evalExpr, because exprTouchesUnsupportedHelperSurface treats keccak256 as a helper-surface leaf and evalExprWithHelpers_eq_evalExpr depends on it.
Add a first-class, documented source-level interface that reuses the once-proved global helper-summary catalog across every selector-dispatched caller and call site: - SupportedSpecHelperProofs.helperCallSummarySound delivers summary soundness at an arbitrary helper call site of any selector-dispatched function, sourced purely from the shared catalog carried in SupportedSpecHelperProofs. - evalInternalCallObeysSummary / execInternalCallObeysSummary / execInternalCallAssignObeysSummary specialise that fact to the three helper call shapes (expression, void statement, assigning statement), landing the helper's summary contract directly on the interpreter result. This is the cross-caller proof reuse that whole-contract correctness needs: a helper proved once is consumed at each call without re-discharging its summary. The compiled-side body proof still reduces through the helper-closed SupportedStmtList fragment, so retargeting it to consume this reuse remains the tracked next step; the trusted boundary is unchanged. Contract.lean comments updated to reflect the now-available reuse interface.
…1747) Higher-order internal calls (helpers with function-pointer parameters) are now supported by a compile-time monomorphization pre-pass over the parsed FunctionDecl array, run before any model/IR lowering. For each call site that passes a statically-known internal helper in a function-pointer position, a first-order clone of the higher-order helper is synthesized (function-pointer parameters dropped, each occurrence replaced by the concrete helper) and the call site is rewritten to target the clone. Specialization runs to a fixpoint; the resulting helpers are topologically ordered so executable emission keeps callee-before-caller. Nothing downstream ever sees a function pointer, so the existing first-order machinery and proofs apply unchanged, with zero overhead when no helper is higher-order. Dynamic dispatch (a runtime value or expression in function-pointer position) still fails fast with a clear #1747 diagnostic. Tests: positive FunctionPointerParamSmoke #check_contract plus a focused negative test (FunctionPointerDynamicArgRejected) in Contracts/Smoke.lean, and a worked HigherOrderDemo contract in CompilationModelFeatureTest.lean asserting the monomorphized model shape and the executable result double(double(5)) = 20. Docs: ROADMAP.md and VERIFICATION_STATUS.md updated for #1747, and also for the #1630 helper-summary reuse interface now consumed at every call site (SupportedSpecHelperProofs.helperCallSummarySound and its three source-semantics call-shape lemmas evalInternalCallObeysSummary / execInternalCallObeysSummary / execInternalCallAssignObeysSummary).
…eference Document the author-facing surface the recent work added but left undocumented: - Higher-order internal helpers (#1747): function-pointer parameters, passing a helper by name, and the monomorphization restriction (statically-known callee only; #1747 diagnostic on dynamic dispatch). - Linked-external call forms: externalCall (single-word value position), tryExternalCall (prepended success flag, multi-return), and externalCallBind (statement position, no-return). Corrects stale prose that claimed at-most-one-return and rejected dynamic args; Array/Bytes arguments and multi-return are supported today. Cross-links the generic foreign-call surface to the named ECM module catalog.
There was a problem hiding this comment.
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 cebef44. Configure here.
…eview) - generate_macro_property_tests: skip higher-order (#1747) internal helpers, which are monomorphized away before lowering and have no external ABI signature to exercise; emitting one crashed the generator. Adds the generated PropertyFunctionPointerParamSmoke.t.sol and a regression test. - check_proof_length: allowlist two #1630 single-delegation theorems whose reported span is inflated by the next theorem's doc-comment preamble. - SourceSemantics: give the three #1630 helper-call corollaries (expression / void-stmt / assigning-stmt) shape-specific first conjuncts so their types are genuinely distinct, instead of three identical summary-only conclusions (Bugbot). The summary fact is still reused via helperCallSummarySound.
…ities/diagnostics pages Agent-facing docs reorganization so contract authors land on verity_contract as the canonical surface and can route by intent. - Add CanonicalSurface + TaskRouter components; surface "which surface do I write?" and the three journeys (start from an idea, port Solidity, prove an existing contract) on index, getting-started, first-contract, solidity-to-verity, and llms.txt. - New Capabilities & Limits page: expressible vs partial vs trust-boundary vs unsupported, plus the deny-flag table for staying in the proved subset. - New Diagnostics page: compiler / macro / linker error -> cause -> fix index. - Add a golden minimal contract skeleton (storage + function + spec + proof + register) in first-contract; label the monad/spec/proof forms as the proof layer beneath verity_contract. - Make trust-model canonical for Layer 1/2/3; trim the architecture re-teach to one sentence + link. - Fix stale Compiler/Specs.lean references to Contracts/Specs.lean (docs pages and generate_contract.py scaffold output/comments). - INTERPRETER_FEATURE_MATRIX: #1630 helper-summary reuse is now a first-class proof interface (helperCallSummarySound + three call-shape corollaries).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Extends Verity's executable source semantics with the hash/calldata
primitives the SPHINCS- C13 accept-path refinement needs. Enables the
keccak accept path to be executed (and thus proved) rather than
reverting at the first hash.
keccak256(offset,size)modeled (SourceSemantics.lean): newkeccakMemorySlice/memorySliceBytesBE/wordToBytesBEhelpers and.keccak256arms inevalExpr/evalExprWithHelpers, wired to thein-tree
KeccakEngine. Previously the first keccak madeexecStmtrevert, making the accept subdomain provably unreachable.
calldataloadWord(Calldata.lean): EVM-faithfulbyte-addressed 32-byte window for unaligned offsets (
r != 0), composinghi/lo words big-endian with zero-padding. Aligned reads (
r = 0) reduceto the prior single-word behaviour exactly. Needed for C13 auth-path
sibling reads at 16-byte-strided offsets.
Compiler/Sha256/Engine.lean),FIPS 180-4, verified against reference vectors. Infrastructure only — the
SHA-256 precompile (0x02) is deliberately NOT wired into the interpreter
yet (word-keyed memory cannot faithfully represent SLH-DSA's 16-byte
precompile-input layout).
Trust docs (
AXIOMS.md/TRUST_ASSUMPTIONS.md) updated forkeccak256_memory_slice_matches_evm. No newsorry; keccak engine iscross-checked against the EVM engine.
Internal-helper proof composition & higher-order helpers
(
SourceSemantics.lean,Contract.lean): a first-class source-levelinterface that threads the once-proved global helper-summary catalog
(
SupportedHelperSummaryProofCatalog, carried bySupportedSpecHelperProofs)through to every selector-dispatched caller and call site.
SupportedSpecHelperProofs.helperCallSummarySounddelivers summarysoundness at an arbitrary helper call site, and
evalInternalCallObeysSummary/
execInternalCallObeysSummary/execInternalCallAssignObeysSummaryspecialise it to the three helper call shapes (expression, void statement,
assigning statement), landing the helper's summary contract directly on the
interpreter result. A helper proved once is now consumed at each call without
re-discharging its summary. The compiled-side body proof still reduces through
the helper-closed
SupportedStmtListfragment, so retargeting it to consumethis reuse is the tracked next step; the trusted boundary is unchanged.
verity_contractrejects function-pointer parameters #1747)(
Verity/Macro/Translate.lean): a compile-time monomorphization pre-pass overthe parsed
FunctionDeclarray, run before any model/IR lowering. For eachcall site that passes a statically-known internal helper in a function-pointer
position, a first-order clone of the higher-order helper is synthesized
(function-pointer params dropped, each occurrence replaced by the concrete
helper) and the call site is rewritten to target the clone. Specialization runs
to a fixpoint and the resulting helpers are topologically ordered so executable
emission keeps callee-before-caller. Nothing downstream ever sees a function
pointer, so the existing first-order machinery and proofs apply unchanged, with
zero overhead when no helper is higher-order. Dynamic dispatch (a runtime value
or expression in function-pointer position) still fails fast with a clear
verity_contractrejects function-pointer parameters #1747diagnostic.
Author-facing usage docs
EDSL reference clarified for external calls and internal helpers
(
docs-site/content/edsl-api-reference.mdx): documents the higher-orderinternal-helper surface from
verity_contractrejects function-pointer parameters #1747 (function-pointer parameters, passing ahelper by name, and the static-callee-only restriction with its
verity_contractrejects function-pointer parameters #1747diagnostic), and the three linked-external call forms —
externalCall(single-word value position),
tryExternalCall(prependedsuccessflag,multi-return), and
externalCallBind(statement position, no return).Corrects now-stale prose that claimed at-most-one return and rejected dynamic
arguments;
Array/Bytesarguments and multi-return are supported today.Cross-links the generic foreign-call surface to the named ECM module catalog.
Documentation only — describes already-shipped behavior, so no trust/axiom
boundary changes.
Agent-facing docs reorganization (
docs-site/): namesverity_contractas the canonical authoring surface and routes authors by intent.
CanonicalSurface+TaskRoutercomponents surface "which surface doI write?" and the three journeys (start from an idea, port from Solidity,
prove an existing contract) on
index,getting-started,first-contract,solidity-to-verity, andllms.txt.capabilities.mdx): expressible vspartial vs trust-boundary vs unsupported, plus the deny-flag table for
staying inside the proved subset.
diagnostics.mdx): compiler / macro / linkererror → cause → fix index.
register) in
first-contract; the monad/spec/proof forms are labelled asthe proof layer beneath
verity_contract.trust-modelis now canonical for the Layer 1/2/3 split; thearchitecturere-teach is trimmed to one sentence + link.
Compiler/Specs.leanreferences to the realContracts/Specs.lean(docs pages +generate_contract.pyscaffold output).INTERPRETER_FEATURE_MATRIXupdated: Layer 2 follow-on: replace SupportedSpec feature exclusions with compositional proof interfaces and widen coverage toward the full EDSL image #1630 helper-summary reuse is now afirst-class proof interface (
helperCallSummarySound+ three corollaries).Documentation only — no trust/axiom boundary changes.
Review & CI follow-ups
SourceSemantics.lean): the threeLayer 2 follow-on: replace SupportedSpec feature exclusions with compositional proof interfaces and widen coverage toward the full EDSL image #1630 helper-call corollaries (
evalInternalCallObeysSummary/execInternalCallObeysSummary/execInternalCallAssignObeysSummary) nowcarry shape-specific first conjuncts (expression / void-statement /
assigning-statement reductions) so their types are genuinely distinct,
rather than three identical summary-only conclusions. The summary fact is
still reused once via
helperCallSummarySound.generate_macro_property_testsnow skips higher-order (verity_contractrejects function-pointer parameters #1747)internal helpers — they are monomorphized away before lowering, have no
external ABI signature to exercise, and previously crashed the generator (adds
a regression test + the generated
PropertyFunctionPointerParamSmoke.t.sol).check_proof_lengthallowlists two Layer 2 follow-on: replace SupportedSpec feature exclusions with compositional proof interfaces and widen coverage toward the full EDSL image #1630 single-delegation theorems whosereported span is inflated by the next theorem's doc-comment preamble.
Test plan
lake buildofSourceSemantics+ reverse-dep importers greenSphincsMinusVerifiersbuilds against this branchhelperCallSummarySound+ threecall-shape specializations) build green in
SourceSemantics.leanverity_contractrejects function-pointer parameters #1747 monomorphization: positiveFunctionPointerParamSmoke#check_contract, negativeFunctionPointerDynamicArgRejected, and theworked
HigherOrderDemomodel/executable assertion (double(double(5)) = 20)linked-external call-form sections
make check(CI-equivalent) green — incl. macro-health, storage-layout,path, and interpreter-feature-summary/boundary sync checks
generate_macro_property_testsregression test green; higher-order(
verity_contractrejects function-pointer parameters #1747) helpers skipped;PropertyFunctionPointerParamSmoke.t.solcleanfix;
lake buildre-verified greenCanonicalSurface/TaskRoutercomponents) — not run in this updateNote
Medium Risk
Changes executable source semantics (keccak, calldata) and compiler validation/CEI for raw Yul, plus macro monomorphization; well-tested and documented but affects verification reach and contract elaboration behavior.
Overview
This PR widens what Verity can execute and reason about in the source interpreter and tightens validation around raw Yul, while adding proof plumbing for internal helpers.
Hash and calldata.
Expr.keccak256no longer always reverts:evalExpr/evalExprWithHelpershash a word-aligned memory slice viakeccakMemorySliceand the in-treeKeccakEngine. Trust docs describe the word-alignedkeccak256_memory_slice_matches_evmassumption.calldataloadWordis updated for unaligned byte windows (hi/lo composition); aligned reads stay behaviorally the same. A new FIPS 180-4 SHA-256 engine (with smoke tests pulled intoCompiler.lean) is infrastructure only—the precompile is not hooked into the interpreter yet.Helpers (#1747, #1630). The macro runs a monomorphization pre-pass before lowering: higher-order internal helpers with a statically known callee name become first-order clones; dynamic function-pointer arguments still error. In proofs,
SupportedSpecHelperProofsgainshelperCallSummarySoundand three call-site corollaries so once-proved helper summaries reuse at every caller;SupportedSpectreats plainkeccak256as supported on helper/call surfaces (only operand subexpressions are scanned).Validation. Raw Yul gets an AST scan for
call/staticcall/delegatecallso CEI and external-call checks do not rely only on fragment metadata;unsafeYulno longer triggers misleading logical-purity “duplicate operand” diagnostics.Reviewed by Cursor Bugbot for commit cebef44. Bugbot is set up for automated code reviews on this repo. Configure here.