Merge branch 'secure-foundations:main' into main

.github/workflows/verus.yml

@@ -0,0 +1,52 @@
+name: verus
+
+on: [pull_request, workflow_dispatch]
+
+jobs:
+  verus:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: Install toolchain dependencies
+        shell: bash
+        run: |
+          curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --profile minimal --default-toolchain none -y
+          echo "${CARGO_HOME:-$HOME/.cargo}/bin" >> $GITHUB_PATH
+
+      - name: Install Rust toolchain
+        run: |
+          rustup update --no-self-update stable
+          rustup install 1.79.0-x86_64-unknown-linux-gnu
+
+      - name: Get the URL for the latest Verus release
+        id: verus-release-info
+        run: |
+          jq --version
+          echo "VERUS_URL=$(curl -s https://api.github.com/repos/verus-lang/verus/releases | jq -r '.[].assets[].browser_download_url' | grep x86-linux -)" >> $GITHUB_OUTPUT
+
+      - name: Download the latest Verus release
+        run: |
+          curl --proto '=https' --tlsv1.2 -LsSf ${{ steps.verus-release-info.outputs.VERUS_URL }} -o verus.zip; unzip verus.zip
+
+      - name: run Verus
+        working-directory: ./tasks
+        run: |
+          # Run `verus` on each file, collecting failures if any
+          ANYFAILED=""
+          for i in *.rs; do
+            echo -n "[verus] $i: "
+            if ../verus-x86-linux/verus "$i" >/dev/null 2>/dev/null; then
+              echo "success"
+            else 
+              echo "failed"
+              # Re-run `verus` on any failure just to display the actual output
+              ../verus-x86-linux/verus "$i" || true
+              ANYFAILED="$ANYFAILED $i"
+            fi
+          done
+          if [ -n "$ANYFAILED" ]; then
+            echo "Failed:$ANYFAILED"
+            exit 1
+          fi

CONTRIBUTORS.md

@@ -0,0 +1,10 @@
+- Alex Bai
+- Jay Bosamiya
+- Edwin Fernando
+- Md Rakib Hossain
+- Jay Lorch
+- Shan Lu
+- Natalie Neamtu
+- Bryan Parno
+- Amar Shah
+- Elanor Tang

README.md

@@ -1,4 +1,4 @@
-# VerusBench: Hand-Written Examples of Verified Verus Code
+# HumanEval-Verus: Hand-Written Examples of Verified Verus Code Derived From HumanEval
 
 This is intended to be a collection of examples translated from the [HumanEval]
 benchmark into Rust.  The goal is that each example will include a textual
@@ -16,8 +16,8 @@ folder](./tasks/gpt), we have (unverified) Rust code generated by ChatGPT.  Of
 course, the code may be completely incorrect, so feel free to ignore it and
 start your code from scratch.
 
-Contributors will be acknowledged in any publications that may be published
-about this benchmark.
+[Contributors](./CONTRIBUTORS.md) should be acknowledged in any publications
+that may be published about this benchmark.
 
 [HumanEval]: https://github.com/openai/human-eval
 [Verus]: https://github.com/verus-lang/verus

tasks/human_eval_008.rs

@@ -38,7 +38,14 @@ fn sum_product(numbers: Vec<u32>) -> (result: (u64, Option<u32>))
         numbers.len() < u32::MAX,
     ensures
         result.0 == sum(numbers@),
