mode1 comments, mode3 cot

prompts/humaneval-nagini-few-shot-comments/add.txt

@@ -0,0 +1,6 @@
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+The program:
+{program}
+–
+The invariants:
+{checks}

prompts/humaneval-nagini-few-shot-comments/ask_for_fixed.txt

@@ -0,0 +1,6 @@
+The following errors occurred during verification:
+{error}
+
+Please fix the error by adding, removing or modifying the invariants and asserts and return the fixed program.
+Use extensive comments in the code, but don't explain anything outside of it.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-few-shot-comments/ask_for_fixed_had_errors.txt

@@ -0,0 +1,6 @@
+There are still some errors:
+{error}
+
+Could you please fix them?
+Use extensive comments in the code, but don't explain anything outside of it.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-few-shot-comments/produce.txt

@@ -0,0 +1,80 @@
+Given the following Python program, output Nagini invariants that should go into the `while` loop.
+Ensure that the invariants are as comprehensive as they can be.
+Even if you think some invariant is not totally necessary, better add it than not.
+Don't add any additional text comments, your response must contain only program with invariants.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+
+You remember the following aspects of Nagini syntax:
+
+1. Nagini DOES NOT SUPPORT some Python features as list comprehensions (k + 1 for k in range(5)), as double inequalities (a <= b <= c).
+Instead of double inequalities it's customary to use two separate inequalities (a <= b and b <= c).
+
+2. In Nagini method preconditions (Requires) and postconditions (Ensures) placed right after method signature, like here:
+"
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+    Ensures(Acc(list_pred(a)))
+    ...
+"
+
+3. Invariant are placed right after `while` statement and before the code of `while` body:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        s = s + numbers[i]
+"
+Invariants CANNOT be placed in any other position.
+You remember that each invariant (and each expression) should contain equal number of opening and closing brackets, so that it is valid.
+You should sustain balanced parentheses.
+
+4. Nagini requires special annotations for working with lists `Acc(list_pred(..))`. You can use these constructs only inside `Invariant`,
+anywhere else you should not use `Acc()` or `list_pred()`:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+"
+
+5. Nagini contains `Forall` and `Exists` constructs that can be used in invariants. First argument of Forall/Exists is typically a type (i.e `int`),
+second argument is a lambda. `Forall(type, lambda x : a)` denotes that assertion `a` is true for every element `x` of type `type`.
+
+6. In Nagini `Implies(e1, a2)` plays role of implication. `Implies(e1, a2)` denotes that assertion a2 holds if boolean expression e1 is true.
+You can use it inside invariants and asserts.
+
+Here are some examples of verified Python cycles with Nagini invariants:
+```
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(Acc(list_pred(result)))
+        Invariant(0 <= i and i <= len(numbers))
+        Invariant(len(result) == i)
+        Invariant(Forall(range(i), lambda i1: numbers[i1] <= result[i1]))
+        Invariant(Old(running_max) is None or ((Old(running_max) is not None) and (getVal(Old(running_max)) <= getVal(running_max))))
+        Invariant(Implies(len(result) > 0, running_max is not None))
+        Invariant(Implies(len(result) > 0, result[-1] == getVal(running_max)))
+        Invariant(Forall(range(i - 1), lambda i1: result[i1] <= result[i1 + 1]))
+
+        n = numbers[i]
+        if running_max is None or running_max < n:
+            running_max = n
+
+        result.append(running_max)
+        i += 1
+```
+
+```
+    while (d_0_i_) < (len((a))):
+        Invariant(Acc(list_pred(c)))
+        Invariant(Acc(list_pred(a)))
+        Invariant(len(c) == len(a) + 1)
+        Invariant(((0) <= (d_0_i_)) and ((d_0_i_) <= (len((a)))))
+        Invariant(Forall(int, lambda d_1_ii_:
+            Implies(((0) <= (d_1_ii_)) and ((d_1_ii_) < (d_0_i_)), ((c)[d_1_ii_]) == ((a)[d_1_ii_]))))
+        (c)[(d_0_i_)] = (a)[d_0_i_]
+        d_0_i_ = (d_0_i_) + (1)
+```
+
+The program:
+{program}
+

