Skip to content

Add missing proofs of properties of communication primitives #23

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 57 commits into
base: master
Choose a base branch
from
Draft

Add missing proofs of properties of communication primitives #23

Changes from all commits
Commits
Show all changes
57 commits
Select commit Hold shift + click to select a range
5d3b3ca
Add proof of `repeated_receive_split`
javierdiaz72 Nov 6, 2022
c14539f
Drop superfluous uses of lemma in `repeated_receive_split`
javierdiaz72 Nov 7, 2022
9a6f13c
Add proof of `repeated_receive_shortcut_redundancy`
javierdiaz72 Nov 9, 2022
819100f
Fix indentation in `repeated_receive_shortcut_redundancy`
javierdiaz72 Nov 10, 2022
d1b0426
Fix formatting of `∏` in auxiliary lemmas
javierdiaz72 Nov 10, 2022
7ef9b72
Add proof of `send_idempotency_under_duploss`
javierdiaz72 Nov 24, 2022
817fe9a
Merge `master` into `enhancement/communication-primitives-missing-pro…
javierdiaz72 Nov 24, 2022
cac3103
Add proof of `send_channel_switch`
javierdiaz72 Nov 25, 2022
016cfb1
Add `TODO` for `transition_from_unidirectional_bridge`
javierdiaz72 Nov 25, 2022
41458d4
Fix format of `repeated_receive_split` assumptions
javierdiaz72 Nov 29, 2022
f23b794
Add and use auxiliary lemmas for `repeated_receive_split`
javierdiaz72 Nov 29, 2022
b791356
Simplify `post_receive n X □` in `repeated_receive_split`
javierdiaz72 Nov 29, 2022
9241baa
Simplify `post_receive n X □` in shortcut redund. of `▹⇧∞`
javierdiaz72 Nov 29, 2022
34c8b2f
Add and use auxiliary lemma for shortcut_redund. of `▹⇧∞`
javierdiaz72 Nov 30, 2022
70ca492
Fix name clash
javierdiaz72 Nov 30, 2022
9d2a5a5
Adapt the code to the changes in `thorn-calculus`
javierdiaz72 Dec 2, 2022
a17ad2e
Adapt `transition_from_` lemmas to a middle-ground scheme
javierdiaz72 Dec 2, 2022
f703d9e
Adapt `transition_from_distributor` lemma to new scheme
javierdiaz72 Dec 2, 2022
a99d197
Fix indentation in `show ?thesis` steps
javierdiaz72 Dec 2, 2022
9c31389
Drop superfluous use of `post_receive_after_parallel`
javierdiaz72 Dec 2, 2022
a52b012
Stop using method repetition in one proof step
javierdiaz72 Dec 5, 2022
7135b17
Make use of `post_receive_after_general_parallel`
javierdiaz72 Dec 6, 2022
c222bf9
Simplify one proof step with the use of `erule`
javierdiaz72 Dec 6, 2022
5c44075
Split one line with `using` and `unfolding` into two lines
javierdiaz72 Dec 6, 2022
2c5363a
Simplify proof step with `simp only:` to restrict simpset
javierdiaz72 Dec 6, 2022
79369e8
Split one line with `using` and `unfolding` into two lines
javierdiaz72 Dec 6, 2022
2c15326
Simplify proof step with `simp only:` to restrict simpset
javierdiaz72 Dec 6, 2022
39ebd0d
Add `transition_from_loss` and `transition_from_duploss`
javierdiaz72 Dec 6, 2022
caf9c23
Add proof of `loop_redundancy_under_duploss`
javierdiaz72 Dec 6, 2022
86a04ae
Rename the `_transition` lemma for unidirectional bridges
javierdiaz72 Dec 6, 2022
aa05769
Simplify proof step by reducing the simpset
javierdiaz72 Dec 6, 2022
daa176f
Fix the format of `transition_from` lemmas statements
javierdiaz72 Dec 6, 2022
ca90926
Make `transition_from_duploss` hold "up to bisimilarity"
javierdiaz72 Dec 8, 2022
eba6125
Add `transition_from_bidirectional_bridge`
javierdiaz72 Dec 8, 2022
a597829
Overhaul `transition_from_bidirectional_bridge`
javierdiaz72 Dec 10, 2022
4d687ff
Join `using`, `unfolding` and `proof` lines into one line
javierdiaz72 Dec 11, 2022
45dee39
Make order of chained facts more user-friendly
javierdiaz72 Dec 11, 2022
d2ae386
Simplify `(simp only:, fastforce)` to just `simp`
javierdiaz72 Dec 11, 2022
4c51b5d
Simplify repeated `fastforce` to just `auto`
javierdiaz72 Dec 11, 2022
e97b959
Make order of chained facts more user-friendly
javierdiaz72 Dec 11, 2022
e281bac
Place `using` and chained facts in the same line
javierdiaz72 Dec 11, 2022
4f0ef4b
Switch from sequential composites to terminal proof steps
javierdiaz72 Dec 13, 2022
f0afd24
Include `𝟬`s in `transition_from_bidirectional_bridge`
javierdiaz72 Dec 13, 2022
a77cfba
Simplify proof of `transition_from_bidirectional_bridge`
javierdiaz72 Dec 13, 2022
e6279a8
Use highest-level `transition_from` lemmas based on context
javierdiaz72 Dec 13, 2022
b7efa26
Restrict simp rules for some proof steps involving `∏`
javierdiaz72 Dec 13, 2022
12a7e9c
Add proof of `receive_channel_switch`
javierdiaz72 Dec 15, 2022
f8805ef
Simplify `receive_channel_switch` proof using new approach
javierdiaz72 Dec 16, 2022
55b400e
Stop overanalyzing transitions from common contexts
javierdiaz72 Dec 20, 2022
e085e35
Overhaul `_transition` lemmas
javierdiaz72 Dec 22, 2022
e45125d
Improve naming of `_transition` lemmas for `duploss`
javierdiaz72 Dec 23, 2022
0509829
Adapt `distributor_transition` proof to the current style
javierdiaz72 Dec 23, 2022
f40d7ab
Move `_transition` lemmas to their correct positions
javierdiaz72 Dec 23, 2022
bc73dd3
Fix layout in `distributor_transition` proof
javierdiaz72 Dec 23, 2022
44280bc
Weaken derivatives of `_transition` lemmas for `duploss`
javierdiaz72 Dec 27, 2022
afbd55c
Weaken derivatives of `_transition` lemmas for `↔`
javierdiaz72 Dec 27, 2022
98edc9b
Restore `receive_channel_switch` along with its proof
javierdiaz72 Dec 29, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading