Integration of type refinements into verus

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.