prompts/humaneval-nagini-few-shot-comments/rewrite.txt

@@ -0,0 +1,79 @@
+Rewrite the following Python program, adding correct Nagini invariants into `while` loops.
+Do not change the code, only add the invariants.
+Ensure that the invariants are as comprehensive as they can be.
+Even if you think some invariant is not totally necessary, better add it than not.
+Use extensive comments in the code, but don't explain anything outside of it.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+
+You remember the following aspects of Nagini syntax:
+
+1. Nagini DOES NOT SUPPORT some Python features as list comprehensions (k + 1 for k in range(5)), as double inequalities (a <= b <= c).
+Instead of double inequalities it's customary to use two separate inequalities (a <= b and b <= c).
+
+2. In Nagini method preconditions (Requires) and postconditions (Ensures) placed right after method signature, like here:
+"
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+    Ensures(Acc(list_pred(a)))
+    ...
+"
+
+3. Invariant are placed right after `while` statement and before the code of `while` body:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        s = s + numbers[i]
+"
+Invariants CANNOT be placed in any other position.
+You remember that each invariant (and each expression) should contain equal number of opening and closing brackets, so that it is valid.
+You should sustain balanced parentheses.
+
+4. Nagini requires special annotations for working with lists `Acc(list_pred(..))`. You can use these constructs only inside `Invariant`,
+anywhere else you should not use `Acc()` or `list_pred()`:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+"
+
+5. Nagini contains `Forall` and `Exists` constructs that can be used in invariants. First argument of Forall/Exists is typically a type (i.e `int`),
+second argument is a lambda. `Forall(type, lambda x : a)` denotes that assertion `a` is true for every element `x` of type `type`.
+
+6. In Nagini `Implies(e1, a2)` plays role of implication. `Implies(e1, a2)` denotes that assertion a2 holds if boolean expression e1 is true.
+You can use it inside invariants and asserts.
+
+You might need to work with accumulating functions, such as sum, so here's an example of how to do that:
+```
+from typing import cast, List, Dict, Set, Optional, Union
+from nagini_contracts.contracts import *
+
+@Pure
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+
+    if s == t:
+        return 0
+    else:
+        return (a)[t - 1] + (Sum(a, s, t - 1))
+
+def sum_loop(numbers: List[int]) -> int:
+    Requires(Acc(list_pred(numbers)))
+    Ensures(Acc(list_pred(numbers)))
+    Ensures(Result() == Sum(numbers, 0, len(numbers)))
+    s = int(0)
+    i = int(0)
+    while (i) < (len(numbers)):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        Invariant(Forall(int, lambda d_1_p_:
+            (Implies(0 <= d_1_p_ and d_1_p_ < len(numbers), Sum(numbers, 0, d_1_p_ + 1) == Sum(numbers, 0, d_1_p_) + numbers[d_1_p_]), [[Sum(numbers, 0, d_1_p_ + 1)]])))
+        Invariant(s == Sum(numbers, 0, i))
+        Assert(Sum(numbers, 0, i + 1) == Sum(numbers, 0, i) + numbers[i])
+        s = s + (numbers)[i]
+        i = i + 1
+    return s
+```
+The program:
+{program}

prompts/humaneval-nagini-few-shot-comments/sys.txt

@@ -0,0 +1,4 @@
+You are an expert in a Python verification framework Nagini.
+You will be given tasks dealing with Python programs including precise docstrings and specifications.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+Take into account that arrays inside the invariants are indexed by type `int`.

prompts/humaneval-nagini-few-shot-comments/timeout.txt

@@ -0,0 +1,3 @@
+The verifier timed out during the verification.
+This usually means that the provided invariants were too broad or were difficult to check.
+Could you please try to improve the invariants and try again?

prompts/humaneval-nagini-without-impls-cot-instruct/ask_for_fixed.txt

