Finished task 139 (#22)

tasks/human_eval_025.rs

@@ -251,7 +251,7 @@ proof fn lemma_drop_last_map_commute(seq: Seq<u8>)
 
 proof fn lemma_fold_right_equivalent_for_nat_u8(factorization: Seq<u8>)
     requires
-        factorization.fold_right(|x, acc: u8| (acc * x) as u8, 1u8) <= 255 as u8,
+        factorization.fold_right(|x, acc: u8| (acc * x) as u8, 1u8) <= u8::MAX as u8,
         forall|i: int| 0 <= i < factorization.len() ==> factorization[i] > 0,
     ensures
         factorization.fold_right(|x, acc: nat| (acc * x) as nat, 1nat) == factorization.map(
@@ -301,7 +301,7 @@ proof fn lemma_fold_right_equivalent_for_nat_u8(factorization: Seq<u8>)
 
 pub fn factorize(n: u8) -> (factorization: Vec<u8>)
     requires
-        1 <= n <= 255,
+        1 <= n <= u8::MAX,
     ensures
         is_prime_factorization(n as nat, [email protected](|_idx, j: u8| j as nat)),
 {
@@ -312,7 +312,7 @@ pub fn factorize(n: u8) -> (factorization: Vec<u8>)
     while (m <= n as u16)
         invariant
             1 < m < n + 2,
-            n <= 255,
+            n <= u8::MAX,
             0 < k <= n,
             forall|j: u8| 1 < j < m ==> #[trigger] (k % j) != 0,
             [email protected]_right(|x: u8, acc: nat| (acc * x) as nat, 1nat) == n as nat / (

tasks/human_eval_139.rs

@@ -5,14 +5,141 @@ HumanEval/139
 /*
 ### VERUS BEGIN
 */
+use vstd::arithmetic::mul::*;
 use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+// specification
+pub closed spec fn factorial(n: nat) -> nat
+    decreases n,
+{
+    if n <= 1 {
+        1
+    } else {
+        n * factorial((n - 1) as nat)
+    }
+}
+
+pub closed spec fn brazilian_factorial(n: nat) -> nat
+    decreases n,
+{
+    if n <= 1 {
+        factorial(1)
+    } else {
+        factorial(n) * brazilian_factorial((n - 1) as nat)
+    }
+}
+
+proof fn lemma_factorial_positive(n: nat)
+    ensures
+        factorial(n) >= 1,
+    decreases n,
+{
+    if (n == 0) {
+    } else {
+        lemma_factorial_positive((n - 1) as nat);
+        assert(factorial(n) >= 1) by {
+            broadcast use lemma_mul_strictly_positive;
+
+        };
+    }
+}
+
+proof fn lemma_brazilian_factorial_positive(n: nat)
+    ensures
+        brazilian_factorial(n) >= 1,
+    decreases n,
+{
+    if (n == 0) {
+    } else {
+        lemma_factorial_positive((n) as nat);
+        lemma_brazilian_factorial_positive((n - 1) as nat);
+        assert(brazilian_factorial(n) >= 1) by {
+            lemma_mul_strictly_positive(
+                factorial(n) as int,
+                brazilian_factorial((n - 1) as nat) as int,
+            )
+        };
+    }
+}
+
+proof fn lemma_brazilian_fib_monotonic(i: nat, j: nat)
+    requires
+        0 <= i <= j,
+    ensures
+        brazilian_factorial(i) <= brazilian_factorial(j),
+    decreases j - i,
+{
+    if (i == j) {
+    } else if (j == i + 1) {
+        assert(factorial(j) >= 1) by { lemma_factorial_positive(j) };
+        assert(brazilian_factorial(j) >= brazilian_factorial(i)) by {
+            broadcast use lemma_mul_increases;
+
+        };
+    } else {
+        lemma_brazilian_fib_monotonic(i, (j - 1) as nat);
+        lemma_brazilian_fib_monotonic((j - 1) as nat, j);
+    }
+}
+
+pub fn brazilian_factorial_impl(n: u64) -> (ret: Option<u64>)
+    ensures
+        match ret {
+            None => brazilian_factorial(n as nat) > u64::MAX,
+            Some(bf) => bf == brazilian_factorial(n as nat),
+        },
+{
+    if n >= 9 {
+        assert(brazilian_factorial(9nat) > u64::MAX) by (compute_only);
+        assert(brazilian_factorial(n as nat) >= brazilian_factorial(9nat)) by {
+            lemma_brazilian_fib_monotonic(9nat, n as nat)
+        };
+        return None;
+    }
+    let mut start = 1u64;
+    let mut end = n + 1u64;
+    let mut fact_i = 1u64;
+    let mut special_fact = 1u64;
+
+    while start < end
+        invariant
+            brazilian_factorial((start - 1) as nat) == special_fact,
+            factorial((start - 1) as nat) == fact_i,
+            1 <= start <= end < 10,
+        decreases (end - start),
+    {
+        assert(brazilian_factorial(start as nat) <= brazilian_factorial(8nat)) by {
+            lemma_brazilian_fib_monotonic(start as nat, 8nat)
+        };
+        assert(brazilian_factorial(8nat) < u64::MAX) by (compute_only);
+
+        assert(brazilian_factorial((start - 1) as nat) >= 1) by {
+            lemma_brazilian_factorial_positive((start - 1) as nat)
+        };
+        assert(factorial(start as nat) <= brazilian_factorial(start as nat)) by {
+            broadcast use lemma_mul_ordering;
+
+        };
+
+        fact_i = start * fact_i;
+
+        special_fact = fact_i * special_fact;
+
+        start = start + 1;
+    }
+    return Some(special_fact);
+
+}
 
 } // verus!
-fn main() {}
+fn main() {
+    println!("{:?}", brazilian_factorial_impl(4));
+    // > 288
+    println!("{:?}", brazilian_factorial_impl(6));
+    // > 24883200
+}
 
 /*
 ### VERUS END