Add source-level internal function visibility

Compiler/CompilationModel/TrustSurface.lean

@@ -24,6 +24,14 @@ private def dedupEcmModules (items : List ECM.ExternalCallModule) : List ECM.Ext
   items.foldl (fun acc item => if acc.contains item then acc else acc ++ [item]) []
 
 private partial def collectLowLevelExprMechanics : Expr → List String
+  | .intrinsic _ (.builtin "create2") _ args =>
+      ["create2"] ++ args.flatMap collectLowLevelExprMechanics
+  | .intrinsic _ (.builtin "extcodecopy") _ args =>
+      ["extcodecopy"] ++ args.flatMap collectLowLevelExprMechanics
+  | .intrinsic _ (.builtin "codecopy") _ args =>
+      ["codecopy"] ++ args.flatMap collectLowLevelExprMechanics
+  | .intrinsic _ _ _ args =>
+      args.flatMap collectLowLevelExprMechanics
   | .call gas target value inOffset inSize outOffset outSize =>
       ["call"] ++ collectLowLevelExprMechanics gas ++ collectLowLevelExprMechanics target ++
         collectLowLevelExprMechanics value ++ collectLowLevelExprMechanics inOffset ++
@@ -94,6 +102,8 @@ private partial def collectLowLevelExprMechanics : Expr → List String
       []
 
 private partial def collectAxiomatizedExprPrimitives : Expr → List String
+  | .intrinsic _ _ _ args =>
+      args.flatMap collectAxiomatizedExprPrimitives
   | .keccak256 offset size =>
       ["keccak256"] ++ collectAxiomatizedExprPrimitives offset ++ collectAxiomatizedExprPrimitives size
   | .call gas target value inOffset inSize outOffset outSize =>
@@ -176,8 +186,8 @@ private def isUnsafeBoundaryMechanic (mechanic : String) : Bool :=
   match mechanic with
   | "call" | "staticcall" | "delegatecall"
   | "returndataSize" | "returndataCopy" | "revertReturndata" | "returndataOptionalBoolAt"
-  | "mload" | "mstore" | "calldataload" | "calldatacopy"
-  | "extcodesize" | "tload" | "tstore" => true
+  | "mload" | "mstore" | "calldataload" | "calldatacopy" | "codecopy"
+  | "extcodesize" | "extcodecopy" | "create2" | "tload" | "tstore" => true
   | _ => false
 
 /-- Collect assembly-shaped low-level mechanics that require an explicit local obligation. -/
@@ -276,7 +286,8 @@ def collectUnsafeBlockReasons (spec : CompilationModel) : List String :=
 
 private def isLinearMemoryMechanic (mechanic : String) : Bool :=
   match mechanic with
-  | "mload" | "mstore" | "calldatacopy" | "returndataCopy" | "returndataOptionalBoolAt" => true
+  | "mload" | "mstore" | "calldatacopy" | "codecopy" | "extcodecopy"
+  | "returndataCopy" | "returndataOptionalBoolAt" => true
   | _ => false
 
 private def collectLinearMemoryMechanicsFromMechanics (mechanics : List String) : List String :=
@@ -374,7 +385,7 @@ def collectEventEmissionMechanics (spec : CompilationModel) : List String :=
 
 private def isDeniedLowLevelMechanic (mechanic : String) : Bool :=
   match mechanic with
-  | "call" | "staticcall" | "delegatecall" | "returndataSize" | "returndataCopy"
+  | "call" | "staticcall" | "delegatecall" | "create2" | "returndataSize" | "returndataCopy"
   | "revertReturndata" | "rawRevert" | "returndataOptionalBoolAt" | "blobbasefee" => true
   | _ => false
 

Compiler/CompilationModel/Types.lean

@@ -572,7 +572,10 @@ inductive LowLevelMechanic where
   | mstore
   | calldataload
   | calldatacopy
+  | codecopy
   | extcodesize
+  | extcodecopy
+  | create2
   | tload
   | tstore
   | rawLog
@@ -599,7 +602,10 @@ def toReportString : LowLevelMechanic → String
   | .mstore => "mstore"
   | .calldataload => "calldataload"
   | .calldatacopy => "calldatacopy"
+  | .codecopy => "codecopy"
   | .extcodesize => "extcodesize"
+  | .extcodecopy => "extcodecopy"
+  | .create2 => "create2"
   | .tload => "tload"
   | .tstore => "tstore"
   | .rawLog => "rawLog"

Compiler/CompilationModelFeatureTest.lean

@@ -6173,6 +6173,25 @@ set_option maxRecDepth 4096 in
     (contains macroCallWithValueTrustReport "\"module\":\"callWithValue\"" &&
       contains macroCallWithValueTrustReport "\"module\":\"callWithValueBytes\"" &&
       contains macroCallWithValueTrustReport "\"assumption\":\"generic_call_with_value_interface\"")
+  let macroCreate2SSTORE2Yul ←
+    expectCompileToYul "macro create2/SSTORE2 smoke spec" Contracts.Smoke.Create2SSTORE2Smoke.spec
+  expectTrue "macro create2 surface lowers to the create2 builtin"
+    (contains macroCreate2SSTORE2Yul "create2(value, initOffset, initSize, salt)")
+  expectTrue "macro SSTORE2 read surface lowers to extcodecopy"
+    (contains macroCreate2SSTORE2Yul "extcodecopy(pointer, destOffset, codeOffset, size)")
+  let macroCreate2SSTORE2TrustReport := emitTrustReportJson [Contracts.Smoke.Create2SSTORE2Smoke.spec]
+  expectTrue "macro create2/SSTORE2 trust report surfaces code-as-data assumptions"
+    (contains macroCreate2SSTORE2TrustReport "\"module\":\"create2Deploy\"" &&
+      contains macroCreate2SSTORE2TrustReport "\"module\":\"sstore2ReadCode\"" &&
+      contains macroCreate2SSTORE2TrustReport "\"assumption\":\"create2_initcode_layout\"" &&
+      contains macroCreate2SSTORE2TrustReport "\"assumption\":\"sstore2_pointer_code_layout\"")
+  let macroCallbackYul ←
+    expectCompileToYul "macro callback ABI smoke spec" Contracts.Smoke.CallbackABISmoke.spec
+  expectTrue "macro callback ABI surface stores selector and bytes length"
+    (contains macroCallbackYul "mstore(__cb_ptr, shl(224, 0x12345678))" &&
+      contains macroCallbackYul "mstore(add(__cb_ptr, 68), data_length)")
+  expectTrue "macro callback ABI surface copies calldata bytes payload"
+    (contains macroCallbackYul "calldatacopy(add(__cb_ptr, 100), data_data_offset, data_length)")
   let erc20AllowanceYul ←
     expectCompileToYul "erc20 allowance smoke spec" erc20AllowanceSmokeSpec
   expectTrue "erc20 allowance ECM lowers to staticcall"

Compiler/Modules/Create2SSTORE2.lean

@@ -0,0 +1,48 @@
+/-
+  Compiler.Modules.Create2SSTORE2: CREATE2 and SSTORE2-style code-as-data helpers.
+
+  These ECMs expose the low-level source surface needed by code-as-data
+  contracts without requiring downstream projects to patch generated Yul.
+-/
+
+import Compiler.ECM
+import Compiler.CompilationModel
+
+namespace Compiler.Modules.Create2SSTORE2
+
+open Compiler.Yul
+open Compiler.ECM
+
+/-- Deploy already-prepared initcode with `create2(value, offset, size, salt)` and
+    bind the deployed address word. The caller owns initcode layout and salt
+    semantics; this module only lowers the EVM mechanic. -/
+def deployModule (resultVar : String) : ExternalCallModule where
+  name := "create2Deploy"
+  numArgs := 4
+  resultVars := [resultVar]
+  writesState := true
+  readsState := false
+  axioms := ["create2_initcode_layout", "create2_address_derivation"]
+  compile := fun _ctx args => do
+    match args with
+    | [value, offset, size, salt] =>
+        pure [YulStmt.let_ resultVar (YulExpr.call "create2" [value, offset, size, salt])]
+    | _ =>
+        throw s!"create2Deploy expects 4 arguments, got {args.length}"
+
+/-- Copy deployed bytecode into memory with `extcodecopy(pointer, dest, offset, size)`.
+    This is the read half of SSTORE2-style code-as-data patterns. -/
+def readCodeModule : ExternalCallModule where
+  name := "sstore2ReadCode"
+  numArgs := 4
+  writesState := false
+  readsState := true
+  axioms := ["sstore2_pointer_code_layout"]
+  compile := fun _ctx args => do
+    match args with
+    | [pointer, destOffset, codeOffset, size] =>
+        pure [YulStmt.expr (YulExpr.call "extcodecopy" [pointer, destOffset, codeOffset, size])]
+    | _ =>
+        throw s!"sstore2ReadCode expects 4 arguments, got {args.length}"
+
+end Compiler.Modules.Create2SSTORE2

