feat(axis3): step 1d — annotation composition with _effects conjunction theorem

When a function has 2+ effect annotations (view, no_external_calls, modifies),
auto-generate an _effects theorem that bundles all individual effect facts into
a single And proposition, simplifying downstream proof automation.

- Add effectAnnotationCount and mkEffectsTheoremCommand in Bridge.lean
- Wire _effects emission in Elaborate.lean for functions with ≥2 annotations
- Add EffectCompositionSmoke test contract exercising all combinations
- Update MacroTranslateInvariantTest with specs, sigs, selectors, theorem checks
- Update MacroTranslateRoundTripFuzz with EffectCompositionSmoke.spec

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: claude

Contracts/MacroTranslateInvariantTest.lean

@@ -324,6 +324,7 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.Smoke.LocalObligationRequiredForUnsafeConstructorBoundary.spec
   , Contracts.Smoke.ModifiesSmoke.spec
   , Contracts.Smoke.NoExternalCallsSmoke.spec
+  , Contracts.Smoke.EffectCompositionSmoke.spec
   ]
 
 private def functionSignature (fn : FunctionSpec) : String :=
@@ -405,6 +406,7 @@ private def expectedExternalSignatures : List (String × List String) :=
   , ("LocalObligationRequiredForUnsafeConstructorBoundary", ["noop()"])
   , ("ModifiesSmoke", ["increment()", "transferOwnership(address)", "deposit(uint256)", "getCounter()"])
   , ("NoExternalCallsSmoke", ["increment()", "getCounter()", "setOwner(address)"])
+  , ("EffectCompositionSmoke", ["getCounter()", "increment()", "setOwner(address)", "deposit(uint256)"])
   ]
 
 private def expectedExternalSelectors : List (String × List String) :=
@@ -469,6 +471,7 @@ private def expectedExternalSelectors : List (String × List String) :=
   , ("LocalObligationRequiredForUnsafeConstructorBoundary", ["0x5dfc2e4a"])
   , ("ModifiesSmoke", ["0xd09de08a", "0xf2fde38b", "0xb6b55f25", "0x8ada066e"])
   , ("NoExternalCallsSmoke", ["0xd09de08a", "0x8ada066e", "0x13af4035"])
+  , ("EffectCompositionSmoke", ["0x8ada066e", "0xd09de08a", "0x13af4035", "0xb6b55f25"])
   ]
 
 private def expectedFor
