diff options
Diffstat (limited to 'content/zettel/3a5c1a.md')
| -rw-r--r-- | content/zettel/3a5c1a.md | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/3a5c1a.md b/content/zettel/3a5c1a.md new file mode 100644 index 0000000..a986dab --- /dev/null +++ b/content/zettel/3a5c1a.md @@ -0,0 +1,24 @@ ++++ +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. |