Skip to content
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

Concretize all abstract functions in the IO-spec #231

Merged
merged 21 commits into from
Nov 15, 2023
Merged

Concretize all abstract functions in the IO-spec #231

Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
6ae29eb
making IO-spec dependend on abstract dataplane
mlimbeck Oct 11, 2023
7fec531
renaming Abs_Dataplane to DataPlaneSpec
mlimbeck Oct 12, 2023
ac31b85
removing local state from IO-spec next place functions
mlimbeck Oct 12, 2023
03ec019
rewriting IO-spec with match clause
mlimbeck Oct 12, 2023
491e444
comment out unnecessary functions
mlimbeck Oct 12, 2023
ed9ade0
providing bodies to abstract functions in IO-spec
mlimbeck Oct 12, 2023
34c58ad
Merge branch 'master' into instantiate-IO-Spec-functions
jcp19 Oct 13, 2023
11ca307
Merge remote-tracking branch 'remotescion/master' into instantiate-IO…
mlimbeck Oct 18, 2023
e4be0b8
merge problems fix
mlimbeck Oct 18, 2023
37c7ac6
cosmetic changes
mlimbeck Oct 18, 2023
a0b37b6
IO-spec fix
mlimbeck Oct 18, 2023
0c2ee68
adding receiving interface to topology
mlimbeck Oct 19, 2023
33cb8d5
concretize dp3s_forward_ext
mlimbeck Nov 1, 2023
d1a45a2
Merge branch 'master' into instantiate-IO-Spec-functions
jcp19 Nov 9, 2023
dc6f540
Apply suggestions from code review
mlimbeck Nov 14, 2023
0203251
minor improvements
mlimbeck Nov 14, 2023
4c87477
minor improvements
mlimbeck Nov 14, 2023
193add2
adding missing comment
mlimbeck Nov 14, 2023
6be6ae6
renaming core and asid function
mlimbeck Nov 14, 2023
6bf4081
Update verification/io/io-spec.gobra
jcp19 Nov 15, 2023
59d3019
precondition for link_type function
mlimbeck Nov 15, 2023
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
1 change: 1 addition & 0 deletions verification/io/dataplane_abstract.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ pure func (dp DataPlaneSpec) GetNeighborIA(ifs IO_ifs) IO_as {
return dp.neighborIAs[ifs]
}

// This function corresponds to function 'asid' in the IO spec
ghost
decreases
pure func (dp DataPlaneSpec) GetLocalIA() IO_as {
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
Expand Down
Loading