New API for typed-protocols #52
typed-protocols: internal lemmas module
- Loading branch information
commit bdf810084689ce0474687ff58f5be29c7858620c
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,133 @@ | ||
| {-# LANGUAGE DataKinds #-} | ||
| {-# LANGUAGE EmptyCase #-} | ||
| {-# LANGUAGE GADTs #-} | ||
| {-# LANGUAGE RankNTypes #-} | ||
| {-# LANGUAGE StandaloneKindSignatures #-} | ||
| {-# LANGUAGE TypeFamilies #-} | ||
| {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} | ||
|
|
||
| {-# HLINT ignore "Use camelCase" #-} | ||
|
|
||
| -- | The module contains exclusion lemmas which are proven using ad absurdum: | ||
| -- | ||
| -- * it's impossible for both client and server have agency | ||
| -- * it's impossible for either side to be in a terminal state (no agency) and | ||
| -- the other side have agency | ||
| -- | ||
| module Network.TypedProtocol.Lemmas where | ||
|
|
||
| import Data.Kind (Type) | ||
| import Network.TypedProtocol.Core | ||
|
|
||
|
|
||
| -- | An evidence that both relative agencies are equal to 'NobodyHasAgency'. | ||
| -- | ||
| type ReflNobodyHasAgency :: RelativeAgency -> RelativeAgency -> Type | ||
| data ReflNobodyHasAgency ra ra' where | ||
| ReflNobodyHasAgency :: ReflNobodyHasAgency | ||
| NobodyHasAgency | ||
| NobodyHasAgency | ||
|
|
||
|
|
||
| -- | A proof that if both @Relative pr a@ and @Relative (FlipAgency pr) a@ are | ||
| -- equal then nobody has agency. In particular this lemma excludes the | ||
| -- possibility that client and server has agency at the same state. | ||
| -- | ||
| exclusionLemma_ClientAndServerHaveAgency | ||
| :: forall (pr :: PeerRole) (a :: Agency) | ||
| (ra :: RelativeAgency). | ||
| SingPeerRole pr | ||
| -> ReflRelativeAgency a ra (Relative pr a) | ||
| -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) | ||
| -> ReflNobodyHasAgency (Relative pr a) | ||
| (Relative (FlipAgency pr) a) | ||
| exclusionLemma_ClientAndServerHaveAgency | ||
| SingAsClient ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency | ||
| exclusionLemma_ClientAndServerHaveAgency | ||
| SingAsServer ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency | ||
|
|
||
| exclusionLemma_ClientAndServerHaveAgency | ||
| SingAsClient ReflClientAgency x = case x of {} | ||
| exclusionLemma_ClientAndServerHaveAgency | ||
| SingAsServer ReflClientAgency x = case x of {} | ||
| exclusionLemma_ClientAndServerHaveAgency | ||
| SingAsClient ReflServerAgency x = case x of {} | ||
| exclusionLemma_ClientAndServerHaveAgency | ||
| SingAsServer ReflServerAgency x = case x of {} | ||
|
|
||
|
|
||
| -- | A proof that if one side has terminated, then the other side terminated as | ||
| -- well. | ||
| -- | ||
|
Comment on lines
+82
to
+84
Contributor
There was a problem hiding this comment. Same here: |
||
| terminationLemma_1 | ||
| :: SingPeerRole pr | ||
| -> ReflRelativeAgency a ra (Relative pr a) | ||
| -> ReflRelativeAgency a NobodyHasAgency (Relative (FlipAgency pr) a) | ||
| -> ReflNobodyHasAgency (Relative pr a) | ||
| (Relative (FlipAgency pr) a) | ||
| terminationLemma_1 | ||
| SingAsClient ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency | ||
| terminationLemma_1 | ||
| SingAsServer ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency | ||
| terminationLemma_1 SingAsClient ReflClientAgency x = case x of {} | ||
| terminationLemma_1 SingAsClient ReflServerAgency x = case x of {} | ||
| terminationLemma_1 SingAsServer ReflClientAgency x = case x of {} | ||
| terminationLemma_1 SingAsServer ReflServerAgency x = case x of {} | ||
|
|
||
|
|
||
| -- | Internal; only need to formulate auxiliary lemmas in the proof of | ||
| -- 'terminationLemma_2'. | ||
| -- | ||
| type FlipRelAgency :: RelativeAgency -> RelativeAgency | ||
| type family FlipRelAgency ra where | ||
| FlipRelAgency WeHaveAgency = TheyHaveAgency | ||
| FlipRelAgency TheyHaveAgency = WeHaveAgency | ||
| FlipRelAgency NobodyHasAgency = NobodyHasAgency | ||
|
|
||
|
|
||
| -- | Similar to 'terminationLemma_1'. | ||
| -- | ||
| -- Note: this could be proven the same way 'terminationLemma_1' is proved, but | ||
| -- instead we use two lemmas to reduce the assumptions (arguments) and we apply | ||
| -- 'terminationLemma_1'. | ||
| -- | ||
| terminationLemma_2 | ||
| :: SingPeerRole pr | ||
| -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) | ||
| -> ReflRelativeAgency a NobodyHasAgency (Relative pr a) | ||
| -> ReflNobodyHasAgency (Relative (FlipAgency pr) a) | ||
| (Relative pr a) | ||
bolt12 marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| terminationLemma_2 singPeerRole refl refl' = | ||
| case terminationLemma_1 singPeerRole | ||
| (lemma_flip singPeerRole refl) | ||
| (lemma_flip' singPeerRole refl') | ||
| of x@ReflNobodyHasAgency -> x | ||
| -- note: if we'd swap arguments of the returned @ReflNobodyHasAgency@ type, | ||
| -- we wouldn't need to pattern match on the result. But in this form the | ||
| -- lemma is a symmetric version of 'terminationLemma_1'. | ||
| where | ||
| lemma_flip | ||
| :: SingPeerRole pr | ||
| -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) | ||
| -> ReflRelativeAgency a (FlipRelAgency ra) (Relative pr a) | ||
|
|
||
| lemma_flip' | ||
| :: SingPeerRole pr | ||
| -> ReflRelativeAgency a ra (Relative pr a) | ||
| -> ReflRelativeAgency a (FlipRelAgency ra) (Relative (FlipAgency pr) a) | ||
|
|
||
| -- both lemmas are identity functions: | ||
| lemma_flip SingAsClient ReflClientAgency = ReflClientAgency | ||
| lemma_flip SingAsClient ReflServerAgency = ReflServerAgency | ||
| lemma_flip SingAsClient ReflNobodyAgency = ReflNobodyAgency | ||
| lemma_flip SingAsServer ReflClientAgency = ReflClientAgency | ||
| lemma_flip SingAsServer ReflServerAgency = ReflServerAgency | ||
| lemma_flip SingAsServer ReflNobodyAgency = ReflNobodyAgency | ||
|
|
||
| lemma_flip' SingAsClient ReflClientAgency = ReflClientAgency | ||
| lemma_flip' SingAsClient ReflServerAgency = ReflServerAgency | ||
| lemma_flip' SingAsClient ReflNobodyAgency = ReflNobodyAgency | ||
| lemma_flip' SingAsServer ReflClientAgency = ReflClientAgency | ||
| lemma_flip' SingAsServer ReflServerAgency = ReflServerAgency | ||
| lemma_flip' SingAsServer ReflNobodyAgency = ReflNobodyAgency | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.