input-output-hk/high-assurance-legacy

Legacy code connected to the high-assurance implementation of the Ouroboros protocol family

Overview

This is the old repository of the project to develop implementations of blockchain consensus protocols from the Ouroboros family in a process calculus and verify that they have various key properties.

In this final, archived form, this repository contains only some old exploratory material as well as code we have chosen not to develop further, in most cases because it got superseded by superior components. We keep this repository around merely for people interested in the history of this project.

The actively developed code of this project can be found in the following GitHub repositories:

• equivalence-reasoner

• transition-systems

• thorn-calculus

• network-equivalences

• ouroboros-high-assurance

high-assurance-legacy's Issues

Formally prove the actual relaying–broadcasting equivalence theorem

Our goal is to formally prove that a diamond-shaped relaying network and a corresponding broadcasting network are bisimilar if their receive channels are lossy.

The comments on #15 provide more information about relaying–broadcasting equivalence, including an informal proof.

Add skeletons of `unidirectional_bridge` core lemmas

Our goal is to add skeletons of the following core lemmas about unidirectional_bridge:

shortcut_addition:
  a → b ∥ b → c ≈⇩♭ a → b ∥ b → c ∥ a → c
loop_redundancy_under_duploss:
  ¤⇧*a ∥ a → a ≈⇩♭ ¤⇧*a

Informally prove relaying–broadcasting equivalence

A relaying network is a network with unidirectional links that contains a route from each node to each node. A broadcasting network is a network where all nodes are connected by a single broadcasting medium.

Our goal is to prove that for each set of nodes every relaying network with these nodes and the single broadcasting network with these nodes behave equivalently in a meaningful sense.

• Develop a sensible representation of networks as processes
• Develop a meaningful notion of equivalence of network behavior based on bisimilarity
• Specify useful auxiliary facts
• Prove the auxiliary facts
• Prove the actual theorem

Formally prove `unidirectional_bridge` core lemmas

Our goal is to formally prove the unidirectional_bridge core lemmas described in #34.

Informal proofs of these lemmas are given in #15 (comment).

Generalize the `shortcut_addition` lemma

Currently the shortcut_addition lemma states a → b ∥ b → c ≈⇩♭ a → b ∥ b → c ∥ a → c. However, it is possible to replace the bridges that target c by multi_receive processes with bodies other than a single Send. Our goal is to generalize the lemma accordingly. No changes to the proof should be necessary.

Improve documentation of `in_bisimilarity_standard`

The documentation of in_bisimilarity_standard is currently not in the same format as the documentation of other proof methods. Our goal is to fix that.

Add skeletons of `duploss` core lemmas

Our goal is to add skeletons of the following core lemmas about duploss:

send_idempotency_under_duploss:
  ¤⇧*a ∥ a ◃ x ∥ a ◃ x ≈⇩♭ ¤⇧* a ∥ a ◃ x

Formally prove `multi_receive` core lemmas

Our goal is to formally prove the multi_receive core lemmas described in #32.

Informal proofs of these lemmas are given in #15 (comment).

Switch to simpler proof methods

A few lemmas in Basic_Transition_System are currently proved using unnecessarily complex proof methods. Our goal is to pick simpler proof methods for them.

Add skeletons of `bidirectional_bridge` core lemmas

Our goal is to add skeletons of the following core lemmas about bidirectional_bridge:

send_channel_switch:
  a ↔ b ∥ a ◃ x ≈⇩♭ a ↔ b ∥ b ◃ x
receive_channel_switch:
  a ↔ b ∥ a ▹ x. P x ≈⇩♭ a ↔ b ∥ b ▹ x. P x
multi_receive_channel_switch:
  a ↔ b ∥ a ▹⇧∞ x. P x ≈⇩♭ a ↔ b ∥ b ▹ x. P x
source_switch:
  a ↔ b ∥ a → c ≈⇩♭ a ↔ b ∥ b → c
target_switch:
  a ↔ b ∥ c → a ≈⇩♭ a ↔ b ∥ c → b
loss_switch:
  a ↔ b ∥ ¤⇧?a ≈⇩♭ a ↔ b ∥ ¤⇧?b