Compiler/Modules/README.md

@@ -15,6 +15,7 @@ structure that the compiler can plug in without modification.
 | `Precompiles.lean` | `ecrecover`, `sha256Memory` / `sha256`, `bn256Add`, `bn256ScalarMul`, `bn256Pairing` | `Stmt.ecrecover`, handwritten SHA-256 / BN254 (alt_bn128) precompile calls |
 | `Callbacks.lean` | `callback` | `Stmt.callback` |
 | `Calls.lean` | `withReturn`, `callWithValue`, `callWithValueBytes`, `bubblingValueCall`, `bubblingValueCallNoOutput` | `Stmt.externalCallWithReturn`; generic `call{value:v}` adapter calls; handwritten low-level `call{value: ...}` wrappers |
+| `Create2SSTORE2.lean` | `create2Deploy`, `sstore2ReadCode` | handwritten CREATE2 deployment and SSTORE2-style `extcodecopy` code-as-data reads |
 
 ## Usage
 

Contracts/Smoke.lean

@@ -11,6 +11,8 @@ import Contracts.SimpleToken.SimpleToken
 import Contracts.ERC20.ERC20
 import Contracts.ERC721.ERC721
 import Compiler.Modules.Calls
+import Compiler.Modules.Callbacks
+import Compiler.Modules.Create2SSTORE2
 import Compiler.Modules.ERC20
 import Compiler.Modules.Oracle
 import Compiler.Modules.Precompiles
@@ -92,6 +94,38 @@ verity_contract MixedMappingChainSmoke where
     let current ← getMappingN approvals [addressToWord owner, tokenId, addressToWord delegate_]
     return current
 
+verity_contract FixedArrayMappingStructSmoke where
+  storage
+    rows : MappingStruct(Uint256,[
+      owner : Address @word 0,
+      roots : FixedArray Bytes32 2 @word 1,
+      proof : FixedArray (FixedArray Uint256 2) 2 @word 3
+    ]) := slot 0
+
+  function writeRoot1 (id : Uint256, root : Bytes32) : Unit := do
+    setStructMember "rows" id "roots[1]" root
+
+  function readRoot1 (id : Uint256) : Bytes32 := do
+    let root ← structMember "rows" id "roots[1]"
+    return root
+
+  function writeProof11 (id : Uint256, value : Uint256) : Unit := do
+    setStructMember "rows" id "proof[1][1]" value
+
+  function readProof11 (id : Uint256) : Uint256 := do
+    let value ← structMember "rows" id "proof[1][1]"
+    return value
+
+example :
+    FixedArrayMappingStructSmoke.spec.fields.any (fun field =>
+      field.name == "rows" &&
+        match field.ty with
+        | Compiler.CompilationModel.FieldType.mappingStruct
+            Compiler.CompilationModel.MappingKeyType.uint256 members =>
+            members.any (fun member => member.name == "roots[1]" && member.wordOffset == 2) &&
+            members.any (fun member => member.name == "proof[1][1]" && member.wordOffset == 6)
+        | _ => false) = true := by decide
+
 verity_contract Bytes32Smoke where
   storage
     value : Uint256 := slot 0
@@ -2160,6 +2194,29 @@ verity_contract BubblingValueCallECMSmoke where
     ecmDo Compiler.Modules.Calls.bubblingValueCallNoOutputModule
       [addressToWord target, ethValue, inputOffset, inputSize]
 
