Add missing proofs of properties of communication primitives

[javierdiaz72]

This will ultimately resolve #3.

[jeltsch]

This review is about repeated_receive_split only.

There is a small issue described in a separate comment below, which I’d like you to address.

Beyond that, there is some general issue, which, I think, mandates some more thorough changes of the code. I’d be happy if you could change the code accordingly, after which I’d continue with my reviewing.

The general issue I mean is that, in my opinion, terms like post_receive n X (λx. ∏B ← [A, A]. B ◃ □ x ∥ ¤⇧+ A) are hard to comprehend. This is because they use post_receive and ∏ in very concrete ways, so that their use doesn’t make things clearer but rather obscures them. In the case of post_receive, the received value is always used with □; in the case of ∏, the list is always of a fixed size. Some unfolding and streamlining leads to terms like (A « suffix n ◃ X ∥ A « suffix n ◃ X ∥ 𝟬) ∥ ¤⇧+ (A « suffix n) (my translation of the above term), which are much easier to understand, in my opinion.

I suggest to introduce analogs of transition_from_repeated_receive for distributor and its specializations (like duplication). These lemmas should use easy-to-read terms like the one above. With these lemmas in place, you can then make the proof of repeated_receive_split more readable.

[javierdiaz72]

The general issue mentioned in this comment is fixed in f23b794, please verify.

[javierdiaz72]

When continuing with the reviewing of repeated_receive_split please take into account b791356 as well. Thanks.

[jeltsch]

When crafting commit message titles, please try to avoid abbreviations of identifiers, which don’t really work, and put identifiers between backticks; so no “shortcut_redund. of ▹⇧∞”. I agree it’s sometimes hard to come up with commit message titles respecting our size limit (which I picked to avoid GitHub cutting them short in output). It sometimes helps to apply a little creativity to find a message that is perhaps not very precise or detailed, but captures the gist of the respective change.

[javierdiaz72]

When crafting commit message titles, please try to avoid abbreviations of identifiers, which don’t really work, and put identifiers between backticks; so no “shortcut_redund. of ▹⇧∞”. I agree it’s sometimes hard to come up with commit message titles respecting our size limit (which I picked to avoid GitHub cutting them short in output). It sometimes helps to apply a little creativity to find a message that is perhaps not very precise or detailed, but captures the gist of the respective change.

The character "_" is a typo, thanks for pointing it out. Nevertheless, I agree with your observation. For this GitHub issue in particular, it doesn't help too much that the issue refers to a bunch of lemmas, which forces me to try to include the respective lemma name in each commit message. I think this is an indicator that perhaps we should have split the issue into several related issues, one for each lemma.

[jeltsch]

I’ve been thinking for some time already that we should have made several issues instead of this one. It’s not just about commit message titles, but also about other things, for example reviewing (I’m always reviewing parts and have to keep track what I’ve already reviewed and what not). I think when I created this issue, there was partly some wishful thinking in my mind: I thought that it would be much less work to resolve this issue.

[jeltsch]

While thinking more about the transition_from_ lemmas, I figured that there is currently some inconsistency among them: the new ones have the adaptations « suffix n pushed inside, but transition_from_repeated_receive doesn’t.

Making transition_from_repeated_receive consistent with the other lemmas would result in the following variant of this lemma:

lemma transition_from_repeated_receive:
  assumes "A ▹⇧∞ x. 𝒫 x →⇩s⦇α⦈ Q"
  obtains n and X
  where "α = A ▹ ⋆⇗n⇖ X" and "Q = post_receive n X 𝒫 ∥ A « suffix n ▹⇧∞ x. 𝒫 x « suffix n"

Unfortunately, the term A « suffix n ▹⇧∞ x. 𝒫 x « suffix n is not so easy to comprehend and obfuscates the fact that the original process A ▹⇧∞ x. 𝒫 x is produced again, just with the adaptation « suffix n added. The latter also has the consequence that the proofs that use this lemma become more complicated, as the two occurrences of « suffix n, which are at the very inside, cannot be ignored via “up to mutation”.

