The ERC-8319 comment upthread cites two lemmas about reg_sm: confiscation is terminal, and confiscation is universally reachable from any non-terminal state. I want to push on what that second lemma means as a property of a standard rather than a proof, and propose that the interesting object is its inverse.
Universal reachability is proven over states, not over consent. As a recovery primitive that’s the guarantee you want (no laundering endpoint is safe). As a standards-track property it’s indistinguishable from a proven-unescapable seizure switch. The proof is neutral between victim-initiated recovery and jurisdiction-initiated confiscation, and nothing in the state machine distinguishes them. That neutrality is the objection the ERC will meet, and it can’t be patched at the policy layer because the lemma is about the transition function itself.
The inverse construction: make revocability a typed property of the asset, opted into at mint. A provisional asset carries an absolute finality_ts; before it, transfers are challengeable by bonded dispute; after it, the asset converts permissionlessly into its final form. The lemma you then prove is the mirror of yours: confiscation is unreachable from any final state, by construction. Reachability holds exactly on the set of states that consented to it, and nowhere else.
Composition is one rule: any output inherits max(finality_ts) of its inputs. Wrapping can’t stack windows and can’t reset them; the window burns down in wall-clock time regardless of topology. Pools don’t commingle types, so contagion is excluded by the type system rather than bounded by graph traversal. The boundary between challengeable and final is disjoint in time (challenge requires t < finality_ts, conversion requires t >= finality_ts), so no block exists where both are valid and there is no ordering race to adjudicate. What remains is censorship of challenges, which prices into the choice of T.
This is a direct answer attempt at Q3. You asked what structure the reduction relation among synchronization strengths should take on top of the §3 preservation map. Typed revocability suggests the strengths are types and the reduction relation is subtyping: provisional safely contains final, and max-composition is the join. An asset’s required strength is declared, not discovered. It also bears on Q5’s clock question: an absolute finality_ts means the asset carries its own clock, so the happened-before relation at the finality boundary is defined by the asset rather than by either domain’s time model.
The general claim: reachability lemmas about enforcement primitives should be proven over the consenting subset of states, not the state space. A standard that proves universal reachability has proven too much.