-
Notifications
You must be signed in to change notification settings - Fork 2
Integration of type refinements into verus
Joshua Gancher edited this page Jan 8, 2024
·
1 revision
A sufficiently abstracted header for an Owl procedure could be a valid Verus header. For example:
def bob_sent(t : tau) @ bob : Unit = () // Only for the happened predicate
type payload = x:tau{happened(bob_sent(x))}
name K : enckey payload @ alice, bob
struct T {
_thekey : Name(K)
}
def get_msg(t : T) @ alice : Option (if sec(K) then payload else Data<adv>) =
input i in
parse t as T(k) in
dec(k, i)
could turn into the pseudo-verus-ish code
abstract type T
abstract predicate sec_K()
abstract predicate happened_bob_sent(x : Vec<u8>)
fn get_msg(t : T) : (res : Option<Vec<u8>>)
ensures res.Some? /\ sec_K() ==> happened_bob_sent(x)
Given the above, arbitrary Verus code could then, for example, store authentic messages in an intermediate queue, and get the refinement that if a message is in the queue and sec_K, then the message was actually sent by bob.