Skip to content

Commit

Permalink
Merge branch 'main' of github.com:edwin1729/human-eval-verus
Browse files Browse the repository at this point in the history
  • Loading branch information
edwin1729 committed Dec 23, 2024
2 parents f9c2fad + 1b03c0f commit 25afa53
Show file tree
Hide file tree
Showing 24 changed files with 2,040 additions and 44 deletions.
52 changes: 52 additions & 0 deletions .github/workflows/verus.yml
Original file line number Diff line number Diff line change
@@ -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
10 changes: 10 additions & 0 deletions CONTRIBUTORS.md
Original file line number Diff line number Diff line change
@@ -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
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
17 changes: 16 additions & 1 deletion tasks/human_eval_008.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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,
{
Expand Down
163 changes: 161 additions & 2 deletions tasks/human_eval_015.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading

0 comments on commit 25afa53

Please sign in to comment.