+set_option linter.unusedVariables false in
+verity_contract Create2SSTORE2Smoke where
+  storage
+    lastPointer : Address := slot 0
+
+  function allow_post_interaction_writes deploy (value : Uint256, initOffset : Uint256, initSize : Uint256, salt : Uint256) : Address := do
+    let pointer ← ecmCall Compiler.Modules.Create2SSTORE2.deployModule
+      [value, initOffset, initSize, salt]
+    setStorageAddr lastPointer (wordToAddress pointer)
+    return wordToAddress pointer
+
+  function readCode (pointer : Address, destOffset : Uint256, codeOffset : Uint256, size : Uint256) : Unit := do
+    ecmDo Compiler.Modules.Create2SSTORE2.readCodeModule
+      [addressToWord pointer, destOffset, codeOffset, size]
+
+set_option linter.unusedVariables false in
+verity_contract CallbackABISmoke where
+  storage
+
+  function onAction (target : Address, amount : Uint256, data : Bytes) : Unit := do
+    ecmDo (Compiler.Modules.Callbacks.callbackModule 0x12345678 1 "data")
+      [addressToWord target, amount]
+
 set_option linter.unusedVariables false in
 verity_contract CallWithValueSmoke where
   storage
@@ -2549,13 +2606,16 @@ end SpecGenSmoke
 #check_contract HelperExternalArgumentSmoke
 #check_contract BlockTimestampSmoke
 #check_contract StructMappingSmoke
+#check_contract FixedArrayMappingStructSmoke
 #check_contract UintKeyStructMappingSmoke
 #check_contract ExternalCallSmoke
 #check_contract TryExternalCallSmoke
 #check_contract LinkedExternalDynamicArgSmoke
 #check_contract LinkedExternalProjectedArrayArgSmoke
 #check_contract NestedStructArrayProjectionSmoke
 #check_contract ExternalCallMultiReturn
+#check_contract Create2SSTORE2Smoke
+#check_contract CallbackABISmoke
 #check_contract Contracts.Vault
 
 example : TupleSmoke.setFromPair = (TupleSmoke.setFromPair : (Uint256 × Uint256) → Verity.Contract Unit) := rfl

README.md

