Add tests that run on github actions

.github/workflows/test-pytest.yml

@@ -0,0 +1,38 @@
+name: Run pytest
+
+on: [push]
+
+env:
+  PYTHON_VERSION: "3.11"
+  POETRY_VERSION: "1.4.2"
+  POETRY_URL: https://install.python-poetry.org
+
+jobs:
+  run-pytest:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Set up Python ${{ env.PYTHON_VERSION }}
+        uses: actions/setup-python@v4
+        with:
+          python-version: ${{ env.PYTHON_VERSION }}
+        id: setup_python
+      - name: Cache Poetry cache
+        uses: actions/cache@v3
+        with:
+          path: ~/.cache/pypoetry
+          key: poetry-cache-${{ runner.os }}-${{ steps.setup_python.outputs.python-version }}-${{ env.POETRY_VERSION }}
+      - name: Cache Packages
+        uses: actions/cache@v3
+        with:
+          path: ~/.local
+          key: poetry-local-${{ runner.os }}-${{ steps.setup_python.outputs.python-version }}-${{ hashFiles('**/poetry.lock') }}-${{ hashFiles('.github/workflows/*.yml') }}
+      - name: Install Poetry ${{ env.POETRY_VERSION }}
+        run: |
+          curl -sSL ${{ env.POETRY_URL }} | python - --version ${{ env.POETRY_VERSION }}
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+      - name: Install Dependencies
+        run: poetry install
+      - name: Run pytest
+        run: poetry run pytest

tests/test_remove.py

@@ -0,0 +1,107 @@
+from textwrap import dedent
+from verified_cogen.runners.validating import remove_asserts_and_invariants
+
+
+def test_remove_line():
+    code = dedent(
+        """\
+        method main() {
+            assert a == 1; // assert-line
+        }"""
+    )
+    assert remove_asserts_and_invariants(code) == dedent(
+        """\
+        method main() {
+        }"""
+    )
+
+
+def test_remove_multiline_assert():
+    code = dedent(
+        """\
+        method main() {
+            // assert-start
+            assert a == 1 by {
+
+            }
+            // assert-end
+        }"""
+    )
+    assert remove_asserts_and_invariants(code) == dedent(
+        """\
+        method main() {
+        }"""
+    )
+
+
+def test_remove_invariants():
+    code = dedent(
+        """\
+        method main() {
+            while true
+                // invariants-start
+                invariant false
+                invariant true
+                // invariants-end
+            {
+            }
+        }"""
+    )
+    assert remove_asserts_and_invariants(code) == dedent(
+        """\
+        method main() {
+            while true
+            {
+            }
+        }"""
+    )
+
+
+def test_remove_all():
+    code = dedent(
+        """\
+        method is_prime(k: int) returns (result: bool)
+          requires k >= 2
+          ensures result ==> forall i :: 2 <= i < k ==> k % i != 0
+          ensures !result ==> exists j :: 2 <= j < k && k % j == 0
+        {
+          var i := 2;
+          result := true;
+          while i < k
+            // invariants-start
+            invariant 2 <= i <= k
+            invariant !result ==> exists j :: 2 <= j < i && k % j == 0
+            invariant result ==> forall j :: 2 <= j < i ==> k % j != 0
+            // invariants-end
+          {
+            if k % i == 0 {
+              result := false;
+            }
+            assert result ==> forall j :: 2 <= j < i ==> k % j != 0; // assert-line
+            // assert-start
+            assert !result ==> exists j :: 2 <= j < i && k % j == 0 by {
+                assert true;
+            }
+            // assert-end
+            i := i + 1;
+          }
+        }"""
+    )
+    assert remove_asserts_and_invariants(code) == dedent(
+        """\
+        method is_prime(k: int) returns (result: bool)
+          requires k >= 2
+          ensures result ==> forall i :: 2 <= i < k ==> k % i != 0
+          ensures !result ==> exists j :: 2 <= j < k && k % j == 0
+        {
+          var i := 2;
+          result := true;
+          while i < k
+          {
+            if k % i == 0 {
+              result := false;
+            }
+            i := i + 1;
+          }
+        }"""
+    )

verified_cogen/runners/validating.py

@@ -7,7 +7,9 @@
 from verified_cogen.runners.invariants import InvariantRunner
 
 # Regular expression to match Dafny method definitions
-method_pattern = re.compile(r'method\s+(\w+)\s*\((.*?)\)\s*returns\s*\((.*?)\)(.*?)\{', re.DOTALL)
+method_pattern = re.compile(
+    r"method\s+(\w+)\s*\((.*?)\)\s*returns\s*\((.*?)\)(.*?)\{", re.DOTALL
+)
 
 
 def generate_validators(dafny_code: str) -> str:
@@ -34,7 +36,9 @@ def generate_validators(dafny_code: str) -> str:
         returns = match.group(3)
         specs = match.group(4)
 
-        validator = f"method {method_name}_valid({parameters}) returns ({returns}){specs}"
+        validator = (
+            f"method {method_name}_valid({parameters}) returns ({returns}){specs}"
+        )
         validator += "{ var ret := "
 
         validator += f"{method_name}({', '.join(param.split(':')[0].strip() for param in parameters.split(',') if param.strip())});"
@@ -43,23 +47,23 @@ def generate_validators(dafny_code: str) -> str:
 
         validators.append(validator)
 
-    return '\n'.join(validators)
+    return "\n".join(validators)
 
 
 def remove_asserts_and_invariants(dafny_code: str) -> str:
     patterns = [
-        r'// assert-line.*\n',
-        r'// assert-start.*?// assert-end\n',
-        r'// invariants-start.*?// invariants-end\n'
+        r" *// assert-start.*?// assert-end\n",
+        r" *// invariants-start.*?// invariants-end\n",
     ]
-    combined_pattern = '|'.join(patterns)
-    cleaned_code = re.sub(combined_pattern, '', dafny_code, flags=re.DOTALL)
-    cleaned_code = re.sub(r'\n\s*\n', '\n', cleaned_code)
-    return cleaned_code.strip()
+    combined_pattern = "|".join(patterns)
+    cleaned_code = re.sub(combined_pattern, "", dafny_code, flags=re.DOTALL)
+    cleaned_code = re.sub(r"\n\s*\n", "\n", cleaned_code)
+    lines = cleaned_code.split("\n")
+    lines = [line for line in lines if "// assert-line" not in line]
+    return "\n".join(lines).strip()
 
 
 class ValidatingRunner(Runner):
-
     @classmethod
     def _add_validators(cls, prg: str, inv_prg: str):
         validators = generate_validators(prg)
@@ -80,7 +84,9 @@ def produce(cls, llm: LLM, prg: str) -> str:
 
     @classmethod
     def insert(cls, llm: LLM, prg: str, checks: str, mode: Mode) -> str:
-        return ValidatingRunner._add_validators(prg, InvariantRunner.insert(llm, prg, checks, mode))
+        return ValidatingRunner._add_validators(
+            prg, InvariantRunner.insert(llm, prg, checks, mode)
+        )
 
     @classmethod
     def precheck(cls, prg: str, mode: Mode):