| name | foundry-spec-properties |
| description | Turn whitepapers, protocol specs, and public documentation into Foundry property tests. Use when Codex needs to derive invariants, conservation rules, atomicity rules, priority rules, price-view behavior, or accounting properties from external specs without weakening tests that expose production mismatches. |
Foundry Spec Properties
Source Handling
Use the current spec source the user names. If it is a URL, fetch or browse it when current access is required. Cite or record the exact source used in the work summary when the property depends on a spec claim.
Separate spec properties from unit/fuzz mirrors. Use a clear directory such as:
test/foundry/property/<spec-name>/
test/foundry/properties/
Follow the repository's existing directory convention when one exists.
Deriving Properties
Look for properties that remain true across many inputs:
- conservation of balances, reserves, shares, or locked amounts
- quote/preview functions matching execution
- batch atomicity and required-action rollback
- price priority, time priority, or path priority
- price bucket/view consistency
- add/remove or deposit/withdraw roundtrips
- permission and lifecycle transitions
- no accidental balance creation or loss
Prefer public semantics over implementation-specific mechanisms.
TDD Policy
Add the property test first. If it fails, do not fix production or relax the property in the same breath. Report whether the failure appears to be:
- invalid harness setup
- reference/spec modeling issue
- production/spec mismatch
- ambiguous spec language
Preserve strict equality unless the spec states a tolerance. Rounding-related failures should remain visible unless the user explicitly decides otherwise.
Validation
Run the focused property file with enough verbosity to capture the counterexample. Then run the property subtree or full Foundry suite as appropriate.
