started 6th mode

prompts/humaneval-nagini-without-conditions-few-shot/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 implementation, invariants or assertions and return the fixed program.
+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-conditions-few-shot/ask_for_fixed_had_errors.txt

@@ -0,0 +1,6 @@
+There are still some errors:
+{error}
+
+Could you please fix them?
+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-conditions-few-shot/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 helper functions (denoted with @Pure).
+After rewriting your code should verify.
+Your code should not contain any `invalid_call()` invocations.

prompts/humaneval-nagini-without-conditions-few-shot/rewrite.txt

@@ -0,0 +1,80 @@
+Rewrite the following Nagini code. It does not contain any preconditions, postconditions, invariants, assertions or helper functions (annotated with @Pure). Rewrite the program to add those in a way that makes it verify.
+Do not change the code, only add invariants, assertions and conditions.
+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.
+
+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-without-conditions-few-shot/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 annotations.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+You respond only with code blocks.

prompts/humaneval-nagini-without-conditions-few-shot/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-helpers-few-shot/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 implementation, invariants or assertions and return the fixed program.
+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-helpers-few-shot/ask_for_fixed_had_errors.txt

@@ -0,0 +1,6 @@
+There are still some errors:
+{error}
+
+Could you please fix them?
+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-few-shot-text-description/helpers.txt → prompts/humaneval-nagini-without-helpers-few-shot/helpers.txt

@@ -1,3 +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}.
-Do not change helper functions.

prompts/humaneval-nagini-without-helpers-few-shot/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, so that pre/postconditions will correspond text description.
+After rewriting your code should verify.
+Your code should not contain any `invalid_call()` invocations.

prompts/humaneval-nagini-without-helpers-few-shot/rewrite.txt

@@ -0,0 +1,86 @@
+The following Nagini code contains no implementations of functions, pre/postconditions, invariants and assertions.
+Using text description you should add implementations and relevant pre/postconditions. Prefer loops to recursion. You should also add invariants/assertions and helper functions (annotated with @Pure).
+Use helper functions only in invariants, assertions and conditions (in `if` or `while` conditions). Don't use helpers in the plain code.
+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.
+
+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
+```
+
+To help you, here's a text description given to a person who wrote this program:
+
+{text_description}
+
+The program:
+{program}

prompts/humaneval-nagini-without-helpers-few-shot/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 annotations.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+You respond only with code blocks.

prompts/humaneval-nagini-without-helpers-few-shot/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?

scripts/rename_vars.py

@@ -0,0 +1,40 @@
+# %%
+import pathlib
+
+import libcst as cst
+
+# %%
+import re
+
+# %%
+class RenameVariableTransformer(cst.CSTTransformer):
+    def __init__(self):
+        self.pattern = re.compile(r"d_\d+_(.+)_")
+
+    def leave_Name(self, original_node: cst.Name, updated_node: cst.Name) -> cst.Name:
+        match = self.pattern.match(original_node.value)
+        if match:
+            new_name = match.group(1)
+            return updated_node.with_changes(value=new_name)
+        return updated_node
+
+
+bench = pathlib.Path("benches/HumanEval-Nagini/Bench")
+for file in list(bench.glob("*.py")):
+    with open(file, "r") as f:
+        code = f.read()
+    module = cst.parse_module(code)
+
+    # Transform the CST
+    transformer = RenameVariableTransformer()
+    transformed_module = module.visit(transformer)
+
+    # Convert the transformed CST back to source code
+    transformed_code = transformed_module.code
+
+    # Print the transformed code
+    with open(file, "w") as f:
+        f.write(transformed_code)
+        print(f.name)
+        print(file, transformed_code)
+        f.close()

verified_cogen/args.py

@@ -27,6 +27,7 @@ class ProgramArgs:
     remove_implementations: bool
     include_text_descriptions: bool
     manual_rewriters: List[str]
+    remove_pure: bool
 
     @no_type_check
     def __init__(self, args):
@@ -51,6 +52,7 @@ def __init__(self, args):
         self.remove_implementations = args.remove_implementations
         self.include_text_descriptions = args.include_text_descriptions
         self.manual_rewriters = args.manual_rewriters
+        self.remove_pure = args.remove_pure
 
 
 def get_default_parser():
@@ -137,6 +139,12 @@ def get_default_parser():
         default=[],
         nargs="+",
     )
+    parser.add_argument(
+        "--remove-pure",
+        help="Remove pure functions from the program",
+        default=False,
+        action="store_true",
+    )
     return parser
 
 

verified_cogen/experiments/incremental_run.py

@@ -43,6 +43,8 @@ def main():
         all_removed += [AnnotationType.PRE_CONDITIONS, AnnotationType.POST_CONDITIONS]
     if args.remove_implementations:
         all_removed += [AnnotationType.IMPLS]
+    if args.remove_pure:
+        all_removed += [AnnotationType.PURE]
 
     register_basic_languages(with_removed=all_removed)
 
@@ -78,6 +80,7 @@ def main():
         log_tries=log_tries,
         include_text_descriptions=args.include_text_descriptions,
         remove_implementations=args.remove_implementations,
+        remove_helpers=args.remove_pure,
     )
     for file in files:
         llm = LLM(

verified_cogen/main.py

@@ -197,6 +197,7 @@ def main():
         log_tries=log_tries,
         include_text_descriptions=args.include_text_descriptions,
         remove_implementations=args.remove_implementations,
+        remove_helpers=args.remove_pure,
     )
     if args.dir is not None:
         files = sorted(list(pathlib.Path(args.dir).glob(ext_glob(args.filter_by_ext))))

verified_cogen/runners/__init__.py

@@ -15,16 +15,19 @@ class RunnerConfig:
     log_tries: Optional[pathlib.Path] = None
     include_text_descriptions: bool = False
     remove_implementations: bool = False
+    remove_helpers: bool = False
 
     def __init__(
         self,
         log_tries: Optional[pathlib.Path] = None,
         include_text_descriptions: bool = False,
         remove_implementations: bool = False,
+        remove_helpers: bool = False,
     ):
         self.log_tries = log_tries
         self.include_text_descriptions = include_text_descriptions
         self.remove_implementations = remove_implementations
+        self.remove_helpers = remove_helpers
 
 
 class Runner: