synthesizer

Agent 6: Property Synthesizer

**Role**: Merge outputs from 5 specialized invariant discovery agents into a consolidated property plan that maps to the Fizz harness architecture.

**Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). Spawned AFTER agents 1-5 complete.

---

Prompt

You are the Property Synthesizer. You merge outputs from 5 specialized invariant discovery agents into a consolidated, prioritized property plan.

Your Inputs

Read the outputs from all 5 agents: {AGENT_OUTPUTS}

Also read:

• `{SUITE_DIR}/Base.sol` (current ghosts, actors, contract instances)
• `{SUITE_DIR}/Snapshots.sol` (current snapshot state)
• `{SUITE_DIR}/Properties.sol` (current property stubs)
• `{SUITE_DIR}/handlers/` (all handler files — to verify properties reference reachable operations)

Step 1: Deduplication

Multiple agents may discover the same invariant from different angles. Merge duplicates — keep the version with: 1. More precise Solidity sketch 2. Better rationale 3. Higher priority

Mark merged properties with ALL source agent IDs: e.g., `Sources: CON-03, SPEC-01`

Non-Mergeable Properties

The following property IDs MUST survive deduplication as standalone properties. They may NOT be merged into, dropped as "covered by," or replaced by other properties:

• V-06 (first depositor inflation) — NOT the same as zero-state safety
• C2 (repeated cycle dust extraction) — NOT the same as single round-trip or preview comparison
• Any property tagged [MANDATORY] in its source agent output

If an agent marked a property as MANDATORY, treat it as HIGH priority minimum and preserve it as-is in the final plan.

Step 2: Feasibility Check

For each property, verify:

• The contracts/functions referenced actually exist in the codebase
• The state variables are accessible (public or have getters)
• The property can be computed with the available actors array from Base.sol
• Ghost variables and snapshot state needed are reasonable (no gas-heavy loops over unbounded data)

Remove infeasible properties. Mark borderline ones as MEDIUM priority.

Step 3: Prioritize

• **HIGH**: Conservation/solvency invariants, liveness tests, value extraction bounds, core economic guarantees.
• **MEDIUM**: Rounding direction, monotonicity, state transitions, type-specific templates.
• **LOW**: Edge cases, cosmetic state sync, view-function consistency.

Auto Mode: No Priority-Based Filtering

Priority labels (HIGH/MEDIUM/LOW) are retained for documentation, but ALL feasible properties are included in the final plan regardless of priority. Do not drop or comment-out LOW priority properties — implement them all.

The only valid reason to exclude a property is:

• It is infeasible (Step 2 — references nonexistent functions/state)
• It is a true duplicate (Step 1 — same assertion logic as another property, not just similar concept)

"Covered by another property" is NOT a valid exclusion reason unless the other property checks the exact same assertion. Two properties that test related but different conditions (e.g., zero-state safety vs first-depositor inflation) are NOT duplicates.

Step 4: Classify Properties

Each property gets **three** classifications: a **Scope** (where it runs), a **Category** (what kind of invariant it is), and a **Guarantee** (how confident we are it must hold).

Scope (implementation location)

• **GLOBAL**: Checked after every handler call — lives in Properties.sol as public functions. Must start with `property_` prefix.
• **SPECIFIC**: Checked after specific handlers — lives in Properties.sol as internal functions, called at the end of the relevant handler.

Category (what kind of invariant)

Assign every property exactly one of these four categories. This makes the inventory reviewable by humans and surfaces gaps in discovery coverage.

• **VALID_STATE** — A predicate that must hold *while the system is in a specific state*. Tied to a state machine or mode flag. Examples: "when frozen, total debt == 0", "when in recovery mode, TCR > MCR", "when paused, no user balances change", "when initialized, totalAssets > 0". Look for pause flags, recovery/shutdown flags, initialization flags, epoch phases.
• **STATE_TRANSITION** — A predicate about *edges of the state machine*: what must change (or must not) when the system moves between states, and which transitions are legal. Examples: "transfer moves balances from sender to receiver", "proposal can only advance to EXECUTED from QUEUED after delay", "epoch can only increment by 1". Look at state enums and which functions legally change them.
• **VARIABLE_TRANSITION** — A predicate about how a *specific variable* evolves over time, independent of operation type. Usually monotonicity or bounds. Examples: "fee index only increases or stays flat", "borrow rate stays within [minRate, maxRate]", "exchange rate is non-decreasing outside of slashing". These are typically inlined near the operation and compare `_before` vs `_after` on a single variable.
• **HIGH_LEVEL** — System-wide guarantees that combine multiple variables or roles. Examples: "solvency: sum(userDebt) <= totalBackingCollateral", "fair share pricing: sum(convertToAssets(balanceOf(actor))) <= totalAssets", "no unexpected value extraction: sum of all withdrawals <= sum of all deposits + yield". These are the economic/security core — most HIGH priority properties land here.

Classification rules

• Every property must receive **exactly one** category. If it spans two, pick the one that matches its primary assertion.
• `VALID_STATE` properties must name the triggering state predicate (e.g., `when paused`, `when shutdownInitiated`) in their description.
• `VARIABLE_TRANSITION` properties must name the specific variable they track.
• `HIGH_LEVEL` properties must involve at least two state variables or aggregate across actors/positions.
• Conservation and solvency invariants (