Adding 92, 94, 97 #35

parno · 2025-09-30T14:32:31Z

This is a really weird keyboard-mash of a function name. I realize it's the one the prompt chose, but I think it would help to add a comment to that effect, so future readers aren't puzzled by it.

-Original file line number
+Diff line change
@@ Expand Up / @@ -9,7 +9,42 @@ use vstd::prelude::*; @@
     verus! {
-    // TODO: Put your solution (the specification, implementation, and proof) to the task here
+    spec fn any_int_spec(x: int, y: int, z: int) -> bool {
+        (x == y + z) || (y == x + z) || (z == x + y)
+    }
+    fn any_int(x: i32, y: i32, z: i32) -> (result: bool)
+        ensures
+            result <==> any_int_spec(x as int, y as int, z as int),
+    {
+        // explicit range checks allow us to drop range requires statements
+        // on our signature
+        let check1 = if y > 0 && z > 0 && y > i32::MAX - z {
+            false
+        } else if y < 0 && z < 0 && y < i32::MIN - z {
+            false
+        } else {
+            y + z == x
+        };
+        let check2 = if x > 0 && z > 0 && x > i32::MAX - z {
+            false
+        } else if x < 0 && z < 0 && x < i32::MIN - z {
+            false
+        } else {
+            x + z == y
+        };
+        let check3 = if x > 0 && y > 0 && x > i32::MAX - y {
+            false
+        } else if x < 0 && y < 0 && x < i32::MIN - y {
+            false
+        } else {
+            x + y == z
+        };
+        check1 || check2 || check3
+    }
     } // verus!
     fn main() {}
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -9,7 +9,141 @@ use vstd::prelude::*; @@
     verus! {
-    // TODO: Put your solution (the specification, implementation, and proof) to the task here
+    pub open spec fn is_prime_spec(n: nat) -> bool {
+        (n > 1) && forall|i| 1 < i < n ==> #[trigger] (n % i) != 0
+    }
+    pub closed spec fn is_prime_so_far(n: nat, k: nat) -> bool
+        recommends
+            n >= k > 1,
+    {
+        forall|i| 1 < i < k ==> #[trigger] (n % i) != 0
+    }
+    fn is_prime(n: u32) -> (res: bool)
+        ensures
+            res == is_prime_spec(n as nat),
+    {
+        if n < 2 {
+            return false;
+        }
+        let mut k = 2;
+        let mut res = true;
+        while (k < n)
+            invariant
+<= k <= n,
+                res == is_prime_so_far(n as nat, k as nat),
+            decreases n - k,
+        {
+            assert((is_prime_so_far(n as nat, k as nat) && (n as nat) % (k as nat) != 0)
+                == is_prime_so_far(n as nat, (k + 1) as nat));
+            res = res && n % k != 0;
+            k = k + 1;
+        }
+        return res;
+    }
+    pub open spec fn spec_sum_digits(n: nat) -> nat
+        decreases n,
+    {
+        if n < 10 {
+            n
+        } else {
+            (n % 10) + spec_sum_digits(n / 10)
+        }
+    }
+    pub proof fn sum_digits_decreases(x: nat)
+        requires
+            x >= 10,
+        ensures
+            spec_sum_digits(x) <= x,
+        decreases x,
+    {
+        let sub_x = x / 10;
+        let inc_x = x % 10;
+        if sub_x >= 10 {
+            sum_digits_decreases(sub_x);
+            assert(inc_x + sub_x <= x + 10);
+        } else {
+            assert(inc_x + spec_sum_digits(sub_x) <= sub_x + 10);
+        }
+    }
+    fn sum_digits(n: u32) -> (count: u32)
+        ensures
+            count == spec_sum_digits(n as nat),
+        decreases n,
+    {
+        if n < 10 {
+            n
+        } else {
+            assert(spec_sum_digits((n as nat)) <= n) by { sum_digits_decreases(n as nat) };
+            (n % 10) + sum_digits(n / 10)
+        }
+    }
+    pub open spec fn spec_find_largest_prime_so_far(s: Seq<nat>, i: nat) -> nat
+        recommends
+<= i <= s.len(),
+        decreases i,
+    {
+        if i <= 0 {
+        } else {
+            let first_i = s.take(i as int);  // first i numbers
+            // largest of the first i-i numbers in the list
+            let largest_in_front = spec_find_largest_prime_so_far(s, (i - 1) as nat);
+            // is the i'th number prime and bigger than the largest of the first i-1 numbers?
+            if is_prime_spec(first_i.last()) && first_i.last() > largest_in_front {
+                first_i.last()
+            } else {
+                largest_in_front
+            }
+        }
+    }
+    pub open spec fn spec_find_largest_prime(s: Seq<nat>) -> nat {
+        spec_find_largest_prime_so_far(s, s.len())
+    }
+    fn find_largest_prime(lst: Vec<u32>) -> (ret: u32)
+        ensures
+            ret == spec_find_largest_prime([email protected]_values(|val: u32| val as nat)),
+    {
+        let mut largest_prime = 0;
+        for i in 0..lst.len()
+            invariant
+                largest_prime == 0 || is_prime_spec(largest_prime as nat),
+                largest_prime == spec_find_largest_prime_so_far(
+                    [email protected]_values(|val: u32| val as nat),
+                    i as nat,
+                ),
+        {
+            let num = lst[i];
+            if is_prime(num) && num > largest_prime {
+                largest_prime = num;
+            }
+        }
+        largest_prime
+    }
+    // note: "skjkasdkd" is the specified function name
+    fn skjkasdkd(lst: Vec<u32>) -> (ret: u32)
+        ensures
+            ret == spec_sum_digits(
+                spec_find_largest_prime([email protected]_values(|val: u32| val as nat)) as nat,
+            ),
+    {
+        let largest_prime = find_largest_prime(lst);
+        let total = sum_digits(largest_prime);
+        total
+    }
     } // verus!
     fn main() {}
@@ Expand Down Expand Up / @@ -44,6 +178,7 @@ skjkasdkd @@
     /*
     ### CANONICAL SOLUTION
+    def skjkasdkd(lst):
         def isPrime(n):
             for i in range(2,int(n**0.5)+1):
                 if n%i==0:
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -5,11 +5,50 @@ HumanEval/97 @@
     /*
     ### VERUS BEGIN
     */
+    use vstd::arithmetic::div_mod::*;
+    use vstd::math::abs as vabs;
     use vstd::prelude::*;
+    use vstd::arithmetic::mul::lemma_mul_upper_bound;
     verus! {
-    // TODO: Put your solution (the specification, implementation, and proof) to the task here
+    pub proof fn lemma_mul_ub_mod_abs(x: int, y: int, a: int, b: int)
+        requires
+            a > 0,
+            b > 0,
+        ensures
+<= (vabs(x) % (a as nat)) * (vabs(y) % (b as nat)) <= (a * b),
+    {
+        lemma_mul_upper_bound((vabs(x) % (a as nat)) as int, a, (vabs(y) % (b as nat)) as int, b);
+    }
+    fn unit_digit(a: i32) -> (ret: i32)
+        ensures
+            ret as int == vabs(a as int) % 10,
+    {
+        let result = if a < 0 {
+            -(a % 10)
+        } else {
+            a % 10
+        };
+        result
+    }
+    pub open spec fn multiply_spec(a: int, b: int) -> nat {
+        (vabs(a) % 10) * (vabs(b) % 10)
+    }
+    fn multiply(a: i32, b: i32) -> (ret: i32)
+        ensures
+            ret as int == multiply_spec(a as int, b as int),
+    {
+        assert(0 <= (vabs(a as int) % 10) * (vabs(b as int) % 10) <= 100) by {
+            lemma_mul_ub_mod_abs(a as int, b as int, 10, 10)
+        };
+        unit_digit(a) * unit_digit(b)
+    }
     } // verus!
     fn main() {}
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adding 92, 94, 97 #35

Uh oh!

Diff view

Diff view

There are no files selected for viewing

parno Sep 30, 2025

Uh oh!

JakeGinesin Sep 30, 2025

Uh oh!

Adding 92, 94, 97 #35

Uh oh!

Adding 92, 94, 97 #35

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

parno Sep 30, 2025

Choose a reason for hiding this comment

Uh oh!

JakeGinesin Sep 30, 2025

Choose a reason for hiding this comment

Uh oh!