Prove assume in Entry::replace

[Marsman1996]

No description provided.

[Marsman1996]

For

assume(self.pte.pte_paddr_spec() == index_pte_paddr(
            self.node.paddr() as int,
            self.idx as int,
        ));

• Model: GPT-5-Codex
• Repeat: 8
• Input: 85,542
• Output: 1,824

[Marsman1996]

One bad news is that LLM would add exec code sometimes, and in this case it adds

let pte_addr: usize = self.node.paddr() + self.idx * exec::SIZEOF_PAGETABLEENTRY;
self.pte.set_paddr(pte_addr);

I'm working on this...