-        result.1 matches Some(v) ==> v == product(numbers@),
+        match result.1 {
+            None =>   // Computing the product overflowed at some point
+            exists|i|
+                #![auto]
+                0 <= i < numbers.len() && product(numbers@.subrange(0, i)) * numbers[i] as int
+                    > u32::MAX,
+            Some(v) => v == product(numbers@),
+        },
 {
     let mut sum_value: u64 = 0;
     let mut prod_value: Option<u32> = Some(1);
@@ -47,6 +54,14 @@ fn sum_product(numbers: Vec<u32>) -> (result: (u64, Option<u32>))
             numbers.len() < u32::MAX,
             sum_value == sum(numbers@.take(index as int)),
             prod_value matches Some(v) ==> v == product(numbers@.take(index as int)),
+            match prod_value {
+                None =>   // Computing the product overflowed at some point
+                exists|i|
+                    #![auto]
+                    0 <= i < index && product(numbers@.subrange(0, i)) * numbers[i] as int
+                        > u32::MAX,
+                Some(v) => v == product(numbers@.take(index as int)),
+            },
             index <= numbers.len(),
             index >= 0,
     {

tasks/human_eval_015.rs

@@ -9,10 +9,169 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+// specification
+pub closed spec fn single_digit_number_to_char(n: nat) -> char {
+    if n == 0 {
+        '0'
+    } else if n == 1 {
+        '1'
+    } else if n == 2 {
+        '2'
+    } else if n == 3 {
+        '3'
+    } else if n == 4 {
+        '4'
+    } else if n == 5 {
+        '5'
+    } else if n == 6 {
+        '6'
+    } else if n == 7 {
+        '7'
+    } else if n == 8 {
+        '8'
+    } else {
+        '9'
+    }
+}
+
+pub closed spec fn number_to_char(n: nat) -> Seq<char>
+    decreases n,
+{
+    if (n == 0) {
+        seq![]
+    } else {
+        number_to_char(n / 10).add(seq![single_digit_number_to_char(n % 10)])
+    }
+}
+
+pub open spec fn string_sequence(n: nat) -> Seq<char>
+    decreases n,
+{
+    if n == 0 {
+        seq!['0']
+    } else {
+        string_sequence((n - 1) as nat).add(seq![' '].add(number_to_char(n)))
+    }
+}
+
+proof fn sanity_check() {
+    assert(string_sequence(1) == seq!['0', ' ', '1']) by (compute);
+    assert(string_sequence(3) == seq!['0', ' ', '1', ' ', '2', ' ', '3']) by (compute);
+    assert(string_sequence(12) == seq![
+        '0',
+        ' ',
+        '1',
+        ' ',
+        '2',
+        ' ',
+        '3',
+        ' ',
+        '4',
+        ' ',
+        '5',
+        ' ',
+        '6',
+        ' ',
+        '7',
+        ' ',
+        '8',
+        ' ',
+        '9',
+        ' ',
+        '1',
+        '0',
+        ' ',
+        '1',
+        '1',
+        ' ',
+        '1',
+        '2',
+    ]) by (compute);
+    assert((number_to_char(158) == seq!['1', '5', '8'])) by (compute);
+}
+
+// implementation
+fn single_digit_number_to_char_impl(n: u8) -> (output: char)
+    requires
+        0 <= n <= 9,
+    ensures
+        single_digit_number_to_char(n as nat) == output,
+{
+    if n == 0 {
+        '0'
+    } else if n == 1 {
+        '1'
+    } else if n == 2 {
+        '2'
+    } else if n == 3 {
+        '3'
+    } else if n == 4 {
+        '4'
+    } else if n == 5 {
+        '5'
+    } else if n == 6 {
+        '6'
+    } else if n == 7 {
+        '7'
+    } else if n == 8 {
+        '8'
+    } else {
+        '9'
+    }
+}
+
+pub fn number_to_char_impl(n: u8) -> (char_vec: Vec<char>)
+    ensures
+        char_vec@ == number_to_char(n as nat),
+{
+    let mut i = n;
+    let mut output = vec![];
+
+    while (i > 0)
+        invariant
+            number_to_char(n as nat) == number_to_char(i as nat).add(output@),
+    {
+        let m = i % 10;
+        let current = single_digit_number_to_char_impl(m);
+        output.insert(0, current);
+        i = i / 10;
+
+        assert(number_to_char(n as nat) == number_to_char(i as nat).add(output@));
+    }
+    return output;
+}
+
+fn string_sequence_impl(n: u8) -> (string_seq: Vec<char>)
+    ensures
+        string_seq@ == string_sequence(n as nat),
+{
+    let mut i = n;
+    let mut output = vec![];
+    while (i > 0)
+        invariant
+            n >= i >= 0,
+            string_sequence(n as nat) == string_sequence(i as nat) + output@,
+        decreases i,
+    {
+        let mut next = number_to_char_impl(i);
+        next.append(&mut output);
+        output = next;
+        output.insert(0, ' ');
+        i = i - 1;
+
+        assert(string_sequence((n) as nat) == string_sequence((i) as nat) + output@);
+    }
+    output.insert(0, '0');
+    assert(string_sequence(n as nat) == output@);
+    return output;
+}
 
 } // verus!
-fn main() {}
+fn main() {
+    print!("{:?}", string_sequence_impl(0));
+    print!("{:?}", string_sequence_impl(5));
+    print!("{:?}", string_sequence_impl(20));
+}
 
 /*
 ### VERUS END