Update Submodules to '25.08-RC' (#968)

* updates to Viper '25.08-RC'

* fixes verification error in test case due to new incompleteness

Author: ArquintL

silver-sif-extension

@@ -80,6 +80,17 @@ func (b BoundedMonotonicSet) ContainsImpliesFContains(i uint16) {
 		b.fcontainshelper(i)
 }
 
+ghost
+opaque
+requires 0 <= i && i <= 256
+requires forall i uint16 :: 0 <= i && i < 256 ==>
+	(i elem domain(b.valuesMap) && acc(b.valuesMap[i], _))
+decreases
+pure func (b BoundedMonotonicSet) fnotcontainshelperUpTo(i uint16) bool {
+    return forall j uint16 :: { b.fcontainshelper(j) } 0 <= j && j < i ==>
+        !b.fcontainshelper(j)
+}
+
 ghost
 ensures res.Inv()
 ensures forall i uint16 :: 0 <= i && i < 256 ==>
@@ -106,23 +117,29 @@ func Alloc() (res BoundedMonotonicSet) {
 		b.valuesMap[i] = new(bool)
 	}
 
+	assert reveal b.fnotcontainshelperUpTo(0)
+
 	invariant 0 <= i && i <= 256
-	invariant forall j uint16 :: 0 <= j && j < i ==>
+	invariant forall j uint16 :: { j elem domain(b.valuesMap) } 0 <= j && j < i ==>
 		j elem domain(b.valuesMap)
 	// injectivity requirement
-	invariant forall j1, j2 uint16 :: 0 <= j1 && j1 < j2 && j2 < i ==>
+	invariant forall j1, j2 uint16 :: { b.valuesMap[j1], b.valuesMap[j2] } 0 <= j1 && j1 < j2 && j2 < i ==>
 		b.valuesMap[j1] != b.valuesMap[j2]
-	invariant forall j uint16 :: i <= j && j < 256 ==>
-		acc(b.valuesMap[j]) && !(*b.valuesMap[j])
-	invariant forall j uint16 :: 0 <= j && j < i ==>
-		acc(b.valuesMap[j], 1/2)
-	invariant forall j uint16 :: 0 <= j && j < i ==>
+	invariant forall j uint16 :: { b.valuesMap[j] } i <= j && j < 256 ==>
+		acc(b.valuesMap[j], 3/4) && !(*b.valuesMap[j])
+	invariant forall j uint16 :: { b.valuesMap[j] } 0 <= j && j < i ==>
+		acc(b.valuesMap[j], 1/4)
+	invariant forall j uint16 :: { b.DoesNotContain(j) } 0 <= j && j < i ==>
 		b.DoesNotContain(j)
-	invariant forall j uint16 :: 0 <= j && j < i ==>
-		!b.fcontainshelper(j)
+	invariant b.fnotcontainshelperUpTo(i)
 	decreases 256 - i
 	for i = 0; i < 256; i +=1 {
-		fold b.DoesNotContain(i)
+	    fold b.DoesNotContain(i)
+		if b.fnotcontainshelperUpTo(i + 1) {} else {
+		    assert reveal b.fnotcontainshelperUpTo(i)
+		    assert reveal b.fnotcontainshelperUpTo(i + 1)
+            assert false
+		}
 	}
 	fold b.Inv()
 	return b