File size: 1,810 Bytes
56de343 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 | module Main where
import System.Environment (getArgs)
import System.Exit (exitFailure, exitSuccess)
import Language.AST
import Language.Parser (parseModule)
import Language.Elaborator (elaborate)
import IR.Boolean (Circuit(..), circuitBody)
import Proof.Produce (proveValidity)
import Proof.Certificate (ProofCertificate(..), ProofConclusion(..))
import Checker.Kernel (checkCertificate, CheckResult(..))
main :: IO ()
main = do
args <- getArgs
case args of
[file] -> verifyFile file
_ -> putStrLn "Usage: pure-validity <file.nf>" >> exitFailure
verifyFile :: FilePath -> IO ()
verifyFile path = do
src <- readFile path
let name = takeWhile (/= '.') $ reverse $ takeWhile (/= '/') $ reverse path
case parseModule name src of
Left err -> do
putStrLn $ "PARSE ERROR: " ++ err
exitFailure
Right modul -> do
case elaborate modul of
Left err -> do
putStrLn $ "ELABORATION ERROR: " ++ show err
exitFailure
Right circuits -> do
putStrLn $ "Module: " ++ name
putStrLn $ "Properties: " ++ show (length circuits)
putStrLn ""
results <- mapM verifyCircuit circuits
let passed = length $ filter id results
total = length results
putStrLn ""
putStrLn $ show passed ++ "/" ++ show total ++ " verified."
if passed == total then exitSuccess else exitFailure
verifyCircuit :: Circuit -> IO Bool
verifyCircuit (Circuit name _ body) = do
let cert = proveValidity name body
case checkCertificate cert of
Verified vname -> do
putStrLn $ " [OK] " ++ vname
return True
Rejected rname reason -> do
putStrLn $ " [FAIL] " ++ rname ++ " — " ++ reason
return False
|