Fix some FPs based on verus-cheat-examples from Chenyuan.

[XuhengLi]

The patch fixed some false positives from Chenyuan's example.

But some remain unclear or tricky. Details below:

=== o-IR__marshal_v__impl2__lemma_serialize_injective-20251126-203400 (26 test cases) ===

1. [FAIL] fix-a15-uselemma-candidate-1.rs - disallowed changes
   The candidate added new proof-lemma functions with unimplemented!() bodies.
   Can you let me know if this was intended and safe?

(None)
=========================
#[verifier::external_body]
proof fn lemma_spec_u64_to_le_bytes_len(x: u64)
    ensures
        spec_u64_to_le_bytes(x).len() == 8
  {
     unimplemented!()
  }

2. [FAIL] fix-a2-seqsetmap-candidate-1.rs - disallowed changes
   Similarly, the candidates are added with a #[verifier::external_body] and adding unimplemented!() to the lemma.

proof fn lemma_serialize_injective(self: &Self, other: &Self) {
}
=============
#[verifier::external_body]
proof fn lemma_serialize_injective(self: &Self, other: &Self) {
  unimplemented!()
}

=== o-IR__marshal_v__impl3__lemma_serialize_injective-20251126-215955 (21 test cases) ===
[FAIL] fix-a4-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a5-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a6-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a8-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a9-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a10-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a11-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a12-uselemma-candidate-1.rs - disallowed changes
[FAIL] fix-a13-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a15-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a17-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a18-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a19-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a20-case_analysis-candidate-1.rs - disallowed changes
3. All of the examples failed for the same reason. I am not sure if this is safe or not -- what is the default type for 0? If it's u8 , I think it's a relatively quick fix; otherwise, I think we should just make it unsafe.

 open spec fn ghost_serialize(&self) -> Seq<u8> {
    match self {
          None => seq![0], 
 ========================
 open spec fn ghost_serialize(&self) -> Seq<u8> {
    match self {
          None => seq![0u8],

[FAIL] fix-a3-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a7-case_analysis-candidate-1.rs - disallowed changes
[FAIL] fix-a16-case_analysis-candidate-1.rs - disallowed changes
4. Pre/post-conditions are added to the lemma - is this allowed?

proof fn lemma_serialize_injective(self: &Self, other: &Self) {
======================
proof fn lemma_serialize_injective(self: &Self, other: &Self)
    requires
    ....
    ensures
    ....

=== o-NR__theorem__lemma1_init-20251203-234417 (19 test cases) ===
[FAIL] fix-a18-postcondition_repair-candidate-1.rs - disallowed changes
5. Hmmmm, the content of the original files seems to be scratched...

=== o-OS__va_range__impl2_new-20251204-153754 (22 test cases) ===
[FAIL] fix-a1-postcondition_repair-candidate-1.rs - disallowed changes
[FAIL] fix-a11-seqsetmap-candidate-1.rs - disallowed changes
[FAIL] fix-a12-seqsetmap-candidate-1.rs - disallowed changes
[FAIL] fix-a17-uselemma-candidate-1.rs - disallowed changes
[FAIL] fix-a20-uselemma-candidate-1.rs - disallowed changes
[FAIL] fix-a3-seqsetmap-candidate-1.rs - disallowed changes
[FAIL] fix-a4-seqsetmap-candidate-1.rs - disallowed changes
[FAIL] fix-a5-seqsetmap-candidate-1.rs - disallowed changes
[FAIL] fix-a6-seqsetmap-candidate-1.rs - disallowed changes
[FAIL] fix-a8-seqsetmap-candidate-1.rs - disallowed changes
6. This one is tricky. Semantically, they are equivalent wrt the exec portion but much more efforts are needed
from a checker's PoV to establish the equivalence...

{
      let seq = Ghost(arbitrary()); // TODO: please replace arbitrary() with the right expression
      Self { start: va, len: len, view: seq }
}
===============================
{
    let seq = Ghost(arbitrary()); // TODO: please replace arbitrary() with the right expression
    let result = Self { start: va, len: len, view: seq };
    proof {
        assert(result.start + result.len * 4096 < usize::MAX);
        assert(spec_va_4k_valid(result.start));
        assert([email protected]() == result.len);
        assert([email protected]_duplicates());
        assert(forall|i: int| #![trigger result@[i]] 0 <= i < result.len ==> spec_va_4k_valid(result@[i]));
        assert(result.view_match_spec());
    }
    result
}

[XuhengLi]

@microsoft-github-policy-service agree

@microsoft-github-policy-service agree

[arsene1995]

Hi Xuheng, thanks for taking a look.

For 1 and 2 above:
Adding an external_body lemma function IS indeed UNsafe.

For 3, 4, 5: reporting them as unsafe is fine. Can we have output that indicates WHY or what part of the code led to the "unsafe" conclusion? As long as the output is more informative, it is all ok for case 3, 4, 5.

For 6:
I feel the example mixed up two separate things.

One:
replacing

{ 
   // the function body
   expr_to_return
}

with

{
   // the function body
   let r = expr_to_return
   r
}

It would be great if this change can be regarded as safe.
But, if not, I understand.

two:
replacing

      let seq = Ghost(arbitrary()); 

with

    let seq  = Ghost(a);

This is the number one source of false positives in my experience.
Can we ignore all the changes made to ghost expression?

[XuhengLi]

Hi Shan,

I have added some information for 3, 4, 5 in the output for my own debugging. I will think about how to make lynette generate more friendly output so we can parse it in Python.

For 6, that's a reasonable split! While the Ghost() one is relatively easy to check, the first one is indeed tricky, imo, since it involves changes in the control flow (to some extent). I will try to address the Ghost() case first. I will probably need some time to consider the other case.

[arsene1995]

Regarding debugging information:

• It would be great if some information can be printed about why a cheating is reported -- I hope such information is presented whenever a cheat is detected, which goes beyond the situations in these test examples.
• Xuheng, don't worry about the format of such information. The consumer of that information will NOT be our python program; it will be LLM. So, format does not matter at all. If you can read it, LLM can read it :-)

Regarding ghost variable thing:
Yeah, I understand this is not a small change.
A lot of times, there is no "Ghost(...)". It could simply be an assignment to a ghost variable or a ghost field.
I understand that any addition/update/deletion of assignment to a Rust variable should be disallowed; but I hope lynette can realize when the involved variables are ghost variables, and allow any changes related to ghost variables.

Thank you Xuheng!