feat(importer): apply modifiers in order and encode user structs

AUDIT.md

@@ -53,7 +53,9 @@ source, Lean importer, specification, execution proofs and focused acceptance
 tests. It is independent of the handwritten `Contracts/Vault` example. The S1
 inheritance slice adds `Contracts/SolidityImportSmoke/Inheritance` with the same
 shape (source, import command, named-storage spec, proofs, focused Python
-suite). No
+suite). The S2 modifiers/structs slice adds
+`Contracts/SolidityImportSmoke/Modifiers` and
+`Contracts/SolidityImportSmoke/Structs` with the same shape. No
 Python frontend, custom serialized IR, generated Lean source, or bytecode is in
 the translation path: the accepted Solidity subset is the kernel-checked
 inductive in `Importer/Syntax.lean` and `Importer/Semantics.lean` is its single
@@ -63,6 +65,13 @@ meaning. Trust and axiom scope are recorded in
 Evidence command for the inheritance slice:
 `python3 Contracts/SolidityImportSmoke/Inheritance/scripts/inheritance_test.py`
 (after `lake build SolidityImportSmokeInheritance`).
+Evidence commands for the modifiers/structs slice:
+`python3 Contracts/SolidityImportSmoke/Modifiers/scripts/modifiers_test.py`
+(after `lake build SolidityImportSmokeModifiers`) and
+`python3 Contracts/SolidityImportSmoke/Structs/scripts/structs_test.py`
+(after `lake build SolidityImportSmokeStructs`). The structs suite also
+imports a named constructor that lists `{who, amount}` out of member order
+(`Expr.pairRev` evaluates source order then packs `uint256 × address`).
 
 ## Current Audit State
 

AXIOMS.md

@@ -15,7 +15,10 @@ and `Quot.sound`; they do not depend on `solidityMappingSlot_injective`.
 `solvent_invariant` is included in that audit. The inheritance-slice suite
 `inheritance_test.py` runs the same `#print axioms` gate on every theorem in
 `Contracts/SolidityImportSmoke/Inheritance/Proofs.lean` and likewise requires
-only `propext` and `Quot.sound`. This does not remove the trusted Solidity frontend/translation boundary described
+only `propext` and `Quot.sound`. The modifiers and structs suites
+`modifiers_test.py` and `structs_test.py` run the same gate on
+`Contracts/SolidityImportSmoke/Modifiers/Proofs.lean` and
+`Contracts/SolidityImportSmoke/Structs/Proofs.lean`. This does not remove the trusted Solidity frontend/translation boundary described
 in `TRUST_ASSUMPTIONS.md`, or change the compiler axiom registry below.
 
 ## Policy

Contracts/SolidityImportSmoke/Modifiers/Modifiers.lean

@@ -0,0 +1,7 @@
+import Contracts.VaultFromSolidity.Importer.Importer
+
+namespace Contracts.SolidityImportSmoke.Modifiers
+
+solidity_contract Child from "Modifiers.sol"
+
+end Contracts.SolidityImportSmoke.Modifiers

Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol

@@ -0,0 +1,93 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+error NotOwner();
+error EnforcedPause();
+error ReentrancyGuardReentrantCall();
+
+abstract contract OwnableLike {
+    address public owner;
+
+    modifier onlyOwner() {
+        if (msg.sender != owner) revert NotOwner();
+        _;
+    }
+}
+
+abstract contract PausableLike {
+    uint256 public paused;
+
+    modifier whenNotPaused() {
+        if (0 < paused) revert EnforcedPause();
+        _;
+    }
+}
+
+abstract contract ReentrancyGuardLike {
+    uint256 public status;
+
+    modifier nonReentrant() {
+        if (1 < status) revert ReentrancyGuardReentrantCall();
+        status = 2;
+        _;
+        status = 1;
+    }
+
+    modifier restore() {
+        uint256 old = status;
+        _;
+        status = old;
+    }
+}
+
+abstract contract HelperLike {
+    uint256 public helperValue;
+
+    modifier bumpHelper() {
+        bump();
+        _;
+    }
+
+    function bump() private {
+        helperValue = 1;
+    }
+}
+
+contract Child is OwnableLike, PausableLike, ReentrancyGuardLike, HelperLike {
+    uint256 public value;
+
+    function setOwner(address next) external {
+        owner = next;
+    }
+
+    function arm() external {
+        status = 1;
+    }
+
+    function guarded(uint256 amount) external onlyOwner whenNotPaused {
+        value = amount;
+    }
+
+    function enter(uint256 amount) external nonReentrant returns (uint256) {
+        value = amount;
+        return amount;
+    }
+
+    function early(uint256 amount) external nonReentrant returns (uint256) {
+        value = amount;
+        return amount;
+    }
+
+    function poison() private {
+        helperValue = 2;
+    }
+
+    function tagged() external bumpHelper {
+        value = 0;
+    }
+
+    function snapshot(uint256 amount) external restore returns (uint256) {
+        status = amount;
+        return amount;
+    }
+}