I propose to go for a middle ground: split off the code for the current iteration from the code for the following iterations and possibly simplify the former, but keep « suffix n outside the latter. For transition_from_repeated_receive, this would result in the following variant of the lemma:

lemma transition_from_repeated_receive:
  assumes "A ▹⇧∞ x. 𝒫 x →⇩s⦇α⦈ Q"
  obtains n and X
  where "α = A ▹ ⋆⇗n⇖ X" and "Q = post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n"

I already have a patch that not only changes the lemma to this variant, but also accordingly adapts the proofs in thorn-calculus that use it.

If we go for this change, we should also modify the other transition_from_ lemmas to use the same scheme. For example, transition_from_duplication should become the following:

lemma transition_from_duplication:
    assumes "¤⇧+ A →⇩s⦇α⦈ Q"
    obtains n and X
    where "α = A ▹ ⋆⇗n⇖ X" and "Q = (A « suffix n ◃ X ∥ A « suffix n ◃ X ∥ 𝟬) ∥ ¤⇧+ A « suffix n"

What do you think about making these changes?

[jeltsch]

I think the solution I proposed above is particularly beautiful in the case of repeated_receive. Look at the shape that Q takes: post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n. This really expresses what’s going on: There are two processes running concurrently. The first one is the target process of a simple receive, the second one is essentially the original process, just with an additional adaptation, which captures the fact that we have repetition. This means that the components of repeated_receive, repetition and receiving, are clearly visible.

[javierdiaz72]

What do you think about making these changes?

Totally agreed. 😃

[jeltsch]

I started reviewing repeated_receive_split and have a first idea for improvement, which I’d like to discuss with you.

[jeltsch]

The statement you prove here is a bit more complex than needed and, most importantly, its proof is very long, which makes it a bit intimidating and not so easy to follow. I came up with an alternative solution, in particular a greatly simplified proof.

My simplification relies on a few general lemmas, which we might want to add to the Þ-calculus:

lemma no_mobility_communication:
  assumes "η ≠ μ" and "P →⇩s⦇IO η A 0 X⦈ P'" and "Q →⇩s⦇IO μ A 0 X⦈ Q'"
  shows "P ∥ Q →⇩s⦇τ⦈ P' ∥ Q'"
  using communication [where n = 0] and assms
  unfolding funpow_0 .

lemma no_mobility_parallel_left_io:
  assumes "P →⇩s⦇IO η A 0 X⦈ P'"
  shows "P ∥ Q →⇩s⦇IO η A 0 X⦈ P' ∥ Q"
  using parallel_left_io [where n = 0] and assms
  by transfer simp

lemma no_mobility_parallel_right_io:
  assumes "Q →⇩s⦇IO η A 0 X⦈ Q'"
  shows "P ∥ Q →⇩s⦇IO η A 0 X⦈ P ∥ Q'"
  using parallel_right_io [where n = 0] and assms
  by transfer simp

Furthermore, my simplification introduces the following lemma, which we probably should keep private:

lemma adapted_repeated_receive_no_mobility_transition:
  shows "
    (A ▹⇧∞ x. 𝒫 x) « suffix n
    →⇩s⦇A « suffix n ▹ ⋆⇗0⇖ X⦈
    post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n"
  unfolding adapted_after_repeated_receive
  using repeated_receive_transition [where 𝒫 = "λx. 𝒫 x « suffix n" and n = 0]
  unfolding post_receive_def
  by transfer force