duplication_switch:
  a ↔ b ∥ ¤⇧+a ≈⇩♭ a ↔ b ∥ ¤⇧+b
duploss_switch:
  a ↔ b ∥ ¤⇧*a ≈⇩♭ a ↔ b ∥ ¤⇧*b
detour_squashing:
  ν b. (a ↔ b) ≈⇩♯ a → a
duploss_detour_collapse:
  ν b. (¤⇧*b ∥ a ↔ b) ≈⇩♯ ¤⇧*a

Make the Isabelle code work with Isabelle2019

Currently our Isabelle code is tested with Isabelle2018. However, Isabelle2019 was released in June 2019. Our goal is to make our code work with Isabelle2019.

Formally prove `bidirectional_bridge` core lemmas

Our goal is to formally prove the bidirectional_bridge core lemmas described in #35.

Informal proofs of these lemmas are given in #15 (comment).

Base the definitions of concrete strong bisimilarity relations on weak residual structures

Currently the strong bisimilarity relations of the basic and the proper transition system are defined in terms of relators that are auto-generated by Isabelle. However, the general proof that strong bisimilarity is contained in weak bisimilarity refers to strong bisimilarity relations that are defined in terms of corresponding weak residual structures. As a result, we cannot apply this general result to our concrete bisimilarity relations.

Our goal is to modify the definitions of the basic and the proper strong bisimilarity relation such that they are based on the corresponding weak residual structures.

• Base the definitions of concrete strong bisimilarity relations on weak residual structures
• Remove the lemma skeletons for concrete strong–weak bisimilarity containment

Reflect the renaming of our process calculus in the code base

We recently changed the name of our process calculus from “χ-calculus” to “♮-calculus”, because there is already another process calculus named “χ-calculus”. Our goal is to change the source code, file names, and documentation in both the Haskell and the Isabelle part of the code base to reflect this change.

Recover the more meaningful names for lift operators and associated rules

Commit b35f3f6 made the χ-calculus formalization use built-in relator support for lift operators. As a consequence, lift operators and their introduction and elimination rules now have to be referenced with more technical names like rel_basic_residual and basic_residual.rel_intros(1) instead of the former, more meaningful names like basic_lift and acting_lift.

Our goal is to reintroduce the more meaningful names by defining them as aliases of the more technical ones and to use them throughout the code.

• Introduce the more meaningful names as aliases
• Switch the complete Isabelle code to using the more meaningful names

Create a top-level `README.md`

Currently we only have README.md files for the subdirectories Haskell and Isabelle. Our goal is to create a top-level README.md as well.

Informally prove equivalence between filtering on receipt and filtering on delivery

Issue #15 introduced the notion of relaying network. In this issue, we consider relaying networks that also filter packets according to some given predicate. There are two filtering strategies: filtering packets as they are received via internal links and filtering packets before delivering them to the user. Our goal is to prove that these two strategies have the same external behavior.

• Develop a notion of behavioral equivalence suitable for this example
• Specify useful auxiliary facts
• Prove the auxiliary facts
• Prove the actual theorem

Add support for multiple parallel composition

The definition of distributors in #36 uses a construct for multiple parallel composition with an associated notation ∏x←xs. P x for expressing the composition of the processes P x, where x is taken from the list xs, and a final process 𝟬. We reckon that this construct and its notation will be useful in other places as well.

Our goal is to implement the parallel composition construct and its notation in the Chi_Calculus session. Our implementation shall closely follow the one of prod_list from HOL.Groups_List and its notation _prod_list. This particularly means the following:

• Bracketing is right-leaning.

• The parallel composition construct does not apply a function to the given list elements before composing. Such function application is realized through the definition of the notation.

Modularize the definition of the basic transition system

Our goal is to split the definition of the basic transition system into the following three parts:

1. atomic rules

2. rules for scoped transitions

3. recursion (“tying the knot”)

This split will be helpful for later developments, as it will allow us to refer to different parts of the transition system definition individually.

Replace `loss_and_duplication` by `duploss`

The use of loss_and_duplication in identifiers makes these very long. Therefore we want to shorten loss_and_duplication to duploss. While we don’t know about any precedent use of the term “duploss” in IT, we recognize that this word has already been used in genetics.

Generalize and otherwise improve the proofs of the basic bisimilarity core laws

We have implemented a number of core laws about the basic strong bisimilarity relation, namely compatibility (preservation) laws, scope extension laws, and neutrality, associativity, and commutativity of parallel composition. These laws have counterparts for the basic weak bisimilarity relation, but these haven’t been proved yet.

Incidentally, the proofs of the core laws for the strong case can be easily generalized to also cover the weak case. This is because it’s possible to prove weak analogs of the introduction rules of the basic strong transition relation. The generalization essentially works by replacing all applications of these introduction rules with their weak counterparts.

Our goal is to generalize the proofs as described and in the process also improve them in other ways. In particular, we want to use more efficient proof methods and avoid more boilerplate in conjunction with NewChannel than before by proving bisimilarities using simulation up to restriction.

• Implement a framework for employing simulation up to restriction in bisimilarity proofs
• Prove the weak analogs of the introduction rules of the basic strong transition relation
• Generalize and otherwise improve the proofs of the core laws

Move `Utilities` out of `Transition_Systems`

Currently the theory Utilities is part of the Transition_Systems session, although it contains general-purpose code that is not tied to transition systems. Our goal is to move it to a session of its own.

Fix typo in name of `bidirectional_bridge_commutativity` lemma

Our goal is to rename birectional_bridge_commutativity to bidirectional_bridge_commutativity.

Fill the holes in the proof of the relaying–broadcasting equivalence theorem

Currently we don’t have simplifier support for bisimilarity reasoning yet, because #10 hasn’t been resolved yet. Therefore the proof of the relaying–broadcasting equivalence theorem contains fake proofs (sorry) for numerous steps. Our goal is to replace these fake proofs by proper proofs, building on the solution to #10.

Add an automatic proof method that shows a given set of possible transitions to be complete

When proving that a certain relation is a simulation, one often needs to consider all forms of transitions possible from a process of a certain shape. Applying case distinction repeatedly for this purpose is laborious and leads to complicated proofs.

In an informal proof, one would typically state the ultimate cases right away and assume that the reader is able to figure out why the given list of cases is comprehensive. Our goal is to make an analogous approach possible for formal proofs in Isar. The user should be able to state the possible cases using the consider construct and let Isabelle automatically proof the elimination rule created by that.

For this purpose, we want to implement a proof method that constructs proofs of such elimination rules. This proof method should make use of elimination rules of transition relations as well as higher-level elimination rules derived from them for more specific shapes of processes. The user should be able to specify the set of rules to apply via a dynamic fact (see Subsubsection 1.3.1 of the Eisbach User Manual).

• Conduct manual experiments to figure out an appropriate proof method definition
• Research whether Eisbach supports different definitions of a dynamic fact for different interpretations of a locale
• Implement the proof method
• Implement higher-level elimination rules

Formalize the proof of equivalence between filtering on receipt and filtering on delivery

Issue #17 asks to develop an informal proof of equivalence between filtering on receipt and filtering on delivery. Our goal is to formalize this proof.

• Prove the auxiliary facts
• Prove the actual theorem

Prove the weak analogs of the basic transition rules

Replacing the basic strong transition relation by the basic weak transition relation in the basic transition rules leads to true statements. Our goal is to prove these statements.

Implement the semantics of the flow language

Our goal is to implement the semantics of the flow language as a function from flows to processes that describe networks that realize these flows.

Move bridge support to the `Chi_Calculus` session

Bridges were previously called “links”, because they were used to represent network links. Meanwhile we represent links differently (by unreliable channels), but bridges have turned out to be useful nevertheless. Since they seem to be a more fundamental concept, we want to move their formalization from Chi_Calculus_Examples to Chi_Calculus.

Add support for automatic conversion of equivalences into laxer equivalences

Behavioral equivalences in applications are typically expressed using proper weak bisimilarity. However, various fundamental bisimilarity laws hold also with stricter bisimilarity relations, namely proper strong bisimilarity or one of the bisimilarity relations of the basic transition system. When implementing such bisimilarity laws as Isabelle lemmas, we always want to state only the version with the strictest bisimilarity relation possible, which we can convert into laxer versions when needed. However, manual application of the conversion laws is cumbersome.

