+++
title = "Continuously matching states without stepping"
date = "2022-04-24"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a5c1"]
forwardlinks = []
zettelid = "3a5c1a"
+++

The `match_states` predicate is supposed to represent a similarity of a
state in the source language and a state in the target language. It
requires a bit of a different view point to be able to implement the
star simulation proof that was described earlier. In essence, one is
still comparing similarities between the two different states, however,
one is mostly using that comparison to also carry proofs about the
previous executions one has performed. In addition to that, the matching
predicate will always match the currently executing instruction, to the
state at the start of the output transition. This requires that one is
able to find the state of the output transition, which in the case of
basic blocks is not that hard as it can actually be reliably computed,
but in cases where it's more difficult, one could use some additional
information that is returned by the generation of the output program.