With these preliminaries sorted out, the above code could be replaced by the following one:

    have "
      ¤⇧+ A ∥ A ▹⇧∞ x. 𝒫 x ∥ A ▹⇧∞ x. 𝒬 x
      ⇒⇩s⦇A ▹ ⋆⇗n⇖ X⦈
      ((𝟬 ∥ 𝟬 ∥ 𝟬) ∥ ¤⇧+ A « suffix n) ∥
      (post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n) ∥
      (post_receive n X 𝒬 ∥ (A ▹⇧∞ x. 𝒬 x) « suffix n)"
    proof -
      have "
        ¤⇧+ A ∥ A ▹⇧∞ x. 𝒫 x ∥ A ▹⇧∞ x. 𝒬 x
        →⇩s⦇A ▹ ⋆⇗n⇖ X⦈
        ((A « suffix n ◃ X ∥ A « suffix n ◃ X ∥ 𝟬) ∥ ¤⇧+ A « suffix n) ∥
        (A ▹⇧∞ x. 𝒫 x) « suffix n ∥ (A ▹⇧∞ x. 𝒬 x) « suffix n"
        unfolding adapted_after_parallel [symmetric]
        by (intro duplication_transition parallel_left_io) 
      moreover have "… →⇩s⦇τ⦈
        ((𝟬 ∥ A « suffix n ◃ X ∥ 𝟬) ∥ ¤⇧+ A « suffix n) ∥
        (post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n) ∥ (A ▹⇧∞ x. 𝒬 x) « suffix n"
        by
          (fast intro:
            no_mobility_communication
            no_mobility_parallel_left_io
            sending
            adapted_repeated_receive_no_mobility_transition
          )
      moreover have "… →⇩s⦇τ⦈
        ((𝟬 ∥ 𝟬 ∥ 𝟬) ∥ ¤⇧+ A « suffix n) ∥
        (post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n) ∥
        (post_receive n X 𝒬 ∥ (A ▹⇧∞ x. 𝒬 x) « suffix n)"
        by
          (fast intro:
            no_mobility_communication
            no_mobility_parallel_left_io
            no_mobility_parallel_right_io
            sending
            adapted_repeated_receive_no_mobility_transition
          )
      ultimately show ?thesis
        by force
    qed

What do you think?

[jeltsch]

Well, by employing is, the code can still be shrunk a bit: 😁

    have "
      ¤⇧+ A ∥ A ▹⇧∞ x. 𝒫 x ∥ A ▹⇧∞ x. 𝒬 x
      ⇒⇩s⦇A ▹ ⋆⇗n⇖ X⦈
      ((𝟬 ∥ 𝟬 ∥ 𝟬) ∥ ¤⇧+ A « suffix n) ∥
      (post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n) ∥
      (post_receive n X 𝒬 ∥ (A ▹⇧∞ x. 𝒬 x) « suffix n)"
      (is "?T ⇒⇩s⦇_⦈ ?U")
    proof -
      have "?T →⇩s⦇A ▹ ⋆⇗n⇖ X⦈
        ((A « suffix n ◃ X ∥ A « suffix n ◃ X ∥ 𝟬) ∥ ¤⇧+ A « suffix n) ∥
        (A ▹⇧∞ x. 𝒫 x) « suffix n ∥ (A ▹⇧∞ x. 𝒬 x) « suffix n"
        unfolding adapted_after_parallel [symmetric]
        by (intro duplication_transition parallel_left_io) 
      moreover have "… →⇩s⦇τ⦈
        ((𝟬 ∥ A « suffix n ◃ X ∥ 𝟬) ∥ ¤⇧+ A « suffix n) ∥
        (post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n) ∥ (A ▹⇧∞ x. 𝒬 x) « suffix n"
        by
          (fast intro:
            no_mobility_communication
            no_mobility_parallel_left_io
            sending
            adapted_repeated_receive_no_mobility_transition
          )
      moreover have "… →⇩s⦇τ⦈ ?U"
        by
          (fast intro:
            no_mobility_communication
            no_mobility_parallel_left_io
            no_mobility_parallel_right_io
            sending
            adapted_repeated_receive_no_mobility_transition
          )
      ultimately show ?thesis
        by force
    qed

[jeltsch]

I think, in other bisimilarity proofs, we were rather explicit when it came to constructing transitions. Your current proof above could be seen as following that style. However, I think what worked with very simple constructions does not work well with this more complex construction: while the reader is taken by the hand and led step by step through the construction, he might lose track, because it’s difficult to get a good overview of the construction due to its complexity. I think it’s better to have a concise proof that makes it easy to see how the construction works on the whole and still doesn’t make it too complicated to figure out how the individual steps can be justified.