@@ -519,6 +522,14 @@ private def checkMutabilitySmoke : IO Unit := do
   -- Verify auto-generated _no_calls theorem exists (#1729, Axis 3 Step 1c).
   let _ := @Contracts.Smoke.NoExternalCallsSmoke.increment_no_calls
   let _ := @Contracts.Smoke.NoExternalCallsSmoke.getCounter_no_calls
+  -- Verify auto-generated _effects conjunction theorem exists (#1729, Axis 3 Step 1d).
+  -- getCounter has view + no_external_calls → _effects bundles both
+  let _ := @Contracts.Smoke.EffectCompositionSmoke.getCounter_effects
+  -- increment has no_external_calls + modifies → _effects bundles both
+  let _ := @Contracts.Smoke.EffectCompositionSmoke.increment_effects
+  -- Also verify the existing NoExternalCallsSmoke.getCounter gets _effects
+  -- (it has view + no_external_calls)
+  let _ := @Contracts.Smoke.NoExternalCallsSmoke.getCounter_effects
 
 private def checkSignedBuiltinSmoke : IO Unit := do
   let functions := Contracts.Smoke.SignedBuiltinSmoke.spec.functions

Contracts/MacroTranslateRoundTripFuzz.lean

@@ -79,6 +79,7 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.Smoke.LowLevelTryCatchSmoke.spec
   , Contracts.Smoke.ModifiesSmoke.spec
   , Contracts.Smoke.NoExternalCallsSmoke.spec
+  , Contracts.Smoke.EffectCompositionSmoke.spec
   ]
 
 private structure FuzzRng where

Contracts/Smoke.lean

@@ -1680,4 +1680,31 @@ verity_contract NoExternalCallsSmoke where
   function setOwner (newOwner : Address) : Unit := do
     setStorageAddr owner newOwner
 
+-- #1729, Axis 3 Step 1d: smoke test for annotation composition (_effects theorem)
+verity_contract EffectCompositionSmoke where
+  storage
+    counter : Uint256 := slot 0
+    owner : Address := slot 1
+    balances : Address → Uint256 := slot 2
+
+  -- view + no_external_calls: _effects bundles _is_view ∧ _no_calls
+  function view no_external_calls getCounter () : Uint256 := do
+    let current ← getStorage counter
+    return current
+
+  -- no_external_calls + modifies: _effects bundles _no_calls ∧ _modifies
+  function no_external_calls increment () modifies(counter) : Unit := do
+    let current ← getStorage counter
+    setStorage counter (add current 1)
+
+  -- Single annotation only (no _effects expected)
+  function no_external_calls setOwner (newOwner : Address) : Unit := do
+    setStorageAddr owner newOwner
+
+  -- No annotations at all
+  function deposit (amount : Uint256) : Unit := do
+    let sender ← msgSender
+    let balance ← getMapping balances sender
+    setMapping balances sender (add balance amount)
+
 end Contracts.Smoke

Verity/Macro/Bridge.lean

@@ -133,4 +133,52 @@ def mkFrameDefCommand
 
   pure #[frameCmd, frameRflCmd]
 
+/-- Count how many effect annotations are active on a function declaration. -/
+def effectAnnotationCount (fnDecl : FunctionDecl) : Nat :=
+  (if fnDecl.isView then 1 else 0) +
+  (if fnDecl.noExternalCalls then 1 else 0) +
+  (if !fnDecl.modifies.isEmpty then 1 else 0)
+
+/-- Auto-generated `_effects` conjunction theorem for functions with multiple
+    effect annotations (#1729, Axis 3 Step 1d).  Bundles all individual effect
+    theorems (`_is_view`, `_no_calls`, `_modifies`) into a single `And` fact so
+    downstream proofs can obtain all guarantees in one `exact`. -/
+def mkEffectsTheoremCommand (fnDecl : FunctionDecl) : CommandElabM Cmd := do
+  let effectsName ← mkSuffixedIdent fnDecl.ident "_effects"
+  let modelName ← mkSuffixedIdent fnDecl.ident "_model"
+  -- Collect conjunct terms and proof terms for each active annotation
+  let mut conjuncts : Array Term := #[]
+  let mut proofs : Array Term := #[]
+  if fnDecl.isView then
+    let viewName ← mkSuffixedIdent fnDecl.ident "_is_view"
+    conjuncts := conjuncts.push (← `(
+        (Compiler.CompilationModel.FunctionSpec.isView
+          ($modelName : Compiler.CompilationModel.FunctionSpec)) = true))
+    proofs := proofs.push (← `($viewName))
+  if fnDecl.noExternalCalls then
+    let noCallsName ← mkSuffixedIdent fnDecl.ident "_no_calls"
+    conjuncts := conjuncts.push (← `(
+        (Compiler.CompilationModel.FunctionSpec.noExternalCalls
+          ($modelName : Compiler.CompilationModel.FunctionSpec)) = true))
+    proofs := proofs.push (← `($noCallsName))
+  if !fnDecl.modifies.isEmpty then
+    let modifiesName ← mkSuffixedIdent fnDecl.ident "_modifies"
+    let fieldTerms : Array Term := fnDecl.modifies.map fun ident => strTermPublic (toString ident.getId)
+    conjuncts := conjuncts.push (← `(
+        (Compiler.CompilationModel.FunctionSpec.modifies
+          ($modelName : Compiler.CompilationModel.FunctionSpec)) = [ $[$fieldTerms],* ]))
+    proofs := proofs.push (← `($modifiesName))
+  -- Build right-nested And: P₁ ∧ P₂ ∧ ... ∧ Pn
+  -- For n=2: And.intro p₁ p₂
+  -- For n=3: And.intro p₁ (And.intro p₂ p₃)
+  let mut propTerm := conjuncts[conjuncts.size - 1]!
+  for i in List.range (conjuncts.size - 1) |>.reverse do
+    propTerm ← `($(conjuncts[i]!) ∧ $propTerm)
+  let mut proofTerm := proofs[proofs.size - 1]!
+  for i in List.range (proofs.size - 1) |>.reverse do
+    proofTerm ← `(And.intro $(proofs[i]!) $proofTerm)
+  `(command|
+    @[simp] theorem $effectsName :
+        $propTerm := $proofTerm)
+
 end Verity.Macro

Verity/Macro/Elaborate.lean

@@ -71,6 +71,12 @@ def elabVerityContract : CommandElab := fun stx => do
         for cmd in frameCmds do
           elabCommand cmd
 
+    -- Emit per-function _effects conjunction theorem when multiple effect
+    -- annotations are active on the same function (#1729, Axis 3 Step 1d).
+    for fn in functions do
+      if effectAnnotationCount fn ≥ 2 then
+        elabCommand (← mkEffectsTheoremCommand fn)
+
     elabCommand (← `(end $contractName))
   catch err =>
     elabCommand (← `(end $contractName))

artifacts/macro_property_tests/PropertyEffectCompositionSmoke.t.sol

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