-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Remove rest_pat from future work, since it has been addressed
- Loading branch information
Showing
2 changed files
with
73 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,7 +1,78 @@ | ||
use builtin::*; | ||
use builtin_macros::*; | ||
use vstd::map::*; | ||
use vstd::modes::*; | ||
use vstd::multiset::*; | ||
use vstd::pervasive::*; | ||
use vstd::seq::*; | ||
use vstd::set::*; | ||
|
||
use crate::abstract_end_point_t::*; | ||
use crate::app_interface_t::*; | ||
use crate::keys_t::*; | ||
use crate::network_t::*; | ||
|
||
verus! { | ||
|
||
fn test() { | ||
let x = (1,); | ||
/* | ||
This comment absorbes the newline that should separate it from the struct | ||
*/ | ||
struct Constants { b: int } | ||
|
||
|
||
// The first set of &&& get out-dented, while the second one is absorbed into a single line | ||
fn clone_value() -> (out: u8) | ||
ensures | ||
match value { | ||
Some(vec) => { | ||
&&& out.is_Some() | ||
&&& out.unwrap()@ == vec@ | ||
}, | ||
None => { | ||
&&& out.is_None() | ||
}, | ||
}, | ||
{ | ||
} | ||
|
||
// Weird formatting of the constructor in the second case | ||
pub fn clone_up_to_view(&self) -> (c: Self) | ||
ensures | ||
c@ == self@, | ||
{ | ||
match self { | ||
CMessage::GetRequest { k } => { CMessage::GetRequest { k: k.clone() } }, | ||
CMessage::SetRequest { k, v } => { CMessage::SetRequest { k: k.clone(), v: CMessage::clone_value(v) } }, | ||
} | ||
} | ||
|
||
// Weird formatting of the return value | ||
pub open spec fn abstractify_outbound_packets_to_seq_of_lsht_packets(packets: Seq<CPacket>) -> Seq< | ||
LSHTPacket, | ||
> | ||
recommends | ||
cpacket_seq_is_abstractable(packets), | ||
{ | ||
[] | ||
} | ||
|
||
// Weird indenting of the last line | ||
proof fn test() { | ||
assert_seqs_equal!(v@, | ||
old(v)@.subrange(0, start as int) + | ||
old(v)@.subrange(start as int + deleted as int, | ||
old(v)@.len() as int)); | ||
} | ||
|
||
// Why the extra newline for the semi-colon? | ||
fn test() -> u64 { | ||
proof { assert_sets_equal!(a, b); }; | ||
proof { | ||
assert_sets_equal!(a, b); | ||
assert_sets_equal!(c, d); | ||
}; | ||
5 | ||
|
||
} | ||
|
||
} // verus! |