/ensure-invariants

name: "ensure-invariants"
description: "Trigger Pattern Always required for DAML audits - Inject Into Breadth agents, depth-edge-case"

ENSURE_INVARIANTS Skill (DAML)

> **Trigger Pattern**: Always required for DAML audits > **Inject Into**: Breadth agents, depth-edge-case > **Finding prefix**: `[DML-EI-N]` > **Rules referenced**: R10, R12, R14

A template's `ensure` clause is its creation precondition: a `create` whose `ensure` is `False` throws `PreconditionFailed` and the contract never exists. A missing or weak `ensure` lets an invalid contract enter the ACS (negative amount, empty party list, inconsistent fields), and every downstream choice then trusts the broken invariant. Separately, DAML `Int`/`Decimal` arithmetic THROWS on overflow rather than wrapping — so an arithmetic boundary is a **liveness/brick** bug (the choice aborts and becomes un-exercisable), not a silent-wrap value bug. The PoC for this class is a set of boundary-value `Script ()` functions (min / 1 / negative / max / empty-list), Aptos-style.

1. Ensure-Clause Inventory

For every template, record its `ensure` and the invariants it should enforce:

| Template | `ensure` Expr | Invariants It Should Enforce | Gap? | |----------|---------------|------------------------------|------| | `{T}` | `amount > 0.0 && obs /= []` / NONE | amount positive, parties non-empty, fields consistent | `[DML-EI-N]` if invariant unguarded |

**Critical patterns to flag**:

• No `ensure` at all on a template carrying an amount/balance/cap → a negative or zero amount contract is creatable (`[ELEVATE:ENSURE_GAP]`).
• An `ensure` that guards some fields but not the security-critical one (e.g., checks `amount > 0` but not `amount <= cap`, or not `maintainer non-empty`).
• An invariant assumed by a choice (`this.amount > 0`) that the `ensure` does not actually establish.

**DAML note**: `ensure` runs on `create` only. A choice that recreates a successor re-runs the successor's `ensure`; if the successor template has a weaker `ensure`, the invariant degrades across the lifecycle.

2. Boundary Substitution

For each ensure-guarded and arithmetic-bearing field, substitute boundary values and trace the outcome:

| Template/Choice | Field/Expr | Value Substituted | Outcome | Finding? | |-----------------|-----------|-------------------|---------|----------| | `{T / T.C}` | `amount` / `a + b` | 0 / 1 / -1 / maxInt / [] | created-invalid / abort / wrong-branch | `[DML-EI-N]` if invalid creatable or reachable abort |

**Substitute and trace**:

• `amount = 0` and `amount = -1`: does the contract create? Does a split produce zero-value children?
• `a + b` where both near `maxInt`/Decimal max: does the choice ABORT (`ArithmeticError`)? A reachable abort on a user path is a liveness brick (`[ELEVATE:ENSURE_GAP]` / boundary).
• empty list (`[]`) where a non-empty list is assumed (signatories, observers, maintainers): does `ensure`/the choice handle it, or does a later `head`/index abort?

3. Cross-Create Consistency

When several choices create instances of the same template, verify they all establish the same invariant.

| Template | Created By (choices) | All Paths Satisfy Same Invariant? | Weakest Path | Finding? | |----------|----------------------|-----------------------------------|--------------|----------| | `{T}` | `{choice list}` | YES/NO | `{choice}` | `[DML-EI-N]` if one path creates weaker state |

**Check for**:

• One creation path that bypasses a check another path enforces (asymmetric creation).
• An accumulator/cap that one creating choice updates but another does not, so the cap is enforced inconsistently (R14).

4. Deadline / Temporal-Gate Enforcement

A deadline is only enforced if a choice actually compares it against `getTime`.

| Template.Choice | Deadline Field | Compared Against `getTime`? | Comparison Relation | Enforced? | |-----------------|----------------|------------------------------|---------------------|-----------| | `{T.C}` | `{deadline}` | YES/NO | `< / <= / >` | `[DML-EI-N]` if deadline never enforced |

**Check for** (`[ELEVATE:DEADLINE_UNENFORCED]`):

• A `deadline`/`maturity`/`expiry` field stored but never read in any choice's guard → the time gate is decorative.
• A comparison against a caller-supplied time argument instead of `getTime` (ledger time) — the caller chooses "now".
• Off-by-one relation (`>=` vs `>`) letting an action happen exactly at/after expiry when it should not.

Finding Template

**ID**: [DML-EI-N]
**Severity**: [High if invalid state corrupts value/cap, Medium if liveness brick or unenforced deadline; Int/Decimal overflow is a LIVENESS finding, NOT auto-downgraded as silent-wrap]
**Step Execution**: ✓1,2,3,4 | ✗(reasons) | ?(uncertain)
**Rules Applied**: [R10:✓/✗, R12:✓/✗, R14:✓/✗]
**Location**: {Module}.daml:LineN (template X)
**Title**: Missing/weak ensure / unenforced deadline on {Template} allows {invalid contract / reachable abort}
**Description**: [The missing precondition or unenforced gate, the boundary value that breaks it, and the downstream choice that trusts the broken invariant]
**Impact**: [Invalid contract enters ACS / arithmetic abort bricks a user path / deadline bypass / cap unenforced]
**PoC steer**: boundary-value Scripts — `boundaryMin/boundaryNeg/boundaryMax : Script ()` calling a shared helper; assert create-invalid SUCCEEDS (ensure gap) or the choice aborts (ArithmeticError, liveness) or the past-deadline action SUCCEEDS (unenforced).

---

Step Execution Checklist (MANDATORY)

| Section | Required | Completed? | Notes | |---------|----------|------------|-------| | 1. Ensure-Clause Inventory | YES | ✓/✗/? | Every template's ensure vs its invariants | | 2. Boundary Substitution | YES | ✓/✗/? | 0 / 1 / -1 / max / empty-list per field | | 3. Cross-Create Consistency | IF template created by 2+ choices | ✓/✗(N/A)/? | All creation paths same invariant | | 4. Deadline / Temporal-Gate Enforcement | IF deadline/expiry field present |