Reference. Deterministic replay [ftip-00IY]

✍️sourceAGENTDRAFTED

Under the replay contract of Definition [ftip-00HF], equal execution inputs produce the same finite trace when the execution map is deterministic; see Theorem [ftip-00HG].