@@ -93,6 +93,7 @@ Verity is complementary to these tools. It is for cases where you need mathemati
 | [veritylang.com](https://veritylang.com/) | Full documentation site |
 | [Solidity to Verity](https://veritylang.com/guides/solidity-to-verity) | Practical syntax and semantic mappings for Solidity ports |
 | [Production Solidity Patterns](https://veritylang.com/guides/production-solidity-patterns) | Agent guidance for production ports, reusable Verity features, and oracle/spec boundaries |
+| [docs/ARCHITECTURE.md](docs/ARCHITECTURE.md) | Contributor map for source features, proof layers, trust surfaces, and regression checks |
 | [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md) | Theorem counts, proof status, test coverage |
 | [docs/INTRINSICS.md](docs/INTRINSICS.md) | Consumer-owned opcode bindings and their trust model |
 | [docs/LOW_LEVEL_YUL.md](docs/LOW_LEVEL_YUL.md) | Policy for typed low-level primitives vs. raw Yul escape hatches |

Verity/Macro/Translate.lean

@@ -514,6 +514,39 @@ private def storageTypeFromSyntax (newtypes : Array NewtypeDecl) (structDecls :
         }
     | _ => throwErrorAt stx "invalid struct member declaration"
 
+  let rec storageStructMemberElementWords (memberName : String) : ValueType → CommandElabM Nat
+    | .uint256 | .int256 | .uint16 | .address | .bool | .bytes32 => pure 1
+    | .newtype _ baseType => storageStructMemberElementWords memberName baseType
+    | .fixedArray elemTy size => do
+        let elemWords ← storageStructMemberElementWords memberName elemTy
+        pure (elemWords * size)
+    | other =>
+        throwErrorAt ty
+          s!"mapping struct member '{memberName}' has unsupported storage type {repr other}; expected a word-like type or FixedArray of word-like types"
+
+  let rec expandStructMemberDecl (memberPrefix : String) (baseOffset : Nat) (memberTy : ValueType)
+      (packed : Option (Nat × Nat)) : CommandElabM (List StructMemberDecl) := do
+    match memberTy with
+    | .newtype _ baseType =>
+        expandStructMemberDecl memberPrefix baseOffset baseType packed
+    | .fixedArray elemTy size => do
+        if packed.isSome then
+          throwErrorAt ty s!"mapping struct fixed-array member '{memberPrefix}' cannot be packed"
+        let elemWords ← storageStructMemberElementWords memberPrefix elemTy
+        let nested ← (List.range size).mapM fun idx =>
+          expandStructMemberDecl s!"{memberPrefix}[{idx}]" (baseOffset + idx * elemWords) elemTy none
+        pure nested.flatten
+    | .uint256 | .int256 | .uint16 | .address | .bool | .bytes32 =>
+        pure [{ name := memberPrefix, ty := memberTy, wordOffset := baseOffset, packed := packed }]
+    | other =>
+        throwErrorAt ty
+          s!"mapping struct member '{memberPrefix}' has unsupported storage type {repr other}; expected a word-like type or FixedArray of word-like types"
+
+  let expandStructMembers (members : Array StructMemberDecl) : CommandElabM (List StructMemberDecl) := do
+    let expanded ← members.mapM fun member =>
+      expandStructMemberDecl member.name member.wordOffset member.ty member.packed
+    pure expanded.toList.flatten
+
   let storageArrayElemTypeFromValueType (elemTy : ValueType) : CommandElabM Compiler.CompilationModel.StorageArrayElemType :=
     match elemTy with
     | .uint256 => pure .uint256
@@ -541,12 +574,12 @@ private def storageTypeFromSyntax (newtypes : Array NewtypeDecl) (structDecls :
   | `(term| MappingStruct($keyTy:term,[ $[$members:verityStructMember],* ])) =>
       pure <| .mappingStruct
         (← keyTypeFromSyntax keyTy)
-        ((← members.mapM structMemberFromSyntax).toList)
+        (← expandStructMembers (← members.mapM structMemberFromSyntax))
   | `(term| MappingStruct2($outerKey:term,$innerKey:term,[ $[$members:verityStructMember],* ])) =>
       pure <| .mappingStruct2
         (← keyTypeFromSyntax outerKey)
         (← keyTypeFromSyntax innerKey)
-        ((← members.mapM structMemberFromSyntax).toList)
+        (← expandStructMembers (← members.mapM structMemberFromSyntax))
   | _ => do
       let vt ← valueTypeFromSyntax newtypes structDecls adtDecls ty
       match vt with

artifacts/macro_property_tests/PropertyCreate2SSTORE2Smoke.t.sol

@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyCreate2SSTORE2SmokeTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke.lean
+ */
+contract PropertyCreate2SSTORE2SmokeTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("Create2SSTORE2Smoke");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: readCode has no unexpected revert
+    function testAuto_ReadCode_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("readCode(address,uint256,uint256,uint256)", alice, uint256(1), uint256(1), uint256(1)));
+        require(ok, "readCode reverted unexpectedly");
+    }
+}

artifacts/macro_property_tests/PropertyFixedArrayMappingStructSmoke.t.sol

@@ -0,0 +1,50 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyFixedArrayMappingStructSmokeTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke.lean
+ */
+contract PropertyFixedArrayMappingStructSmokeTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("FixedArrayMappingStructSmoke");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: writeRoot1 has no unexpected revert
+    function testAuto_WriteRoot1_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("writeRoot1(uint256,bytes32)", uint256(1), bytes32(uint256(0xBEEF))));
+        require(ok, "writeRoot1 reverted unexpectedly");
+    }
+    // Property 2: TODO decode and assert `readRoot1` result
+    function testTODO_ReadRoot1_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("readRoot1(uint256)", uint256(1)));
+        require(ok, "readRoot1 reverted unexpectedly");
+        assertEq(ret.length, 32, "readRoot1 ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 3: writeProof11 has no unexpected revert
+    function testAuto_WriteProof11_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("writeProof11(uint256,uint256)", uint256(1), uint256(1)));
+        require(ok, "writeProof11 reverted unexpectedly");
+    }
+    // Property 4: TODO decode and assert `readProof11` result
+    function testTODO_ReadProof11_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("readProof11(uint256)", uint256(1)));
+        require(ok, "readProof11 reverted unexpectedly");
+        assertEq(ret.length, 32, "readProof11 ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+}