Our goal is to develop a proof method that applies conversion into laxer bisimilarity laws automatically. We plan to make this proof methods so general that it not only works for bisimilarities but for arbitrary equivalence relations.

Move the proofs of bisimilarity core laws into separate theories

Currently the proofs of the bisimilarity core laws of the basic and the proper transition system are part of the theories Basic_Transition_System and Proper_Transition_System respectively. Our plan is to move them into new, dedicated theories Basic_Bisimilarity_Core_Laws and Proper_Bisimilarity_Core_Laws.

Add Isabelle export of Haskell-embedded ♮-calculus code

Our goal is to implement an interpretation that turns a ♮-calculus program into Isabelle source code that represents this program using the Isabelle embedding of the calculus.

Formally prove the actual forwarding–broadcasting equivalence theorem

Our goal is to formally prove that a diamond-shaped forwarding mesh with a backlink and a corresponding broadcasting network are bisimilar if receive channels are lossy.

Purge `bisimilarity_standard`

Currently, the bisimilarity_proof_method does the following:

1. Reduce a goal of the form ⟦ A⇩1; …; A⇩n ⟧ ⟹ s ∼ t to ⟦ A⇩1; …; A⇩n ⟧ ⟹ 𝒳 s t and 𝒳 ≤ (∼)

2. Reduce 𝒳 ≤ (∼) to symp 𝒳 and sym 𝒳 (using in_bisimilarity_standard)

3. Reduce symp 𝒳 to an equivalent statement that uses plain logic instead of operations on relations

4. Reduce sim 𝒳 to an equivalent statement that uses plain logic instead of operations on relations

Our goal is to purge bisimilarity_standard by performing the following:

• Move 4 to a separate proof method is_simulation_standard

• Remove 3

• Remove 2 (but keep in_bisimilarity_standard)

Replace `link` by `bridge`

We used to represent network links by processes that forward packets. Meanwhile, however, we represent network links by channels and use forwarding processes for different means. Therefore we don’t want to use the term “link” for forwarding processes anymore but refer to such processes as “bridges”.

Implement the syntax of the flow language

Our goal is to implement the syntax of the flow language as an algebraic data type.

Generalize the proofs of the basic bisimilarity core laws

We have implemented a number of core laws about the basic strong bisimilarity relation, namely compatibility (preservation) laws, scope extension laws, and neutrality, associativity, and commutativity of parallel composition. These laws have counterparts for the basic weak bisimilarity relation, but these haven’t been proved yet.

