Relating interaction tree and small-step semantics

[alxest]

I am trying to prove refinement between two different interpretations of the same program -- one in interaction tree and the other in small-step semantics (in fact, CompCert Clight). Specifically, I give small-step semantics to an interaction tree (a state consists of interaction tree) and then use traditional simulation techniques between the two small-step semantics. However, I cannot see a simple simulation relation because the two take quite different approaches to modeling loop/recursion (and its continuation). I have some rough ideas on doing this, but I guess there is some related work and I am reinventing the wheel in an ugly way...

Any advice is appreciated. Thank you!

[alxest]

FYI: My rough idea is to define two marker events to mark the beginning (event <) and the end (event >) of a function, merely to give simulation relation. (these events are ignored in top-level) That way, I can regain stack-like structure from an interaction tree and can give a simulation relation between source/target stacks.

[Lysxia]

I'm afraid I don't have any references to point to. Maybe one of my coauthor does?

How are function calls represented, in both the itree and the original small-step semantics? In particular I'm curious about the details of how you handle recursion in itree.

[alxest]

@Lysxia (I guess I have found a solution, but I will write these as a reference.)

Problem

In itree, I defined recursion using mrec combinator. Specifically, each function has type list val -> itree (MyCallE +' E) val and I use mrec to make it list val -> itree E val. (MyCallE consists of list val) The problem here is that, the resulting itree has unfolded (or, flattened?) all the recursive function calls, while in small-step semantics we do not. As an example, consider this simple program.

f(n) = if(n>0) {
L0:      print "A" ;
L1:      f(n-1) ;
L2:      print "A" 
       }

Let's say that I want to show f(5) has the same behavior in these two semantics. At the beginning of f(3),

• itree state will be like following: print A ; print A; ... print A where print "A" appears 8 times in total.
• The small-step state will be like following: State (n ~> 3) L0, Stack [(n ~> 4), L2] ++ [(n ~> 5), L2] where the first argument of State is local environment (mapping var to value) and the second argument is the program counter.

Here, I need to give a simulation relation that relates State (n ~> 3) L0 with the first 6 occurrences of print "A", and relates Stack ... with the last 2 occurrences of print "A". However, doing this requires in-depth understanding of f, where the proof technique that I want should be general and not specialized to a specific program.

Solution

I give an intermediate semantics as a bridge between the two. The idea is to give a stack-like structure to itree, which is useful for better simulation relation. Specifically, its state is (itree (MyCallE +' E) val), List (ktree (MyCallE +' E) val val). (Note that we do have MyCallE event here, because we don't use mrec to handle them; we handle them in step relation.) Its step relation is like the original one, but it handles MyCallE by pushing a new itree into the stack. (and handles Ret correspondingly)

Now we can prove itree-semantics f(4) ~= Clight-semantics f(4) with transitivity.

• itree ~= itree-stack I expect that I can prove this for an arbitrary itree so that user can use it as a meta-theory.
• itree-stack ~= Clight In the example above (beginning of f(3)), this itree-stack semantics has the following state: (call f ;; print "A" ;; Ret _), [fun _ => print "A" ;; Ret _] ++ [fun _ => print "A" ;; Ret _] . Now, we can directly relate this with Clight state -- its structure is the same.

[Lysxia]

Thanks, this is quite instructive!

One detail that's itching me is that the state of the intermediate semantics, a pair (t, [k1; ...; kn]) : (itree (MyCallE +' E) val) * List (ktree (MyCallE +' E) val val), is eventually intended to represent a single itree interp something (t >>= k1 >>= ... >>= kn). Thus it seems possible to make the intermediate semantics directly an itree, as a denotational semantics of the original Clight state. The benefits of this slight reformulation is that it allows the intermediate semantics to (re)use a generic step relation on itrees (whereas there currently seems to be an ad-hoc step relation), and the relation itree ~= itree-stack can simply be eutt.

[alxest]

@Lysxia Thanks for your reply. It seems I didn't make the point clear. Let me try to clarify my viewpoint again.

My verification strategy is as follows: spec (itree) >= ... >= impl (itree) >= impl (Clight).

• In this scenario, I don't want to do mathematical reasoning at all while proving impl (itree) >= impl (Clight). All the mathematical reasoning (e.g., induction) should be done in the high-level refinement (left ones). itree has very nice recursion theory, so I can happily prove this high-level refinement.

• However, the problem is in impl (itree) >= impl (Clight). itree has already abstracted away too much information so that it is hard to directly prove this low-level refinement.

  Simply, think of a fibonacci function. impl (itree) is already a spec (directly returning the desired result), and proving impl (itree) >= impl (Clight) means that you are doing inductive reasoning in this level, and you can't get full benefit of itree's recursion theory here -- you have to write tedious details of inductive reasoning in simulation relation here.

  More generally, let's see the above example again. The itree state consists of flatten print "A" ** 8 (1) without stack-like structure, and (2) all the future computations already represented. However, this is not the case for the Clight. In order to relate itree/Clight state properly (e.g., I should not relate the example Clight state with print "A" ** 9 or print "A" ** 7; it has to be related only with print "A" ** 8), one has to calculate that State (n ~> 3) L0 will call print "A" 6 times in the future (and similarly for each stack frames), where this calculation involves mathematical reasoning that I would like to avoid in the low-level refinement.

---

To address this discrepancy, I put f_impl (itree-stack) between f_impl (itree) and f_impl (Clight). This f_impl (itree-stack) is close enough to both f_impl (itree) and f_impl (Clight), so proving these two separate conditions is much easier than directly proving f_impl (itree) >= f_impl (Clight).

• f (itree) >= f (itree-stack): interpreting && binding all the continuation stack (what you wrote as interp something t >>= k1 >>= ... >>= kn) will yield exactly the same single itree as in f (itree). Actually, I use this as the simulation relation, and all the proof is trivial.
• f (itree-stack) >= f (Clight): both has the stack-structure so it is much easier to give simulation relation than before. I don't have to calculate that State (n ~> 3) L0 will print 6 times (and similarly for each stack frames) anymore.