[javierdiaz72]

I think we should implement this simplification.

[javierdiaz72]

However, although much shorter, I'm not yet so convinced that bundling the application of three transition rules such as sending, parallel_left_io and communication plus a pseudo-transition rule such as adapted_repeated_receive_no_mobility_transition into a single proof step actually improves readability. 🤔.

[jeltsch]

At least, we say in the proof method expression that we use adapted_repeated_receive_no_mobility_transition, as well as sending and communication. As a result, the reader can at least figure out with reasonable effort what’s going on. I’d say making a sending and a receiving transition on arbitrarily deep subprocesses and combining them with communication is a quite natural thing for someone used to process calculi. Therefore, the only real issue I see is the use of the non-standard adapted_receive_no_mobility_transition, but at least this would have been introduced immediately before repeated_receive_split.

I think there are two competing effects at play here:

• More detailed proofs make the entire construction explicit and this way aid understanding.
• More concise proofs make the overall structure of the construction clearer and this way aid understanding.

I think the importance of the second point varies greatly with the complexity of the construction: while for simple constructions, like combining receive with parallel_left_io, it is of virtually no relevance, it is of considerable importance for constructions like the one we’re talking about here. Therefore, I’d say for simple constructions it is not so clear whether being concise is better or not, but it is rather clear that it is better for complex constructions.

Let’s go for this concise version.

[jeltsch]

The no-mobility versions of transition system rules that the concise version uses have been introduced by input-output-hk/thorn-calculus#71 now.

[javierdiaz72]

Please note that the PR mentioned above has already been accepted.

[jeltsch]

Could you please make all _transition lemmas in this theory (like loss_transition) public, move them between the corresponding adapted_after_ and transition_from_ lemmas, give them consistent naming, and add any missing such lemmas? The result of that would be the next thing I’d like to review. 🙂

[javierdiaz72]

Could you please make all _transition lemmas in this theory (like loss_transition) public, move them between the corresponding adapted_after_ and transition_from_ lemmas, give them consistent naming, and add any missing such lemmas? The result of that would be the next thing I’d like to review. slightly_smiling_face

Done in e085e35, please review.

[jeltsch]

Could you please make all _transition lemmas in this theory (like loss_transition) public, move them between the corresponding adapted_after_ and transition_from_ lemmas, give them consistent naming, and add any missing such lemmas? The result of that would be the next thing I’d like to review. slightly_smiling_face

Done in e085e35, please review.

Two initial requests:

• Could you please move these lemmas before the corresponding transition_from_ lemmas (but after the corresponding adapted_after_ lemmas), as asked for above? This way, the order corresponds to what we have for repeated_receive.
• Could you please change the names of the duploss-related lemmas to duploss_losing_transition and duploss_duplicating_transition? These names correspond to what we have for bidirectional_bridge: they have the same structure and also incorporate the case names from the corresponding transition_from_ lemma.

[javierdiaz72]

* Could you please move these lemmas _before_ the corresponding `transition_from_` lemmas (but after the corresponding `adapted_after_` lemmas), as asked for above? This way, the order corresponds to what we have for `repeated_receive`.

If I do that then the current proof of distributor_transition will not be able to make use of transition_from_distributor. Of course, I can come up with a proof that does not make such use at the expense of some repetition. What's your opinion?

[javierdiaz72]

* Could you please change the names of the `duploss`-related lemmas to `duploss_losing_transition` and `duploss_duplicating_transition`? These names correspond to what we have for `bidirectional_bridge`: they have the same structure and also incorporate the case names from the corresponding `transition_from_` lemma.

Fixed in e45125d, please verify.

[javierdiaz72]

* Could you please move these lemmas _before_ the corresponding `transition_from_` lemmas (but after the corresponding `adapted_after_` lemmas), as asked for above? This way, the order corresponds to what we have for `repeated_receive`.

