mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-04 20:03:40 +00:00
35 lines
1.1 KiB
Python
35 lines
1.1 KiB
Python
|
from pacta.audit import scan_hygiene, strip_lean_comments
|
||
|
|
from pacta.manifest import discover_layout
|
||
|
|
|
||
|
|
|
||
|
|
def test_strip_comments_avoids_false_sorry():
|
||
|
|
text = "-- sorry\n/- axiom hidden -/\ntheorem ok : True := by trivial\n"
|
||
|
|
stripped = strip_lean_comments(text)
|
||
|
|
assert "sorry" not in stripped
|
||
|
|
assert "axiom hidden" not in stripped
|
||
|
|
assert "by trivial" in stripped
|
||
|
|
|
||
|
|
|
||
|
|
def test_hygiene_detects_forbidden_patterns(tmp_path):
|
||
|
|
proofs = tmp_path / "repo" / "verification" / "Proofs"
|
||
|
|
proofs.mkdir(parents=True)
|
||
|
|
(proofs / "SpecMain.lean").write_text(
|
||
|
|
"""
|
||
|
|
axiom bad : True
|
||
|
|
theorem empty : True := by trivial
|
||
|
|
theorem gap : Nat := by
|
||
|
|
sorry
|
||
|
|
def x := by native_decide
|
||
|
|
""",
|
||
|
|
encoding="utf-8",
|
||
|
|
)
|
||
|
|
layout = discover_layout(tmp_path / "repo")
|
||
|
|
issues = scan_hygiene(layout, certificates=["Missing.cert"])
|
||
|
|
codes = {issue.code for issue in issues}
|
||
|
|
assert "axiom-in-proofs" in codes
|
||
|
|
assert "trivial-true-target" in codes
|
||
|
|
assert "by-trivial-in-spec" in codes
|
||
|
|
assert "sorry" in codes
|
||
|
|
assert "native-decide" in codes
|
||
|
|
assert "missing-certificate-name" in codes
|