Contracts/SolidityImportSmoke/Modifiers/Proofs.lean

@@ -0,0 +1,75 @@
+import Contracts.SolidityImportSmoke.Modifiers.Spec
+import Verity.Proofs.Stdlib.SolidityImport
+
+namespace Contracts.SolidityImportSmoke.Modifiers.Proofs
+open Verity
+open Verity.Proofs.Stdlib.SolidityImport
+open Contracts.SolidityImportSmoke.Modifiers.Child
+open Spec
+
+theorem status_restored (s post : ContractState) (amount : Uint256)
+    (h : (early amount).run s = .success amount post) :
+    early_spec amount (view s) (view post) := by
+  unfold early_spec
+  by_cases h0 : s.msgValue = 0
+  · by_cases hst : 1 < (view s).status.val
+    · solidity_simp
+    · solidity_simp
+      subst h
+      solidity_simp
+  · solidity_simp
+
+theorem early_meets_spec (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0) (harmed : (view s).status = 1) :
+    ∃ post, (early amount).run s = ContractResult.success amount post ∧
+      early_spec amount (view s) (view post) := by
+  unfold early_spec
+  solidity_simp
+
+theorem guarded_success_spec (s post : ContractState) (amount : Uint256)
+    (h : (guarded amount).run s = .success () post) :
+    guarded_spec amount (view s) (view post) := by
+  unfold guarded_spec
+  by_cases h0 : s.msgValue = 0
+  · by_cases ho : s.sender = (view s).owner
+    · by_cases hp : (view s).paused.val = 0
+      · solidity_simp
+        subst h
+        solidity_simp
+      · solidity_simp
+    · by_cases hp : (view s).paused.val = 0
+      · solidity_simp
+      · solidity_simp
+  · solidity_simp
+
+theorem guarded_reverts_not_owner_before_pause (s : ContractState) (amount : Uint256)
+    (h0 : s.msgValue = 0)
+    (howner : s.sender ≠ (view s).owner)
+    (hpaused : 0 < (view s).paused.val) :
+    (guarded amount).run s = ContractResult.revert "NotOwner()" s := by
+  by_cases ho : s.sender = (view s).owner
+  · exact (howner ho).elim
+  · have := hpaused
+    solidity_simp
+
+theorem tagged_uses_base_helper (s post : ContractState)
+    (h : tagged.run s = .success () post) :
+    tagged_spec (view s) (view post) := by
+  unfold tagged_spec
+  by_cases h0 : s.msgValue = 0
+  · solidity_simp
+    subst h
+    solidity_simp
+  · solidity_simp
+
+theorem snapshot_restores_status (s post : ContractState) (amount : Uint256)
+    (h : (snapshot amount).run s = .success amount post) :
+    snapshot_spec amount (view s) (view post) := by
+  unfold snapshot_spec
+  by_cases h0 : s.msgValue = 0
+  · solidity_simp
+    subst h
+    solidity_simp
+  · solidity_simp
+
+end Contracts.SolidityImportSmoke.Modifiers.Proofs

Contracts/SolidityImportSmoke/Modifiers/Spec.lean

@@ -0,0 +1,36 @@
+import Verity.EVM.Uint256
+import Contracts.SolidityImportSmoke.Modifiers.Modifiers
+
+namespace Contracts.SolidityImportSmoke.Modifiers.Spec
+
+open Verity
+open Verity.EVM.Uint256
+open Contracts.SolidityImportSmoke.Modifiers.Child
+
+def early_spec (amount : Uint256) (pre post : Storage) : Prop :=
+  post.status = 1 ∧
+  post.value = amount ∧
+  post.owner = pre.owner ∧
+  post.paused = pre.paused
+
+def guarded_spec (amount : Uint256) (pre post : Storage) : Prop :=
+  post.value = amount ∧
+  post.status = pre.status ∧
+  post.owner = pre.owner ∧
+  post.paused = pre.paused
+
+def tagged_spec (pre post : Storage) : Prop :=
+  post.helperValue = 1 ∧
+  post.value = 0 ∧
+  post.status = pre.status ∧
+  post.owner = pre.owner ∧
+  post.paused = pre.paused
+
+def snapshot_spec (_amount : Uint256) (pre post : Storage) : Prop :=
+  post.status = pre.status ∧
+  post.value = pre.value ∧
+  post.owner = pre.owner ∧
+  post.paused = pre.paused ∧
+  post.helperValue = pre.helperValue
+
+end Contracts.SolidityImportSmoke.Modifiers.Spec