Consistency and freshness

• Every consumed record and note opens under a note-tree root from the pool's window R_NOTE.
• Every nullifier must be absent from the pool's nullifier set and distinct within the transaction. J checks intra-transaction distinctness; the pool checks the set.
• Historical membership proves existence, not liveness. A method that needs the current value of mutable private state consumes and recreates the record with a fresh rho and salt. The framework compiles a non_consuming choice to exactly that, so the surface stays Daml-like while the ledger stays UTXO. The cost is that two concurrent uses of one record conflict, which they would not in Canton.
• v2: an indexed Merkle tree over nullifiers, updated by a batch proof, gives non-membership proofs and therefore a true fetch under a recent root. Not required for any v1 workflow.

Time

time_bucket as in weld.md, accepted at current or previous bucket. Deadlines are record fields compared against it. No other clock.