Really excited to see this paper released! 
Quick question on counterfactual terminology: when you say “X could happen on-chain, but doesn’t” should that be interpreted as “X could happen on-chain, but hasn’t yet”? Related to this: if the operation X does happen to be later enforced on-chain, does it transition from “counterfactual X” to “actual/factual(?!) X”?