If I do that then the current proof of distributor_transition will not be able to make use of transition_from_distributor. Of course, I can come up with a proof that does not make such use at the expense of some repetition. What's your opinion?

After some thinking, I realized that, for the sake of consistency with respect to the other _transition lemmas, the proof of distributor_transition should actually rely on repeated_receive_transition. I'm currently working on such a proof.

[javierdiaz72]

Now, the new proof of distributor_transition is in 0509829 and the relocation of the _transition lemmas is in f40d7ab, please verify.

[jeltsch]

If I do that then the current proof of distributor_transition will not be able to make use of transition_from_distributor. Of course, I can come up with a proof that does not make such use at the expense of some repetition. What's your opinion?

After some thinking, I realized that, for the sake of consistency with respect to the other _transition lemmas, the proof of distributor_transition should actually rely on repeated_receive_transition. I'm currently working on such a proof.

The proof of distributor_transition should indeed not rely on transition_from_distributor. I must say at the moment I can’t even imagine how you would use transition_from_distributor to prove distributor_transition, as it is kind of the opposite lemma.

[jeltsch]

The proof of distributor_transition should indeed not rely on transition_from_distributor. I must say at the moment I can’t even imagine how you would use transition_from_distributor to prove distributor_transition, as it is kind of the opposite lemma.

I just looked at the old code, which is as follows:

lemma distributor_transition:
  shows "A ⇒ Bs →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ ∏B ← Bs. B « suffix n ◃ X ∥ (A ⇒ Bs) « suffix n"
proof -
  have "A ⇒ Bs →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ post_receive n X (λx. ∏B ← Bs. B ◃ □ x ∥ A ⇒ Bs)"
    unfolding distributor_def
    using receiving
    by (subst repeated_receive_proper_def)
  then show ?thesis
    by (elim transition_from_distributor, auto simp only:)
qed

I understand now how you use transition_from_distributor to prove distributor_transition. You first construct a prototype transition by going down to the transition system rules, avoiding repeated_receive_transition. You definitely have to construct a transition first, because transition_from_distributor doesn’t construct one (this is what made me wonder why you would use transition_from_distributor). Afterwards, you use transition_from_distributor to learn what the transition you have constructed actually is, so to say. Yes, this approach works, but I’d say it’s unnecessarily complicated; so it’s good to have the proof modified now.

[javierdiaz72]

Now, the new proof of distributor_transition is in 0509829 and the relocation of the _transition lemmas is in f40d7ab, please verify.

If I do that then the current proof of distributor_transition will not be able to make use of transition_from_distributor. Of course, I can come up with a proof that does not make such use at the expense of some repetition. What's your opinion?

After some thinking, I realized that, for the sake of consistency with respect to the other _transition lemmas, the proof of distributor_transition should actually rely on repeated_receive_transition. I'm currently working on such a proof.

The proof of distributor_transition should indeed not rely on transition_from_distributor. I must say at the moment I can’t even imagine how you would use transition_from_distributor to prove distributor_transition, as it is kind of the opposite lemma.

You can construct an initial transition using receiving and then use this transition with transition_from_distributor to simplify the target process:

lemma distributor_transition:
  shows "A ⇒ Bs →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ ∏B ← Bs. B « suffix n ◃ X ∥ (A ⇒ Bs) « suffix n"
proof -
  have "A ⇒ Bs →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ post_receive n X (λx. ∏B ← Bs. B ◃ □ x ∥ A ⇒ Bs)"
    unfolding distributor_def
    using receiving
    by (subst repeated_receive_proper_def)
  then show ?thesis
    by (elim transition_from_distributor, auto simp only:)
qed

[jeltsch]

I have reviewed the _transition lemmas and have some requests for changes.

[jeltsch]

The statement of this lemma should be ¤⇧* A →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ 𝟬 ∥ ¤⇧* A « suffix n, for the following reasons:

• All our previous _transition and transition_from_ lemmas use transitions of the form P →⦇α⦈ T ∥ P.
• All our previous _transition lemmas use the target process families that are used by their corresponding transition_from_ lemmas.

[javierdiaz72]

