Skip to content
This repository has been archived by the owner on May 3, 2024. It is now read-only.

Commit

Permalink
improve IO-spec
Browse files Browse the repository at this point in the history
  • Loading branch information
mlimbeck committed Jul 24, 2023
2 parents 8a0452e + 4540095 commit bf2c331
Show file tree
Hide file tree
Showing 2 changed files with 70 additions and 17 deletions.
42 changes: 27 additions & 15 deletions verification/io/other_defs.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ type IO_msgterm adt {
}

MsgTerm_Num {
MsgTerm_Num_ int // formallized as nat in Isabelle
MsgTerm_Num_ uint // formallized as nat in Isabelle
}

MsgTerm_Key {
Expand All @@ -60,7 +60,7 @@ type IO_msgterm adt {
}

MsgTerm_FS {
MsgTerm_FS_ seq[IO_msgterm]
MsgTerm_FS_ set[IO_msgterm]
}

MsgTerm_MPair {
Expand Down Expand Up @@ -107,8 +107,6 @@ pure func (hf IO_HF) extr_asid() IO_as {
return hf.HVF.extract_asid()
}



// function 'toab' in Isabelle, originally of type HF_scheme -> aahi_scheme
ghost
pure
Expand Down Expand Up @@ -159,31 +157,46 @@ pure func link_type(p1 IO_as, p2 IO_ifs) IO_Link

ghost
decreases
pure func egif_prov2(hf1 IO_HF, asid IO_as) bool
pure func egif_prov2(hf1 IO_HF, asid IO_as) bool{
return egif2_type(hf1, asid, IO_Link(IO_CustProv{}))
}

ghost
decreases
pure func egif_core2(hf1 IO_HF, asid IO_as) bool
pure func egif_core2(hf1 IO_HF, asid IO_as) bool{
return egif2_type(hf1, asid, IO_Link(IO_PeerOrCore{}))
}

ghost
decreases
pure func egif_cust2(hf1 IO_HF, asid IO_as) bool
pure func egif_cust2(hf1 IO_HF, asid IO_as) bool{
return egif2_type(hf1, asid, IO_Link(IO_ProvCust{}))
}

ghost
decreases
pure func inif_cust2(hf1 IO_HF, asid IO_as) bool
pure func inif_cust2(hf1 IO_HF, asid IO_as) bool{
return inif2_type(hf1, asid, IO_Link(IO_ProvCust{}))
}

ghost
decreases
pure func inif_core2(hf1 IO_HF, asid IO_as) bool
pure func inif_core2(hf1 IO_HF, asid IO_as) bool{
return inif2_type(hf1, asid, IO_Link(IO_PeerOrCore{}))
}

ghost
decreases
pure func inif_prov2(hf1 IO_HF, asid IO_as) bool
pure func inif_prov2(hf1 IO_HF, asid IO_as) bool{
return inif2_type(hf1, asid, IO_Link(IO_CustProv{}))
}

ghost
decreases
pure func if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool
pure func if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool{
return ifs == none[IO_ifs] ? false : link_type(asid, get(ifs)) == link
//exists outif IO_ifs :: some(outif) == ifs && link_type(asid, outif) == link
}

type ext2_rec struct {
op1 IO_as
Expand Down Expand Up @@ -213,10 +226,9 @@ ghost
decreases
pure func dp2_in_ext(s IO_dp2_state, asid IO_as, ifs IO_ifs, pkt IO_pkt2) bool

// TODO: how is this defined?
// extract_asid
ghost
decreases
pure func (m IO_msgterm) extract_asid() IO_as

pure func (m IO_msgterm) extract_asid() IO_as {
return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_
}
/* End of To clarify */
45 changes: 43 additions & 2 deletions verification/io/router.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -27,11 +27,52 @@ pure func core_as_set() set[IO_as]

ghost
decreases
pure func hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool
pure func hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool {
return let inif := p4.InIF2 in
let egif := p4.EgIF2 in
let x := p4.HVF in
let ts := IO_msgterm(MsgTerm_Num{p2}) in
let uinfo := IO_msgterm(MsgTerm_FS{p3}) in
let l := IO_msgterm(MsgTerm_L{seq[IO_msgterm]{ts, if2term(inif), if2term(egif), uinfo}}) in
exists a IO_key :: x == mac(macKey(a), l)
}

//Helper function (not in Isabelle)
ghost
decreases
pure func asidToKey(asid IO_as) IO_key{
return IO_key(Key_macK{asid})
}

ghost
decreases
pure func macKey(key IO_key) IO_msgterm {
return IO_msgterm(MsgTerm_Key{key})
}

ghost
decreases
pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm {
return IO_msgterm( MsgTerm_Hash {
MsgTerm_Hash_ : IO_msgterm( MsgTerm_MPair{
MsgTerm_MPair_1 : fst,
MsgTerm_MPair_2 : snd,
}),
})
}

ghost
decreases
pure func if2term(ifs option[IO_ifs]) IO_msgterm {
return ifs == none[IO_ifs] ? MsgTerm_Empty{} : IO_msgterm(MsgTerm_AS{IO_as(get(ifs))})
}

ghost
decreases
pure func upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm]
pure func upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm] {
return let setHVF := set[IO_msgterm]{p2.HVF} in
(p1 union setHVF) setminus (p1 intersection setHVF)
}

ghost
decreases
Expand Down

0 comments on commit bf2c331

Please sign in to comment.