From 02ee0994daa6473ce3b74ce96c27c5d64c764670 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 15 Jul 2024 17:47:44 -0700 Subject: [PATCH 1/3] Remove extra \n via comments inside &&& blocks --- src/lib.rs | 19 +++++++++++++++---- tests/verus-consistency.rs | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+), 4 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 01da399..7f5e9b7 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1076,19 +1076,30 @@ fn to_doc<'a>( Rule::bulleted_expr => block_braces(arena, map_to_doc(ctx, arena, pair), true), Rule::bulleted_expr_inner => { let pairs = pair.into_inner(); - let mut first = true; + let mut prefix_hardline = false; arena.concat(pairs.map(|p| { let d = to_doc(ctx, p.clone(), arena); match p.as_rule() { + Rule::COMMENT => { + // Prevent an unnecessary additional newline after comments + prefix_hardline = false; + d + } Rule::triple_and | Rule::triple_or => { - if first { - first = false; + if !prefix_hardline { + prefix_hardline = true; d } else { arena.hardline().append(d) } } - _ => d, + _ => { + if p.into_inner().flatten().last().unwrap().as_rule() == Rule::COMMENT { + // Prevent an unnecessary additional newline after comments + prefix_hardline = false; + } + d + } } })) } diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index 8c1c7dc..a82ad24 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1585,6 +1585,39 @@ fn verus_quantifier_and_bulleted_expr_precedence() { "###); } +#[test] +fn verus_bulleted_expr_comment_handling() { + let file = r#" +verus! { +fn foo() { + // these should stay together + &&& x + &&& y + // xy + &&& xy + // zzz + &&& z +} +} +"#; + + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + fn foo() { + // these should stay together + &&& x + &&& y + // xy + &&& xy + // zzz + &&& z + } + + } // verus! + "###); +} + #[test] fn verus_skip_leaves_code_unchanged() { let file = r#" verus! { spec fn foo() { 1 + 2 } #[verusfmt::skip] spec fn bar() { 1 + 2 } From 8a3cfffbdbf80fa37c77c17e213a0468dac59d48 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 15 Jul 2024 17:49:11 -0700 Subject: [PATCH 2/3] snap --- examples/ironfleet.rs | 18 +---------- examples/nr.rs | 30 ------------------- examples/pagetable.rs | 12 -------- .../source/vstd/std_specs/range.rs | 1 - 4 files changed, 1 insertion(+), 60 deletions(-) diff --git a/examples/ironfleet.rs b/examples/ironfleet.rs index cfa61dd..c7ac839 100644 --- a/examples/ironfleet.rs +++ b/examples/ironfleet.rs @@ -3253,7 +3253,6 @@ impl HostState { None => true, Some(host_state) => { &&& netc.ok() // port of env.ok.ok() - &&& host_state.invariants(&netc.my_end_point()) &&& crate::host_protocol_t::init( host_state@, @@ -3584,7 +3583,6 @@ impl HostState { &&& self.abstractable() &&& self.delegation_map.valid() // TODO why no valid_key? - &&& (forall|k| self.h@.dom().contains(k) ==> #[trigger] valid_value(self.h@[k])) &&& self.sd.valid() &&& match &self.received_packet { @@ -3609,7 +3607,6 @@ impl HostState { &&& self@.constants.me.abstractable() &&& self.num_delegations < self.constants.params.max_delegations // why did we move this here? - &&& self.constants.params@ == AbstractParameters::static_params() &&& self.resend_count < 100000000 } @@ -4088,13 +4085,11 @@ impl HostState { == netc.ok() // Because all `net_events` are sends, the condition "even if ok is false, if we sent at least one // packet..." is implied by "even if ok is false, if `net_events` has length > 0...". - &&& (ok || event_results.sends.len() > 0) ==> netc.history() == old_netc_history + event_results.ios // There's supposed to be a distinction between the ios that we intended to do and the // event_seq that we actually did. (See EventResult definition.) But in the interest of // mimicking Dafny Ironfleet, we make no such distinction. - &&& event_results.ios == event_results.event_seq() &&& event_results.well_typed_events() &&& ok ==> { @@ -4196,7 +4191,6 @@ impl HostState { ) // The Dafny Ironfleet "common preconditions" take an explicit cpacket, but we need to talk // about - &&& self.host_state_common_postconditions(*old(self), cpacket, sent_packets@) }), { @@ -5681,7 +5675,6 @@ pub open spec(checked) fn receive_packet( ||| { &&& pre.received_packet is None // No packet currently waiting to be processed (buffered in my state) // Record incoming packet in my state and possibly ack it - &&& SingleDelivery::receive(pre.sd, post.sd, pkt, ack, out) &&& if SingleDelivery::new_single_message(pre.sd, pkt) { post.received_packet == Some(pkt) // Enqueue this packet for processing @@ -5695,8 +5688,7 @@ pub open spec(checked) fn receive_packet( ..post } // Nothing else changes - } - ||| { + }||| { // internal buffer full or okay to ignore packets; drop this message and wait for it to be retransmitted. &&& pre.received_packet is Some || okay_to_ignore_packets() &&& post == pre @@ -9754,11 +9746,8 @@ pub fn receive_with_demarshal(netc: &mut NetClient, local_addr: &EndPoint) -> (r &&& (rr.is_Packet() ==> { &&& net_event@.is_Receive() &&& true // NetPacketIsAbstractable is true - &&& rr.get_Packet_cpacket().abstractable() // can parse u8s up to NetEvent. - &&& true // EndPointIsValidPublicKey - &&& !(rr.get_Packet_cpacket()@.msg is InvalidMessage) ==> { &&& rr.get_Packet_cpacket()@ == abstractify_net_packet_to_sht_packet( net_event@.get_Receive_r(), @@ -9834,9 +9823,7 @@ fn take_buf(buf: &mut Vec) { /// valid() pub open spec fn outbound_packet_is_valid(cpacket: &CPacket) -> bool { &&& cpacket.abstractable() // CPacketIsAbstractable - &&& cpacket.msg.is_marshalable() // CSingleMessageMarshallable - &&& ( !cpacket.msg.is_InvalidMessage()) // (out.msg.CSingleMessage? || out.msg.CAck?) @@ -9845,7 +9832,6 @@ pub open spec fn outbound_packet_is_valid(cpacket: &CPacket) -> bool { pub open spec fn send_log_entry_reflects_packet(event: NetEvent, cpacket: &CPacket) -> bool { &&& event.is_Send() &&& true // NetPacketIsAbstractable == EndPointIsAbstractable == true - &&& cpacket.abstractable() &&& cpacket@ == abstractify_net_packet_to_sht_packet(event.get_Send_s()) } @@ -10296,7 +10282,6 @@ pub enum ReceiveImplResult { pub open spec fn valid_ack(ack: CPacket, original: CPacket) -> bool { &&& ack.abstractable() &&& outbound_packet_is_valid(&ack) // how does this relate to abstractable? - &&& ack.src@ == original.dst@ &&& ack.dst@ == original.src@ } @@ -11455,7 +11440,6 @@ impl SingleDelivery { /// Protocol/SHT/SingleDelivery.i.dfy ShouldAckSingleMessage pub open spec(checked) fn should_ack_single_message(self, pkt: Packet) -> bool { &&& pkt.msg is Message // Don't want to ack acks - &&& { let last_seqno = tombstone_table_lookup(pkt.src, self.receive_state); pkt.msg.get_Message_seqno() <= last_seqno diff --git a/examples/nr.rs b/examples/nr.rs index 4806b98..cf92442 100644 --- a/examples/nr.rs +++ b/examples/nr.rs @@ -512,12 +512,10 @@ spec fn state_refinement_relation_basic( &&& (0 <= s.version && s.version <= s.log.len()) // the state corresponds to the state computed at the given version - &&& t.state == s.nrstate_at_version( s.version, ) // the request ids of the readonly/update requests and responses must be unique - &&& s.readonly_reqs.dom().disjoint(s.update_reqs.dom()) &&& s.readonly_reqs.dom().disjoint(s.update_resps.dom()) &&& s.update_reqs.dom().disjoint(s.update_resps.dom()) @@ -525,7 +523,6 @@ spec fn state_refinement_relation_basic( t.resps.dom(), ) // requests are complete: if a request in present in the AState then it must be present in the SState - &&& (forall|rid| (#[trigger] s.readonly_reqs.contains_key(rid) || #[trigger] s.update_reqs.contains_key(rid) || #[trigger] s.update_resps.contains_key(rid)) <==> (#[trigger] t.reqs.contains_key( @@ -534,7 +531,6 @@ spec fn state_refinement_relation_basic( rid, ))) // requests/responses in the rightmaps - &&& (forall|rid| #[trigger] t.reqs.contains_key(rid) && #[trigger] t.reqs[rid].is_Read() ==> s.readonly_reqs.contains_key(rid)) @@ -547,25 +543,21 @@ spec fn state_refinement_relation_basic( rid, )) // for all log entries > version, there must be a response with the given version - &&& (forall|v: LogIdx| s.version <= v && v < s.log.len() ==> update_response_with_version( s.update_resps, v, )) // for any two update responses, if the request id differs, the version in the log must also differ - &&& (forall|rid1, rid2| #[trigger] s.update_resps.contains_key(rid1) && #[trigger] s.update_resps.contains_key(rid2) && rid1 != rid2 ==> s.update_resps[rid1] != s.update_resps[rid2]) // for all update responses, the version must be within the log - &&& (forall|rid| #[trigger] s.update_resps.contains_key(rid) ==> s.update_resps[rid].0 < s.log.len()) // for all update requests, they must be part of the requests and the operation must match - &&& (forall|rid| #[trigger] s.update_reqs.contains_key(rid) ==> t.reqs.contains_key(rid) && t.reqs[rid] == InputOperation::
::Write( @@ -573,14 +565,12 @@ spec fn state_refinement_relation_basic( )) // forall update responses larger than the current version, they must be in the requests, // the update operation must match - &&& (forall|rid| #[trigger] s.update_resps.contains_key(rid) && s.update_resps[rid].0 >= s.version ==> { &&& t.reqs.contains_key(rid) &&& t.reqs[rid] == InputOperation::
::Write(s.log[s.update_resps[rid].0 as int]) }) // for all update responses smaller than th eversion, they must be valid - &&& (forall|rid| #[trigger] s.update_resps.contains_key(rid) && s.update_resps[rid].0 < s.version ==> update_response_is_valid(s, t, r_points, rid)) @@ -3116,13 +3106,11 @@ pub open spec fn LogRangeMatchesQueue( &&& (logIndexLower == logIndexUpper ==> queueIndex == queue.len()) // otherwise, we check the log - &&& (logIndexLower < logIndexUpper ==> { &&& log.contains_key( logIndexLower, ) // local case: the entry has been written by the local node - &&& (log.index(logIndexLower).node_id == nodeId ==> { // there must be an entry in the queue that matches the log entry &&& queueIndex < queue.len() @@ -3140,7 +3128,6 @@ pub open spec fn LogRangeMatchesQueue( ) }) // remote case: the entry has been written by the local node, there is nothing to match, recourse - &&& (log.index(logIndexLower).node_id != nodeId ==> LogRangeMatchesQueue( queue, log, @@ -3169,13 +3156,11 @@ pub open spec fn LogRangeMatchesQueue2( &&& (logIndexLower == logIndexUpper ==> queueIndex == queue.len()) // otherwise, we check the log - &&& (logIndexLower < logIndexUpper ==> { &&& log.contains_key( logIndexLower, ) // local case: the entry has been written by the local node - &&& (log.index(logIndexLower).node_id == nodeId ==> { // there must be an entry in the queue that matches the log entry &&& queueIndex @@ -3183,7 +3168,6 @@ pub open spec fn LogRangeMatchesQueue2( // &&& updates.contains_key(queue.index(queueIndex as int)) // &&& updates.index(queue.index(queueIndex as int)).is_Placed() // &&& updates.index(queue.index(queueIndex as int)).get_Placed_idx() == logIndexLower - &&& LogRangeMatchesQueue2( queue, log, @@ -3195,7 +3179,6 @@ pub open spec fn LogRangeMatchesQueue2( ) }) // remote case: the entry has been written by the local node, there is nothing to match, recourse - &&& (log.index(logIndexLower).node_id != nodeId ==> LogRangeMatchesQueue2( queue, log, @@ -7410,7 +7393,6 @@ impl NrLog
{ // // The following will result in a resource limit exceeded // - &&& log_entries[i]@.value.op == operations[i as int] // @@ -8205,7 +8187,6 @@ impl NrLogAppendExecDataGhost
{ &&& self.combiner@@.value.is_Placed() ==> self.pre_exec(responses) &&& self.cb_combiner@@.value == pre.cb_combiner@@.value // other fields in common_pred - &&& self.request_ids == pre.request_ids } @@ -9925,14 +9906,12 @@ impl ThreadToken
{ &&& (self.tid as nat) < MAX_THREADS_PER_REPLICA // &&& self.fc_client@@.instance == fc_inst - &&& self.batch_perm@@.value.is_None() &&& self.fc_client@@.key == self.tid as nat } pub open spec fn wf(&self, replica: &Replica
) -> bool { &&& self.wf2(replica.spec_id() + 1) // +1 here because ids got < replicas - &&& self.rid@ == replica.spec_id() &&& self.fc_client@@.instance == replica.flat_combiner_instance &&& self.batch_perm@@.pcell == replica.contexts[self.thread_id_spec() as int].batch.0.id() @@ -10695,11 +10674,9 @@ impl crate::NR
for NodeReplicated
{ &&& self.cyclic_buffer_instance@ == self.log.cyclic_buffer_instance@ // the number of replicas should be the as configured - &&& self.replicas.len() <= MAX_REPLICAS // the replicas should be well-formed and the instances match - &&& (forall|i| 0 <= i < self.replicas.len() ==> { &&& (#[trigger] self.replicas[i]).wf() @@ -11465,7 +11442,6 @@ pub open spec fn is_readonly_ticket( &&& ticket@.value.is_Init() && ticket@.value.get_Init_op() == op // requires ticket.loc == TicketStubSingletonLoc.loc() - &&& ticket@.instance == log } @@ -11480,7 +11456,6 @@ pub open spec fn is_readonly_stub( &&& stub@.instance == log // ensures ssm.IsStub(rid, output, stub.val) -> (exists ctail, op, nodeid :: stub == ReadOp(rid, ReadonlyDone(op, output, nodeid, ctail))) - &&& stub@.key == rid &&& stub@.value.is_Done() &&& stub@.value.get_Done_ret() == result @@ -11496,7 +11471,6 @@ pub open spec fn is_update_ticket( &&& ticket@.value.is_Init() && ticket@.value.get_Init_op() == op // requires ticket.loc == TicketStubSingletonLoc.loc() - &&& ticket@.instance == log } @@ -11511,7 +11485,6 @@ pub open spec fn is_update_stub( &&& stub@.instance == log // ensures ssm.IsStub(rid, output, stub.val) -> (exists log_idx :: stub == UpdateOp(rid, UpdateDone(output, log_idx))) - &&& stub@.key == rid &&& stub@.value.is_Done() &&& stub@.value.get_Done_ret() == result @@ -11937,19 +11910,16 @@ pub open spec fn behavior_equiv( ||| (a.is_Inited() && b.is_Inited()) // || (a.Stepped? && a.op.InternalOp? && equiv(a.tail, b)) - ||| (a.is_Stepped() && a.get_Stepped_1().is_Internal() && behavior_equiv( *a.get_Stepped_2(), b, )) // || (b.Stepped? && b.op.InternalOp? && equiv(a, b.tail)) - ||| (b.is_Stepped() && b.get_Stepped_1().is_Internal() && behavior_equiv( a, *b.get_Stepped_2(), )) // || (a.Stepped? && b.Stepped? && a.op == b.op && equiv(a.tail, b.tail)) - ||| (a.is_Stepped() && b.is_Stepped() && a.get_Stepped_1() == b.get_Stepped_1() && behavior_equiv(*a.get_Stepped_2(), *b.get_Stepped_2())) } diff --git a/examples/pagetable.rs b/examples/pagetable.rs index 6e9c162..84c528c 100644 --- a/examples/pagetable.rs +++ b/examples/pagetable.rs @@ -3573,7 +3573,6 @@ pub mod PT { // reflexive &&& pt.used_regions.contains(pt.region) // transitive - &&& forall|i: nat, r: MemRegion| #![trigger pt.entries[i as int].get_Some_0().used_regions.contains(r), pt.used_regions.contains(r)] i < pt.entries.len() && pt.entries[i as int].is_Some() @@ -4139,14 +4138,12 @@ pub mod PT { new_regions, ) // and only those we added - &&& new_regions.disjoint(old(mem).regions()) &&& (forall|r: MemRegion| new_regions.contains(r) ==> !(#[trigger] pt.used_regions.contains( r, ))) // Invariant preserved - &&& inv_at( mem, pt_res, @@ -4154,7 +4151,6 @@ pub mod PT { ptr, ) // We only touch already allocated regions if they're in pt.used_regions - &&& (forall|r: MemRegion| !(#[trigger] pt.used_regions.contains(r)) && !(new_regions.contains(r)) ==> mem.region_view(r) === old(mem).region_view(r)) @@ -5873,7 +5869,6 @@ pub mod PT { removed_regions, ) // and only those we removed - &&& (forall|r: MemRegion| removed_regions.contains(r) ==> !(#[trigger] mem.regions().contains(r))) &&& (forall|r: MemRegion| @@ -5881,7 +5876,6 @@ pub mod PT { r, ))) // Invariant preserved - &&& inv_at( mem, pt_res, @@ -5889,7 +5883,6 @@ pub mod PT { ptr, ) // We only touch regions in pt.used_regions - &&& (forall|r: MemRegion| !(#[trigger] pt_res.used_regions.contains(r)) && !( #[trigger] removed_regions.contains(r)) ==> mem.region_view(r) === old( @@ -9864,7 +9857,6 @@ pub open spec fn step_ReadWrite( base + pte.frame.size, ) // .. and the result depends on the flags. - &&& match op { RWOp::Store { new_value, result } => { if pmem_idx < c.phys_mem_size && !pte.flags.is_supervisor @@ -9894,7 +9886,6 @@ pub open spec fn step_ReadWrite( vmem_idx, ) // .. and the result is always a pagefault and an unchanged memory. - &&& s2.mem === s1.mem &&& match op { RWOp::Store { new_value, result } => result.is_Pagefault(), @@ -10602,7 +10593,6 @@ pub open spec fn step_ReadWrite( &&& paddr === (pte.frame.base + (vaddr - base)) as nat // .. and the result depends on the flags. - &&& match op { RWOp::Store { new_value, result } => { if pmem_idx < s1.mem.len() && !pte.flags.is_supervisor @@ -10634,7 +10624,6 @@ pub open spec fn step_ReadWrite( &&& between(vaddr, base, base + pte.frame.size) }) // .. and the result is always a pagefault and an unchanged memory. - &&& s2.mem === s1.mem &&& match op { RWOp::Store { new_value, result } => result.is_Pagefault(), @@ -10647,7 +10636,6 @@ pub open spec fn step_ReadWrite( pub open spec fn step_PTMemOp(s1: HWVariables, s2: HWVariables) -> bool { &&& s2.mem === s1.mem // s2.tlb is a submap of s1.tlb - &&& forall|base: nat, pte: PageTableEntry| s2.tlb.contains_pair(base, pte) ==> s1.tlb.contains_pair( base, diff --git a/examples/verus-snapshot/source/vstd/std_specs/range.rs b/examples/verus-snapshot/source/vstd/std_specs/range.rs index d6164b8..5426738 100644 --- a/examples/verus-snapshot/source/vstd/std_specs/range.rs +++ b/examples/verus-snapshot/source/vstd/std_specs/range.rs @@ -68,7 +68,6 @@ impl< &&& self.cur.spec_is_lt(self.end) || self.cur == self.end // TODO (not important): use new "matches ==>" syntax here - &&& if let Some(init) = init { &&& init.start == init.cur &&& init.start == self.start From 2bcea185436af4526e3b90d5f89af1e979c48424 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 15 Jul 2024 18:23:23 -0700 Subject: [PATCH 3/3] Update changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index b948294..c3b4705 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ # Unreleased +* Handle comments inside `&&&`/`|||`-bulleted blocks better + # v0.3.8 * Support dividing statement lists into clauses/stanzas