The problem I see is that the process families (𝟬 ∥ ¤⇧? A « suffix n) ∥ ¤⇧+ A « suffix n and 𝟬 ∥ ¤⇧* A « suffix n are not equal but bisimilar (since an application of parallel_associativity would be needed). Therefore, I think that, in line with what we did for transition_from_duploss, the statement of this lemma should be as follows:

lemma duploss_losing_transition:
  obtains Q where "¤⇧* A →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ Q" and "Q ∼⇩s 𝟬 ∥ ¤⇧* A « suffix n"

What do you think?

[jeltsch]

Yes, this would be the obvious choice. The question is whether this would make the proofs that use these lemmas more complicated. Are we using these lemmas somewhere at the moment, and, if yes, do we rely on them stating just a plain transition?

[jeltsch]

I found two uses of these lemmas: in line 1254 and in line 1575. For the former, things might get more complex in a sense, because we would have to perform a simulation step to show that the follow-up transition we construct has a counterpart that starts at Q. The same applies in principle also to the latter, but there we have currently quite some follow-up reasoning with that complex term ?T, which might get considerably simplified if we turned to the new versions of those lemmas.

What do you think? Should we make the change you proposed and see where it leads us? If in some particular situation we find that this makes matters more complicated, we could still unfold duploss or bidirectional_bridge on the spot and reason with the _transition lemmas for the underlying constructs.

[javierdiaz72]

I think that makes much sense and we should go for it.

[jeltsch]

Great! Please make the necessary changes then. I’d like to encourage you to use the reworked lemmas wherever somehow feasible instead of going for the unfolding solution. It’s more high-level and thus should make the proofs cleaner and more understandable in general.

[javierdiaz72]

Done in 44280bc and afbd55c, please verify.

[jeltsch]

lemma duploss_losing_transition:
  obtains Q where "¤⇧* A →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ Q" and "Q ∼⇩s 𝟬 ∥ ¤⇧* A « suffix n"

Actually, I think the two statements after where should be swapped, because, as far as I remember, we typically first say what the obtained variables are about.

[jeltsch]

Hmm, on the other hand, as it is now, the statement reads more naturally. Also, in contrast to, say, the transition_from_ lemmas, this lemma doesn’t tell us anything about variables used in some assumption. Maybe we should leave the statement as written above.

[jeltsch]

The statement of this lemma should be ¤⇧* A →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ (A « suffix n ◃ X ∥ A « suffix n ◃ X ∥ 𝟬) ∥ ¤⇧* A « suffix n, for the reasons stated above.

[jeltsch]

The statement of this lemma should be A ↔ B →⇩s⦇A ▹ ⋆⇗n⇖ X⦈ (B « suffix n ◃ X ∥ 𝟬) ∥ (A ↔ B) « suffix n, for the reasons stated above.

[jeltsch]

The statement of this lemma should be A ↔ B →⇩s⦇B ▹ ⋆⇗n⇖ X⦈ (A « suffix n ◃ X ∥ 𝟬) ∥ (A ↔ B) « suffix n, for the reasons stated above.

[javierdiaz72]

Unfortunately, I made a mistake when describing the first step of my approach to proving repeated_receive_channel_switch:

Instead of performing a case distinction on the transition A ↔ B ∥ A ▹⇧∞ x. 𝒫 x →⇩s⦇α⦈ S, we translate this transition into A ↔ B ∥ B ▹⇧∞ x. 𝒫 x →⇩s⦇α⦈ S, using receive_channel_switch, exploiting the fact that bisimilarity is a simulation relation.

The mistake I made is that I pretended the application of receive_channel_switch would change the channel for receiving for each iteration, when in fact it does so only for the first. Incidentally, if this version of the first step would work, the second step wouldn’t, as we need to get into process families related by the bisimulation relation up to context etc., which means the channels for receiving have to be different for the follow-up iterations.

So what does the correct version of the first step look like?