Incidentally, the proofs of the core laws for the strong case can be easily generalized to also cover the weak case. This is because the weak analogs of all basic transition rules hold (see #76). The generalization works by replacing all applications of basic transition rules with applications of fact parameters that can be specialized to either the basic transition rules or their weak analogs. Our goal is to generalize the proofs in this way.

Separate the loss servers from the bridges in `distributor_split`

Currently the distributor_split lemma is stated as follows:

distributor_split:
  ¤⇧+a ∥ ∏b ← bs. ¤⇧?b ∥ a ⇒ bs ≈⇩♭ ¤⇧+a ∥ ∏b ← bs. (¤⇧?b ∥ a → b)

Our goal is to separate the loss servers ¤⇧?b from the bridges a → b on the right-hand side, to make the statement conform to our usual style of putting all loss servers before any bridge. This will result in the following statement:

distributor_split:
  ¤⇧+a ∥ ∏b ← bs. ¤⇧?b ∥ a ⇒ bs ≈⇩♭ ¤⇧+a ∥ ∏b ← bs. ¤⇧?b ∥ ∏b ← bs. a → b

Besides achieving stylistic consistency, this new statement has the advantage of making it clear that the loss servers on both sides of the bisimilarity are the same.

Formally prove `distributor` core lemma

Our goal is to formally prove the distributor core lemma described in #36.

An informal proof of this lemma is given in #15 (comment).

Reduce the boilerplate in the proofs of the basic bisimilarity core laws

Currently the proofs of the bisimilarity core laws of the basic transition system are suffering from unnecessary boilerplate. Our goal is to reduce this boilerplate by a more advanced handling of the rules for scoped transitions and the use of “up to” techniques.

Add skeletons of `multi_receive` core lemmas

Our goal is to add skeletons of the following core lemmas about multi_receive:

multi_receive_split:
  ⟦⋀x. P x →⇩♭⦃τ⦄ 𝟬; ⋀x. Q x →⇩♭⦃τ⦄ 𝟬⟧ ⟹
  ¤⇧+a ∥ a ▹⇧∞ x. (P x ∥ Q x) ≈⇩♭ ¤⇧+a ∥ a ▹⇧∞ x. P x ∥ a ▹⇧∞ x. Q x
context_localization:
  a ▹⇧∞ x. P x ∥ b ▹⇧∞ x. Q x ≈⇩♭ a ▹⇧∞ x. P x ∥ b ▹⇧∞ x. (a ▹⇧∞ x. P x ∥ Q x)

Formally prove lemma `sidetrack_addition`

Our goal is to formally prove the sidetrack_addition lemma described in #65.

Add skeleton of distributor support

A distributor is like a bridge, except that it allows to relay a packet to an arbitrary number of channels (and multiple times to the same channel). Distributors can be defined in Isabelle as follows:

abbreviation distributor :: "[chan, chan list] ⇒ process" (infix "⇒" 100) where
  "a ⇒ bs ≡ a ▹⇧∞ x. ∏b←bs. b ◃ x"

Our goal is to add the above definition to the χ-calculus formalization along with a skeleton of the following distributor core lemma:

distributor_split:
  ¤⇧+a ∥ ∏b ← bs. ¤⇧?b ∥ a ⇒ bs ≈⇩♭ ¤⇧+a ∥ ∏b ← bs. (¤⇧?b ∥ a → b)

Formally prove `duploss` core lemmas

Our goal is to formally prove the duploss core lemmas described in #33.

Informal proofs of these lemmas are given in #15 (comment).

Is there a way to generate a PDF file or some other kind of easily read documentation from the Isabelle sources?

tx in advance...i understood from a tweet by Charles that there was a pdf here for Chi Calculus (link: https://twitter.com/IOHK_Charles/status/999453156319752192)

Add a skeleton of lemma `sidetrack_addition`

Our goal is to add a skeleton of the following lemma:

sidetrack_addition:
  ∏b ← bs. ¤⇧?b ∥ a ⇒ (b⇩0 # bs) ≈⇩♭ ∏b ← bs. ¤⇧?b ∥ a ⇒ (b⇩0 # bs) ∥ a → b⇩0

Add missing spaces between transition operators and residuals

When writing a transitions where the residual explicitly mentions a label and a target process, we don’t put a space between the transition operator and the residual; so we write, for example, p →⇩♭⦃α⦄ q. In the past, we also didn’t put a space when the residual was a variable; so we wrote, for example, p →⇩♭c. However, we consider the latter bad practice meanwhile.

Our goal is to insert spaces between the transition operator and the residual where there are currently none.

Remove obsolete relaying–broadcasting equivalence code

We already have a partial proof of relaying–broadcasting equivalence, but it refers to our previous, inferior way of representing networks as processes.

Our goal is to remove this partial proof, in order to make way for a new proof based on our new, superior network representation (see #26). This removal shall cover also the skeletons of source_shift and dead_end_collapse, as these will become obsolete through resolving #35.

Add simplifier support for equivalence reasoning

Currently, when reasoning with bisimilarities, we need to apply core bisimilarities manually. This leads to long and hard-to-create proofs. Especially the need for manual application of compatibility (preservation) laws and associativity of parallel composition constitutes a hardship.

Our goal is to employ Isabelle’s simplifier to automate the creation of such boring proof steps. A challenge is that the simplifier seems to work only for equational reasoning by default. We want to make it work also for equivalence reasoning and thus in particular for bisimilarity reasoning.

• Research how to best use the simplifier for reasoning with arbitrary equivalences
• Implement simplifier support for equivalence reasoning

Formalize the proof of relaying–broadcasting equivalence

Issue #15 asks to develop an informal proof of relaying–broadcasting equivalence. Our goal is to formalize this proof.

• Prove the auxiliary facts
• Prove the actual theorem