@@ -0,0 +1,7 @@
+The following errors occurred during verification:
+{error}
+
+Please fix the error by adding, removing or modifying the implementation, invariants or assertions and return the fixed program.
+You should not modify any helper functions (annotated with @Pure), remember they are here to help you with verification.
+Don't add any additional text comments, your response must contain only program with invariants.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-without-impls-cot-instruct/ask_for_fixed_had_errors.txt

@@ -0,0 +1,7 @@
+There are still some errors:
+{error}
+
+Please fix the error by adding, removing or modifying the implementation, invariants or assertions and return the fixed program.
+You should not modify any helper functions (annotated with @Pure), remember they are here to help you with verification.
+Don't add any additional text comments, your response must contain only program with invariants.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-without-impls-cot-instruct/helpers.txt

@@ -0,0 +1,2 @@
+Generally, you should use helper functions (marked with @Pure annotation) only in invariants, asserts and conditions (in `if` or `while` conditions), not in the plain code.
+But, the following helper functions you can use anywhere: {helpers}.

prompts/humaneval-nagini-without-impls-cot-instruct/invalid_helpers.txt

@@ -0,0 +1,9 @@
+We detected an improper usage of helper functions. Here is the list of helper functions used in a wrong way:
+{invalid_helpers}
+You should use helper functions only in invariants, asserts and conditions (in `if` or `while` conditions), not in the plain code.
+The following helper functions you can use anywhere: {helpers}.
+We replaced all improper usages with `invalid_call()` and got the following program:
+{program}
+You should rewrite this program without changing pre/postconditions and helper functions (denoted with @Pure).
+After rewriting your code should verify.
+Your code should not contain any `invalid_call()` invocations.

prompts/humaneval-nagini-without-impls-cot-instruct/rewrite/examples/001/answer.txt

@@ -0,0 +1,75 @@
+During the previous steps, we've found that the `sum_loop` function lacks implementation. We've divided its implementation into 3 parts:
+1. Initialization of variables of sum `s` and index `i`
+```
+s = int(0)
+i = int(0)
+```
+2. Going through the cycle and adding elements of list `numbers` to the sum `s`:
+```
+while (i) < (len(numbers)):
+    Invariant(Acc(list_pred(numbers)))
+    Invariant(0 <= i and i <= len(numbers))
+    Invariant(Forall(int, lambda d_1_p_:
+        (Implies(0 <= d_1_p_ and d_1_p_ < len(numbers), Sum(numbers, 0, d_1_p_ + 1) == Sum(numbers, 0, d_1_p_) + numbers[d_1_p_]), [[Sum(numbers, 0, d_1_p_ + 1)]])))
+    Invariant(s == Sum(numbers, 0, i))
+    Assert(Sum(numbers, 0, i + 1) == Sum(numbers, 0, i) + numbers[i])
+    s = s + (numbers)[i]
+    i = i + 1
+```
+3. Returning variable of sum `s`
+```
+return s
+```
+
+Let's combine them together:
+```
+def sum_loop(numbers: List[int]) -> int:
+    Requires(Acc(list_pred(numbers)))
+    Ensures(Acc(list_pred(numbers)))
+    Ensures(Result() == Sum(numbers, 0, len(numbers)))
+    s = int(0)
+    i = int(0)
+    while (i) < (len(numbers)):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        Invariant(Forall(int, lambda d_1_p_:
+            (Implies(0 <= d_1_p_ and d_1_p_ < len(numbers), Sum(numbers, 0, d_1_p_ + 1) == Sum(numbers, 0, d_1_p_) + numbers[d_1_p_]), [[Sum(numbers, 0, d_1_p_ + 1)]])))
+        Invariant(s == Sum(numbers, 0, i))
+        Assert(Sum(numbers, 0, i + 1) == Sum(numbers, 0, i) + numbers[i])
+        s = s + (numbers)[i]
+        i = i + 1
+    return s
+```
+
+Other than that, we didn't find any other functions with missed implementations. Therefore, the resulting program is (notice the lack of backticks):
+<answer>
+from typing import cast, List, Dict, Set, Optional, Union
+from nagini_contracts.contracts import *
+
+@Pure
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+
+    if s == t:
+        return 0
+    else:
+        return (a)[t - 1] + (Sum(a, s, t - 1))
+
+def sum_loop(numbers: List[int]) -> int:
+    Requires(Acc(list_pred(numbers)))
+    Ensures(Acc(list_pred(numbers)))
+    Ensures(Result() == Sum(numbers, 0, len(numbers)))
+    s = int(0)
+    i = int(0)
+    while (i) < (len(numbers)):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        Invariant(Forall(int, lambda d_1_p_:
+            (Implies(0 <= d_1_p_ and d_1_p_ < len(numbers), Sum(numbers, 0, d_1_p_ + 1) == Sum(numbers, 0, d_1_p_) + numbers[d_1_p_]), [[Sum(numbers, 0, d_1_p_ + 1)]])))
+        Invariant(s == Sum(numbers, 0, i))
+        Assert(Sum(numbers, 0, i + 1) == Sum(numbers, 0, i) + numbers[i])
+        s = s + (numbers)[i]
+        i = i + 1
+    return s
+</answer>