* We start with the transition `A ↔ B ∥ A ▹⇧∞ x. 𝒫 x →⇩s⦇α⦈ S` and observe that `A ↔ B ∥ A ▹⇧∞ x. 𝒫 x` is equal to `A ↔ B ∥ A ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x)`, which in turn is bisimilar to `A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x)` because of `receive_channel_switch`. We derive the transition `A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) →⇩s⦇α⦈ S` from the original transition by means of simulation.

* After having derived this transition, we perform case distinction on it. Handling the different cases should be simple, since the simulating transitions have to originate from `A ↔ B ∥ B ▹⇧∞ x. 𝒫 x`, which is equal to `A ↔ B ∥ B ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x)`, which differs from `A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x)` only in the channel used for `repeated_receive`. This difference is what we actually need for having target process families being in the bisimulation relation up to context etc.

By the way, I assumed above that the simulating side uses the same bridge as the original side. However, we should probably use the same trick for exploiting quasi-symmetry as for receive_channel_switch, which would mean that the bridge on the simulating side would be B ↔ A instead of A ↔ B.

I was implementing this and came across the following issue: Since receive_channel_switch involves ≈⇩s (and not ∼⇩s), then by means of simulation I was only able to derive the weak transition A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) ⇒⇩s⦇α⦈ S' for some S' ≈⇩s S instead of the strong transition A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) →⇩s⦇α⦈ S that you mentioned in the first step above. Do you have any other idea to work around this issue and still be able to use receive_channel_switch or should just we go ahead and prove the lemma applying the usual approach?

[jeltsch]

Hi, @javierdiaz72! What is 98edc9b about? Did you accidentally delete receive_channel_switch at some point?

[jeltsch]

I was implementing this and came across the following issue: Since receive_channel_switch involves ≈⇩s (and not ∼⇩s), then by means of simulation I was only able to derive the weak transition A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) ⇒⇩s⦇α⦈ S' for some S' ≈⇩s S instead of the strong transition A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) →⇩s⦇α⦈ S that you mentioned in the first step above. Do you have any other idea to work around this issue and still be able to use receive_channel_switch or should just we go ahead and prove the lemma applying the usual approach?

You’re absolutely right: we get a weak transition; so the only way to kind of save my approach would be to analyze this weak transition, which would be too involved. However, I just thought a bit about an alternative and came up with the following solution:

1. We show the auxiliary lemma A ↔ B ∥ A ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) ≈⇩s A ↔ B ∥ A ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x) on the transition system level. For handling transitions that originate from the second argument of ∥, we proceed as follows:
   1. We observe that the only possible kind of transition is that of a receiving transition ending in a process family A ↔ B ∥ post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n, which we simulate by the analogous transition from the right-hand side.
   2. We observe that the target process families are equal to post_receive n X 𝒫 ∥ A ↔ B ∥ (A ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x)) « suffix n and post_receive n X 𝒫 ∥ A ↔ B ∥ (B ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x)) « suffix n.
   3. We observe that the latter of the above process families is weakly bisimilar to post_receive n X 𝒫 ∥ A ↔ B ∥ (A ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x)) « suffix n because of receive_channel_switch.
   4. We use this fact to show that we get indeed a simulation via “up to bisimilarity” and “up to context”.
2. We derive from the auxiliary lemma the fact A ↔ B ∥ A ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) ≈⇩s A ↔ B ∥ B ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x) by using receive_channel_switch again.
3. We observe that this is equivalent to the statement we want to prove, given the definition of repeated_receive.

What do you think about this approach? Do you think it would be at least a bit simpler that proving repeated_receive_channel_switch from scratch and thus repeating things from the proof of receive_channel_switch?

[javierdiaz72]

Hi, @javierdiaz72! What is 98edc9b about? Did you accidentally delete receive_channel_switch at some point?

I'm not sure what happened, it seems to me that I accidentally left out receive_channel_switch altogether upon my first commit, so I had to put back the lemma and include its proof in this new commit.

[javierdiaz72]

3. receive_channel_switch

I was implementing this and came across the following issue: Since receive_channel_switch involves ≈⇩s (and not ∼⇩s), then by means of simulation I was only able to derive the weak transition A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) ⇒⇩s⦇α⦈ S' for some S' ≈⇩s S instead of the strong transition A ↔ B ∥ B ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) →⇩s⦇α⦈ S that you mentioned in the first step above. Do you have any other idea to work around this issue and still be able to use receive_channel_switch or should just we go ahead and prove the lemma applying the usual approach?

You’re absolutely right: we get a weak transition; so the only way to kind of save my approach would be to analyze this weak transition, which would be too involved. However, I just thought a bit about an alternative and came up with the following solution:

1. We show the auxiliary lemma `A ↔ B ∥ A ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) ≈⇩s A ↔ B ∥ A ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x)` on the transition system level. For handling transitions that originate from the second argument of `∥`, we proceed as follows:
   
   1. We observe that the only possible kind of transition is that of a receiving transition ending in a process family `A ↔ B ∥ post_receive n X 𝒫 ∥ (A ▹⇧∞ x. 𝒫 x) « suffix n`, which we simulate by the analogous transition from the right-hand side.
   2. We observe that the target process families are equal to `post_receive n X 𝒫 ∥ A ↔ B ∥ (A ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x)) « suffix n` and `post_receive n X 𝒫 ∥ A ↔ B ∥ (B ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x)) « suffix n`.
   3. We observe that the latter of the above process families is weakly bisimilar to `post_receive n X 𝒫 ∥ A ↔ B ∥ (A ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x)) « suffix n` because of `receive_channel_switch`.
   4. We use this fact to show that we get indeed a simulation via “up to bisimilarity” and “up to context”.

2. We derive from the auxiliary lemma the fact `A ↔ B ∥ A ▹ x. (𝒫 x ∥ A ▹⇧∞ x. 𝒫 x) ≈⇩s A ↔ B ∥ B ▹ x. (𝒫 x ∥ B ▹⇧∞ x. 𝒫 x)` by using `receive_channel_switch` again.

3. We observe that this is equivalent to the statement we want to prove, given the definition of `repeated_receive`.

What do you think about this approach? Do you think it would be at least a bit simpler that proving repeated_receive_channel_switch from scratch and thus repeating things from the proof of receive_channel_switch?

The problem I see with this approach is that in step (iv) we should use the function [∼⇩s] ⌢ ℳ ⌢ [≈⇩s], however ℳ ⌢ [≈⇩s] is not respectful. Please correct me if I'm wrong.

[jeltsch]

The problem I see with this approach is that in step (iv) we should use the function [∼⇩s] ⌢ ℳ ⌢ [≈⇩s], however ℳ ⌢ [≈⇩s] is not respectful. Please correct me if I’m wrong.

Oh, no: yet another of these easy-to-overlook issues that make the whole approach fail. 😓 Did you spot this issue while trying to write the proof in Isabelle, or did you spot it beforehand?

What do you think: should we just go for a traditional transition level proof, without any reuse of receive_channel_split?

[javierdiaz72]

Oh, no: yet another of these easy-to-overlook issues that make the whole approach fail. sweat Did you spot this issue while trying to write the proof in Isabelle, or did you spot it beforehand?

I spot it when writing down a "proof sketch" using some Isabelle syntax and then checked it directly in Isabelle. 😁

What do you think: should we just go for a traditional transition level proof, without any reuse of receive_channel_split?

Honestly, I don't have any idea how to reuse receive_channel_split. Perhaps it's best to go for a traditional transition level proof and later, if we come up with a better solution, implement it.

[jeltsch]

Honestly, I don't have any idea how to reuse receive_channel_split. Perhaps it's best to go for a traditional transition level proof and later, if we come up with a better solution, implement it.

The only potentially better approach I can come up with at the moment is to prove a lemma that is generic in the “up to” method and then derive from it both receive_channel_switch and repeated_receive_channel_switch. However, I suggest that we just prove repeated_receive_channel_switch from scratch for now. If we want, we can use the approach with the generic lemma later, but I think we should rather stay with the direct proofs of the lemmas.