Skip to content

Commit

Permalink
Revert "Interactive prover that stops when oracle returns nothing"
Browse files Browse the repository at this point in the history
  • Loading branch information
@cascremers
cascremers committed Jun 14, 2024
1 parent beb4f03 commit a4b4929
Show file tree
Hide file tree
Showing 8 changed files with 125 additions and 138 deletions.
1 change: 0 additions & 1 deletion data/js/tamarin-prover-ui.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,6 @@ var ui = {
65 : function() { mainDisplay.applyProver('characterization'); }, // A
98 : function() { mainDisplay.applyProver('bounded-autoprove'); }, // b
66 : function() { mainDisplay.applyProver('bounded-characterization'); }, // B
111 : function() { mainDisplay.applyProver('oracle-autoprove'); },
115 : function() { mainDisplay.applyProver('autoprove-all'); }, // s
83 : function() { mainDisplay.applyProver('characterization-all'); }, // S
74 : function() { proofScript.jump('next/smart', null); }, // j
Expand Down
162 changes: 92 additions & 70 deletions lib/theory/src/Theory/Constraint/Solver/ProofMethod.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ import Data.Label hiding (get)
import qualified Data.Label as L
import Data.List (intersperse,partition,groupBy,sortBy,isPrefixOf,findIndex,intercalate)
import qualified Data.Map as M
import Data.Maybe (catMaybes, fromMaybe, mapMaybe)
import Data.Maybe (catMaybes, fromMaybe)
-- import Data.Monoid
import Data.Ord (comparing)
import qualified Data.Set as S
Expand Down Expand Up @@ -449,34 +449,28 @@ finishedSubterms pc sys = hasReducibleOperatorsOnTop (reducibleFunSyms $ mhMaude
-- Heuristics
------------------------------------------------------------------------------

data ProofInstruction = ApplySorry

data Ranking a = Ranking
{ ranked :: a
, instruction :: Maybe ProofInstruction }

plainRanking :: a -> Ranking a
plainRanking = (`Ranking` Nothing)

-- | Use a 'GoalRanking' to sort a list of 'AnnotatedGoal's stemming from the
-- given constraint 'System'.
rankGoals :: ProofContext -> GoalRanking ProofContext -> [Tactic ProofContext] -> System -> [AnnotatedGoal] -> Ranking [AnnotatedGoal]
rankGoals ctxt ranking tacticsList sys = case ranking of
GoalNrRanking -> plainRanking . goalNrRanking
OracleRanking quitOnEmpty oracleName -> oracleRanking (const goalNrRanking) oracleName quitOnEmpty ctxt sys
OracleSmartRanking quitOnEmpty oracleName -> oracleRanking (smartRanking ctxt False) oracleName quitOnEmpty ctxt sys
UsefulGoalNrRanking -> plainRanking. sortOn (\(_, (nr, useless)) -> (useless, nr))
SapicRanking -> plainRanking . sapicRanking ctxt sys
SapicPKCS11Ranking -> plainRanking . sapicPKCS11Ranking ctxt sys
SmartRanking useLoopBreakers -> plainRanking . smartRanking ctxt useLoopBreakers sys
SmartDiffRanking -> plainRanking . smartDiffRanking ctxt sys
InjRanking useLoopBreakers -> plainRanking . injRanking ctxt useLoopBreakers sys
InternalTacticRanking quitOnEmpty tactic -> internalTacticRanking (chosenTactic tacticsList tactic) quitOnEmpty ctxt sys
rankGoals :: ProofContext -> GoalRanking ProofContext -> [Tactic ProofContext] -> System -> [AnnotatedGoal] -> [AnnotatedGoal]
rankGoals ctxt ranking tacticsList = case ranking of
GoalNrRanking -> \_sys -> goalNrRanking
OracleRanking oracleName -> oracleRanking oracleName ctxt
OracleSmartRanking oracleName -> oracleSmartRanking oracleName ctxt
UsefulGoalNrRanking ->
\_sys -> sortOn (\(_, (nr, useless)) -> (useless, nr))
SapicRanking -> sapicRanking ctxt
SapicPKCS11Ranking -> sapicPKCS11Ranking ctxt
SmartRanking useLoopBreakers -> smartRanking ctxt useLoopBreakers
SmartDiffRanking -> smartDiffRanking ctxt
InjRanking useLoopBreakers -> injRanking ctxt useLoopBreakers
InternalTacticRanking tactic-> internalTacticRanking (chosenTactic tacticsList tactic) ctxt

where
chosenTactic :: [Tactic ProofContext] -> Tactic ProofContext-> Tactic ProofContext
chosenTactic [] t = chooseError tacticsList t
chosenTactic (h:q) t = if checkName h t then h else chosenTactic q t
chosenTactic (h:q) t = case (checkName h t) of
True -> h
False -> chosenTactic q t

definedHeuristic = intercalate [','] (foldl (\acc x -> (_name x):acc ) [] tacticsList)

Expand All @@ -491,23 +485,17 @@ rankGoals ctxt ranking tacticsList sys = case ranking of
-- system is solved.
rankProofMethods :: GoalRanking ProofContext -> [Tactic ProofContext] -> ProofContext -> System
-> [(ProofMethod, (M.Map CaseName System, String))]
rankProofMethods ranking tactics ctxt sys =
let rankedGoals = rankGoals ctxt ranking tactics sys $ openGoals sys
cs = contradictions ctxt sys
in case rankedGoals of
Ranking gs (Just ApplySorry)
| null cs && not (null gs) -> [(Sorry (Just "Oracle ranked no goals"), (M.empty, ""))]
Ranking gs _ -> do
(m, expl) <-
(contradiction <$> cs)
<|> (case L.get pcUseInduction ctxt of
AvoidInduction -> [(Simplify, ""), (Induction, "")]
UseInduction -> [(Induction, ""), (Simplify, "")]
)
<|> (solveGoalMethod <$> gs)
case execProofMethod ctxt m sys of
Just cases -> return (m, (cases, expl))
Nothing -> []
rankProofMethods ranking tactics ctxt sys = do
(m, expl) <-
(contradiction <$> contradictions ctxt sys)
<|> (case L.get pcUseInduction ctxt of
AvoidInduction -> [(Simplify, ""), (Induction, "")]
UseInduction -> [(Induction, ""), (Simplify, "")]
)
<|> (solveGoalMethod <$> (rankGoals ctxt ranking tactics sys $ openGoals sys))
case execProofMethod ctxt m sys of
Just cases -> return (m, (cases, expl))
Nothing -> []
where
contradiction c = (Contradiction (Just c), "")

Expand Down Expand Up @@ -595,38 +583,72 @@ goalNrRanking = sortOn (fst . snd)

-- | A ranking function using an external oracle to allow user-definable
-- heuristics for each lemma separately.
oracleRanking :: (System -> [AnnotatedGoal] -> [AnnotatedGoal])
-> Oracle
-> Bool
oracleRanking :: Oracle
-> ProofContext
-> System
-> [AnnotatedGoal]
-> Ranking [AnnotatedGoal]
oracleRanking preSort oracle quitOnEmpty ctxt _sys ags0 = unsafePerformIO $ do
let ags = preSort _sys ags0
let inp = unlines $ zipWith (\i ag -> show i ++": "++ (concat . lines . render $ pgoal ag)) [(0::Int)..] ags
outp <- readProcess (oraclePath oracle) [ L.get pcLemmaName ctxt ] inp

let indices = mapMaybe readMay $ lines outp
ranked = mapMaybe (atMay ags) indices
remaining = filter (`notElem` ranked) ags
logMsg = ">>>>>>>>>>>>>>>>>>>>>>>> START INPUT\n"
++ inp
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> START OUTPUT\n"
++ outp
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> END Oracle call\n"
guard $ trace logMsg True

return (Ranking (ranked ++ remaining)
(guard (quitOnEmpty && null ranked) *> Just ApplySorry))
-> [AnnotatedGoal] -> [AnnotatedGoal]
oracleRanking oracle ctxt _sys ags0
-- | AvoidInduction == (L.get pcUseInduction ctxt) = ags0
| otherwise =
unsafePerformIO $ do
let ags = goalNrRanking ags0
let inp = unlines
(map (\(i,ag) -> show i ++": "++ (concat . lines . render $ pgoal ag))
(zip [(0::Int)..] ags))
outp <- readProcess (oraclePath oracle) [ L.get pcLemmaName ctxt ] inp

let indices = catMaybes . map readMay . lines $ outp
ranked = catMaybes . map (atMay ags) $ indices
remaining = filter (`notElem` ranked) ags
logMsg = ">>>>>>>>>>>>>>>>>>>>>>>> START INPUT\n"
++ inp
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> START OUTPUT\n"
++ outp
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> END Oracle call\n"
guard $ trace logMsg True
-- _ <- getLine
-- let sd = render $ vcat $ map prettyNode $ M.toList $ L.get sNodes sys
-- guard $ trace sd True

return (ranked ++ remaining)
where
pgoal (g,(_nr,_usefulness)) = prettyGoal g

-- | A ranking function using an external oracle to allow user-definable
-- heuristics for each lemma separately, using the smartRanking heuristic
-- as the baseline.
oracleSmartRanking :: Oracle
-> ProofContext
-> System
-> [AnnotatedGoal] -> [AnnotatedGoal]
oracleSmartRanking oracle ctxt _sys ags0
-- | AvoidInduction == (L.get pcUseInduction ctxt) = ags0
| otherwise =
unsafePerformIO $ do
let ags = smartRanking ctxt False _sys ags0
let inp = unlines
(map (\(i,ag) -> show i ++": "++ (concat . lines . render $ pgoal ag))
(zip [(0::Int)..] ags))
outp <- readProcess (oraclePath oracle) [ L.get pcLemmaName ctxt ] inp
let indices = catMaybes . map readMay . lines $ outp
ranked = catMaybes . map (atMay ags) $ indices
remaining = filter (`notElem` ranked) ags
logMsg = ">>>>>>>>>>>>>>>>>>>>>>>> START INPUT\n"
++ inp
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> START OUTPUT\n"
++ outp
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> END Oracle call\n"
guard $ trace logMsg True
-- let sd = render $ vcat $ map prettyNode $ M.toList $ L.get sNodes sys

return (ranked ++ remaining)
where
pgoal (g,(_nr,_usefulness)) = prettyGoal g

-- | This function apply a tactic to a list of AnnotatedGoals to retrive an ordered list according
-- | to its Prio/Deprio's functions
itRanking :: Tactic ProofContext -> [AnnotatedGoal] -> Bool -> ProofContext -> System -> Ranking [AnnotatedGoal]
itRanking tactic ags quitOnEmpty ctxt _sys =
Ranking result (guard (quitOnEmpty && null rankedPrioGoals && null rankedDeprioGoals) *> Just ApplySorry)
itRanking :: Tactic ProofContext -> [AnnotatedGoal] -> ProofContext -> System -> [AnnotatedGoal]
itRanking tactic ags ctxt _sys = result
where
-- Getting the functions from priorities
prioToFunctions = map functionsPrio (_prios tactic)
Expand Down Expand Up @@ -692,18 +714,18 @@ itRanking tactic ags quitOnEmpty ctxt _sys =
-- | A ranking function using a tactic to allow user-definable heuristics
-- for each lemma separately, using the user chosen defaultMethod heuristic
-- as the baseline.
internalTacticRanking :: Tactic ProofContext -> Bool -> ProofContext -> System -> [AnnotatedGoal] -> Ranking [AnnotatedGoal]
internalTacticRanking tactic quitOnEmpty ctxt _sys ags0 = trace logMsg res
internalTacticRanking :: Tactic ProofContext -> ProofContext -> System -> [AnnotatedGoal] -> [AnnotatedGoal]
internalTacticRanking tactic ctxt _sys ags0 = trace logMsg res
where
defaultMethod = _presort tactic -- retrieve baseline heuristic
ags = ranked $ rankGoals ctxt defaultMethod [tactic] _sys ags0 -- get goals accordingly
ags = rankGoals ctxt defaultMethod [tactic] _sys ags0 -- get goals accordingly
pgoal (g,(_nr,_usefulness)) = prettyGoal g
inp = unlines
(map (\(i,ag) -> show i ++": "++ (concat . lines . render $ pgoal ag))
(zip [(0::Int)..] ags))
res = itRanking tactic ags quitOnEmpty ctxt _sys -- apply the tactic ranking
res = itRanking tactic ags ctxt _sys -- apply the tactic ranking
dict = M.fromList (zip ags [(0::Int)..])
outp = map (fromMaybe (-1) . flip M.lookup dict) (ranked res)
outp = map (fromMaybe (-1)) (map (flip M.lookup dict) res)
prettyOut = unlines (map show outp)
logMsg = ">>>>>>>>>>>>>>>>>>>>>>>> START INPUT\n"
++ inp
Expand Down
53 changes: 22 additions & 31 deletions lib/theory/src/Theory/Constraint/System.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@ module Theory.Constraint.System (
, Deprio(..)
-- , Ranking(..)
, defaultTactic
, usesOracle
, mapInternalTacticRanking
, maybeSetInternalTacticName

Expand Down Expand Up @@ -508,9 +507,9 @@ data Tactic a = Tactic{
-- order of solving in a constraint system.
data GoalRanking a =
GoalNrRanking
| OracleRanking Bool Oracle
| OracleSmartRanking Bool Oracle
| InternalTacticRanking Bool (Tactic a)
| OracleRanking Oracle
| OracleSmartRanking Oracle
| InternalTacticRanking (Tactic a)
| SapicRanking
| SapicPKCS11Ranking
| UsefulGoalNrRanking
Expand All @@ -534,14 +533,6 @@ defaultHeuristic = Heuristic . defaultRankings
defaultTactic :: Tactic ProofContext
defaultTactic = Tactic "default" (SmartRanking False) [] []

usesOracle :: Heuristic a -> Bool
usesOracle (Heuristic rs) = all isOracleRanking rs
where
isOracleRanking :: GoalRanking a -> Bool
isOracleRanking (OracleRanking _ _) = True
isOracleRanking (OracleSmartRanking _ _) = True
isOracleRanking (InternalTacticRanking _ _) = True
isOracleRanking _ = False

-- Default to "./oracle" in the current working directory.
defaultOracle :: Oracle
Expand All @@ -567,8 +558,8 @@ maybeSetOracleRelPath :: Maybe FilePath -> Oracle -> Oracle
maybeSetOracleRelPath p o = o{ oracleRelPath = p }

mapOracleRanking :: (Oracle -> Oracle) -> (GoalRanking ProofContext) -> (GoalRanking ProofContext)
mapOracleRanking f (OracleRanking b o) = OracleRanking b (f o)
mapOracleRanking f (OracleSmartRanking b o) = OracleSmartRanking b (f o)
mapOracleRanking f (OracleRanking o) = OracleRanking (f o)
mapOracleRanking f (OracleSmartRanking o) = OracleSmartRanking (f o)
mapOracleRanking _ r = r

oraclePath :: Oracle -> FilePath
Expand All @@ -578,23 +569,23 @@ maybeSetInternalTacticName :: Maybe String -> Tactic ProofContext -> Tactic Proo
maybeSetInternalTacticName s t = maybe t (\x -> t{ _name = x }) s

mapInternalTacticRanking :: (Tactic ProofContext -> Tactic ProofContext) -> GoalRanking ProofContext -> GoalRanking ProofContext
mapInternalTacticRanking f (InternalTacticRanking q t) = InternalTacticRanking q (f t)
mapInternalTacticRanking f (InternalTacticRanking t) = InternalTacticRanking (f t)
mapInternalTacticRanking _ r = r


goalRankingIdentifiers :: M.Map String (GoalRanking ProofContext)
goalRankingIdentifiers = M.fromList
[ ("s", SmartRanking False)
, ("S", SmartRanking True)
, ("o", OracleRanking False defaultOracle)
, ("O", OracleSmartRanking False defaultOracle)
, ("o", OracleRanking defaultOracle)
, ("O", OracleSmartRanking defaultOracle)
, ("p", SapicRanking)
, ("P", SapicPKCS11Ranking)
, ("c", UsefulGoalNrRanking)
, ("C", GoalNrRanking)
, ("i", InjRanking False)
, ("I", InjRanking True)
, ("{.}", InternalTacticRanking False defaultTactic)
, ("{.}", InternalTacticRanking defaultTactic)
]

goalRankingIdentifiersNoOracle :: M.Map String (GoalRanking ProofContext)
Expand Down Expand Up @@ -626,11 +617,11 @@ goalRankingIdentifiersDiff :: M.Map String (GoalRanking ProofContext)
goalRankingIdentifiersDiff = M.fromList
[ ("s", SmartDiffRanking)
, ("S", SmartRanking True)
, ("o", OracleRanking False defaultOracle)
, ("O", OracleSmartRanking False defaultOracle)
, ("o", OracleRanking defaultOracle)
, ("O", OracleSmartRanking defaultOracle)
, ("c", UsefulGoalNrRanking)
, ("C", GoalNrRanking)
, ("{.}", InternalTacticRanking False defaultTactic)
, ("{.}", InternalTacticRanking defaultTactic)
]

goalRankingIdentifiersDiffNoOracle :: M.Map String (GoalRanking ProofContext)
Expand Down Expand Up @@ -678,7 +669,7 @@ listGoalRankingsDiff noOracle = M.foldMapWithKey


filterHeuristic :: Bool -> String -> [GoalRanking ProofContext]
filterHeuristic diff ('{':t) = if '}' `elem` t then InternalTacticRanking False (Tactic (takeWhile (/= '}') t) (SmartRanking False) [] []):(filterHeuristic diff $ tail $ dropWhile (/= '}') t) else error "A call to a tactic is supposed to end by '}' "
filterHeuristic diff ('{':t) = if '}' `elem` t then InternalTacticRanking (Tactic (takeWhile (/= '}') t) (SmartRanking False) [] []):(filterHeuristic diff $ tail $ dropWhile (/= '}') t) else error "A call to a tactic is supposed to end by '}' "
filterHeuristic False (c:t) = (stringToGoalRanking False [c]):(filterHeuristic False t)
filterHeuristic True (c:t) = (stringToGoalRankingDiff False [c]):(filterHeuristic True t)
filterHeuristic _ ("") = []
Expand All @@ -688,15 +679,15 @@ goalRankingName :: GoalRanking ProofContext -> String
goalRankingName ranking =
"Goals sorted according to " ++ case ranking of
GoalNrRanking -> "their order of creation"
OracleRanking _ oracle -> "an oracle for ranking, located at " ++ printOracle oracle
OracleSmartRanking _ oracle -> "an oracle for ranking based on 'smart' heuristic, located at " ++ printOracle oracle
OracleRanking oracle -> "an oracle for ranking, located at " ++ printOracle oracle
OracleSmartRanking oracle -> "an oracle for ranking based on 'smart' heuristic, located at " ++ printOracle oracle
UsefulGoalNrRanking -> "their usefulness and order of creation"
SapicRanking -> "heuristics adapted for processes"
SapicPKCS11Ranking -> "heuristics adapted to a specific model of PKCS#11 expressed using SAPIC. deprecated."
SmartRanking useLoopBreakers -> "the 'smart' heuristic" ++ loopStatus useLoopBreakers
SmartDiffRanking -> "the 'smart' heuristic (for diff proofs)"
InjRanking useLoopBreakers -> "heuristics adapted to stateful injective protocols" ++ loopStatus useLoopBreakers
InternalTacticRanking _ tactic -> "the tactic written in the theory file: "++ _name tactic
InternalTacticRanking tactic -> "the tactic written in the theory file: "++ _name tactic
where
loopStatus b = " (loop breakers " ++ (if b then "allowed" else "delayed") ++ ")"
printOracle o@(Oracle workDir relPath) =
Expand All @@ -709,9 +700,9 @@ prettyGoalRankings rs = unwords (map prettyGoalRanking rs)

prettyGoalRanking :: GoalRanking ProofContext -> String
prettyGoalRanking ranking = case ranking of
OracleRanking _ oracle -> findIdentifier ranking ++ " \"" ++ fromMaybe "" (oracleRelPath oracle) ++ "\""
OracleSmartRanking _ oracle -> findIdentifier ranking ++ " \"" ++ fromMaybe "" (oracleRelPath oracle) ++ "\""
InternalTacticRanking _ tactic -> '{':_name tactic++"}"
OracleRanking oracle -> findIdentifier ranking ++ " \"" ++ fromMaybe "" (oracleRelPath oracle) ++ "\""
OracleSmartRanking oracle -> findIdentifier ranking ++ " \"" ++ fromMaybe "" (oracleRelPath oracle) ++ "\""
InternalTacticRanking tactic -> '{':_name tactic++"}"
_ -> findIdentifier ranking
where
findIdentifier r = case find (compareRankings r . snd) combinedIdentifiers of
Expand All @@ -722,9 +713,9 @@ prettyGoalRanking ranking = case ranking of
-- this assumes the diff rankings don't use a different character for the same goal ranking.
combinedIdentifiers = M.toList goalRankingIdentifiers ++ M.toList goalRankingIdentifiersDiff

compareRankings (OracleRanking _ _) (OracleRanking _ _) = True
compareRankings (OracleSmartRanking _ _) (OracleSmartRanking _ _) = True
compareRankings (InternalTacticRanking _ _) (InternalTacticRanking _ _) = True
compareRankings (OracleRanking _) (OracleRanking _) = True
compareRankings (OracleSmartRanking _) (OracleSmartRanking _) = True
compareRankings (InternalTacticRanking _ ) (InternalTacticRanking _ ) = True
compareRankings r1 r2 = r1 == r2


Expand Down
Loading

0 comments on commit a4b4929

Please sign in to comment.