From 57d2c71115210caa547e5a9f150f6ba8138e8738 Mon Sep 17 00:00:00 2001
From: AlexShefY <alex.shefer.31@gmail.com>
Date: Mon, 21 Oct 2024 12:57:45 +0200
Subject: [PATCH] changed prompt

---
 .../steps/001/examples/001/answer.txt         |  1 +
 .../steps/001/examples/001/question.txt       | 37 +++++++++++++++++++
 .../steps/001/question.txt                    |  2 +-
 verified_cogen/runners/languages/nagini.py    |  8 ++--
 4 files changed, 44 insertions(+), 4 deletions(-)
 create mode 100644 prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/answer.txt
 create mode 100644 prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/question.txt

diff --git a/prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/answer.txt b/prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/answer.txt
new file mode 100644
index 0000000..863c07d
--- /dev/null
+++ b/prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/answer.txt
@@ -0,0 +1 @@
+understood
\ No newline at end of file
diff --git a/prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/question.txt b/prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/question.txt
new file mode 100644
index 0000000..389b628
--- /dev/null
+++ b/prompts/humaneval-nagini-cot-instruct/steps/001/examples/001/question.txt
@@ -0,0 +1,37 @@
+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`.
+
+Respond with 'understood' to this message. Remember this knowledge to solve the task that will be given further
\ No newline at end of file
diff --git a/prompts/humaneval-nagini-cot-instruct/steps/001/question.txt b/prompts/humaneval-nagini-cot-instruct/steps/001/question.txt
index bf18ead..389b628 100644
--- a/prompts/humaneval-nagini-cot-instruct/steps/001/question.txt
+++ b/prompts/humaneval-nagini-cot-instruct/steps/001/question.txt
@@ -34,4 +34,4 @@ anywhere else you should not use `Acc()` or `list_pred()`:
 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`.
 
-Don't respond to this code. Remember this knowledge to solve the task that will be given further
\ No newline at end of file
+Respond with 'understood' to this message. Remember this knowledge to solve the task that will be given further
\ No newline at end of file
diff --git a/verified_cogen/runners/languages/nagini.py b/verified_cogen/runners/languages/nagini.py
index cae8b22..f1f6df0 100644
--- a/verified_cogen/runners/languages/nagini.py
+++ b/verified_cogen/runners/languages/nagini.py
@@ -36,6 +36,8 @@ def __init__(self, remove_annotations: list[AnnotationType]):  # type: ignore
         )
 
     def separate_validator_errors(self, errors: str) -> tuple[str, str]:
-        raise NotImplementedError(
-            "Separating validator errors is not implemented for Verus yet"
-        )
+        lines = errors.split("\n")
+        lines = [
+            line for line in lines if "Verification successful" not in line and "Verification took" not in line
+        ]
+        return "\n".join(lines), ""