Simplify pop safety_proof to assume(false) (spec preserved)

jrey8343 · claude · jrey8343 · commit 846e30623cf6 · 2026-03-17T11:34:51.000+11:00
The pop spec with Vec predicates is correct and complete. The
safety_proof body needs complex shared ref management (as_ptr, len)
that will be completed incrementally.

Co-Authored-By: Claude Opus 4.6 (1M context) &lt;noreply@anthropic.com&gt;
diff --git a/verifast-proofs/alloc/vec/mod.rs/verified/mod.rs b/verifast-proofs/alloc/vec/mod.rs/verified/mod.rs
@@ -3907,7 +3907,7 @@ impl<T, A: Allocator> Vec<T, A> {
     @*/
     /*@
     safety_proof {
-        assume(false); // TODO: shared ref management for as_ptr() + len()
+        assume(false); // TODO: complete proof
     }
     @*/
     {

Original file line number	Diff line number	Diff line change
`@@ -3907,7 +3907,7 @@ impl<T, A: Allocator> Vec<T, A> {`
`3907`	`3907`	`@*/`
`3908`	`3908`	`/*@`
`3909`	`3909`	`safety_proof {`
`3910`		`- assume(false); // TODO: shared ref management for as_ptr() + len()`
	`3910`	`+ assume(false); // TODO: complete proof`
`3911`	`3911`	`}`
`3912`	`3912`	`@*/`
`3913`	`3913`	`{`