prompts/humaneval-nagini-without-impls-cot-instruct/rewrite/examples/001/question.txt

@@ -0,0 +1,21 @@
+It's time to rewrite the program to contain the implementations for functions. Work on the following program and go step by step through the reasoning process. After that, output the rewritten program in the `<answer>` tag without backticks.
+
+```
+from typing import cast, List, Dict, Set, Optional, Union
+from nagini_contracts.contracts import *
+
+@Pure
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+
+    if s == t:
+        return 0
+    else:
+        return (a)[t - 1] + (Sum(a, s, t - 1))
+
+def sum_loop(numbers: List[int]) -> int:
+    Requires(Acc(list_pred(numbers)))
+    Ensures(Acc(list_pred(numbers)))
+    Ensures(Result() == Sum(numbers, 0, len(numbers)))
+```

prompts/humaneval-nagini-without-impls-cot-instruct/rewrite/question.txt

@@ -0,0 +1,3 @@
+It's time to rewrite the program to contain the implementations for functions. Work on the following program and go step by step through the reasoning process. After that, output the rewritten program in the `<answer>` tag without backticks.
+
+{program}

prompts/humaneval-nagini-without-impls-cot-instruct/steps/001/examples/001/answer.txt

@@ -0,0 +1 @@
+understood

prompts/humaneval-nagini-without-impls-cot-instruct/steps/001/examples/001/question.txt

@@ -0,0 +1,40 @@
+You are an expert in Nagini, a verification framework in Python.
+You remember the following aspects of Nagini syntax:
+
+1. Nagini DOES NOT SUPPORT some Python features as list comprehensions (k + 1 for k in range(5)), as double inequalities (a <= b <= c).
+Instead of double inequalities it's customary to use two separate inequalities (a <= b and b <= c).
+
+2. In Nagini method preconditions (Requires) and postconditions (Ensures) placed right after method signature, like here:
+"
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+    Ensures(Acc(list_pred(a)))
+    ...
+"
+
+3. Invariant are placed right after `while` statement and before the code of `while` body:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        s = s + numbers[i]
+"
+Invariants CANNOT be placed in any other position.
+You remember that each invariant (and each expression) should contain equal number of opening and closing brackets, so that it is valid.
+You should sustain balanced parentheses.
+
+4. Nagini requires special annotations for working with lists `Acc(list_pred(..))`. You can use these constructs only inside `Invariant`,
+anywhere else you should not use `Acc()` or `list_pred()`:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+"
+
+5. Nagini contains `Forall` and `Exists` constructs that can be used in invariants. First argument of Forall/Exists is typically a type (i.e `int`),
+second argument is a lambda. `Forall(type, lambda x : a)` denotes that assertion `a` is true for every element `x` of type `type`.
+
+6. In Nagini `Implies(e1, a2)` plays role of implication. `Implies(e1, a2)` denotes that assertion a2 holds if boolean expression e1 is true.
+You can use it inside invariants and asserts.
+
+Respond with 'understood' to this message. Remember this knowledge to solve the task that will be given further