Merge pull request #446 from yavivanov/pr-plainOpenGoals-fix

Solving the second issue of PR#394 without plainOpenGoals

Makefile

@@ -422,6 +422,10 @@ accountability-case-studies:	$(ACCOUNTABILITY_CS_TARGETS)
 ## Regression (old issues)
 ##########################
 
+FAST_REGRESSION_CASE_STUDIES=issue446-1.spthy issue446-2.spthy
+FAST_REGRESSION_TARGETS=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies$(SUBDIR)regression/trace/,$(FAST_REGRESSION_CASE_STUDIES)))
+
+
 REGRESSION_CASE_STUDIES=issue216.spthy issue193.spthy issue310.spthy issue519.spthy issue527.spthy issue515.spthy
 
 REGRESSION_TARGETS=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies$(SUBDIR)regression/trace/,$(REGRESSION_CASE_STUDIES)))
@@ -433,7 +437,7 @@ DEFAULTORACLE_CASE_STUDIES=defaultoracle.spthy
 DEFAULTORACLE_CASE_TARGETS=$(subst .spthy,_analyzed-deforacle.spthy, $(addprefix case-studies$(SUBDIR)regression/trace/,$(DEFAULTORACLE_CASE_STUDIES)))
 
 # case studies
-regression-case-studies:	$(REGRESSION_TARGETS) $(SEQDFS_TARGETS) $(DEFAULTORACLE_CASE_TARGETS)
+regression-case-studies:	$(REGRESSION_TARGETS) $(SEQDFS_TARGETS) $(DEFAULTORACLE_CASE_TARGETS) $(FAST_REGRESSION_TARGETS)
 	grep "verified\|falsified\|processing time" case-studies$(SUBDIR)regression/trace/*.spthy
 
 
@@ -491,7 +495,7 @@ case-studies: 	case-studies$(SUBDIR)system.info $(CS_TARGETS)
 ## Fast case studies
 ####################
 
-FAST_CS_TARGETS = case-studies$(SUBDIR)Tutorial_analyzed.spthy $(CCS15_PCS_TARGETS) $(TESTOBSEQ_TARGETS) $(FEATURES_CS_TARGETS) $(REGRESSION_OBSEQ_TARGETS) $(CSF12_CS_TARGETS) $(IND_CS_TARGETS) $(CCS15_CS_TARGETS) $(XOR_TRACE_TARGETS) $(POST17_TRACE_TARGETS) $(CLASSIC_CS_TARGETS) $(AKE_BP_CS_TARGETS) $(SEQDFS_TARGETS) $(DEFAULTORACLE_CASE_TARGETS) $(XOR_DIFF_OBSEQONLY_TARGETS)
+FAST_CS_TARGETS = case-studies$(SUBDIR)Tutorial_analyzed.spthy $(CCS15_PCS_TARGETS) $(TESTOBSEQ_TARGETS) $(FEATURES_CS_TARGETS) $(REGRESSION_OBSEQ_TARGETS) $(CSF12_CS_TARGETS) $(IND_CS_TARGETS) $(CCS15_CS_TARGETS) $(XOR_TRACE_TARGETS) $(POST17_TRACE_TARGETS) $(CLASSIC_CS_TARGETS) $(AKE_BP_CS_TARGETS) $(SEQDFS_TARGETS) $(DEFAULTORACLE_CASE_TARGETS) $(FAST_REGRESSION_TARGETS) $(XOR_DIFF_OBSEQONLY_TARGETS)
 
 fast-case-studies: case-studies$(SUBDIR)system.info $(FAST_CS_TARGETS)
 	mkdir -p case-studies$(SUBDIR)

case-studies-regression/fast-tests/regression/trace/issue446-1_analyzed.spthy

@@ -0,0 +1,69 @@
+theory lemma_falsified_verified begin
+
+// Function signature and definition of the equational theory E
+
+functions: fst/1, pair/2, snd/1
+equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
+
+
+
+
+
+rule (modulo E) A:
+   [ ] --[ A( 'x' ) ]-> [ ]
+
+  /* has exactly the trivial AC variant */
+
+lemma lemma_verified:
+  all-traces "∀ x #i. (A( x ) @ #i) ⇒ (A( x ) @ #i)"
+/*
+guarded formula characterizing all counter-examples:
+"∃ x #i. (A( x ) @ #i) ∧ ¬(A( x ) @ #i)"
+*/
+simplify
+by contradiction /* from formulas */
+
+lemma lemma_falsified:
+  all-traces "∀ x #i. (A( x ) @ #i) ⇒ (A( x ) @ #i)"
+/*
+guarded formula characterizing all counter-examples:
+"∃ x #i. (A( x ) @ #i) ∧ ¬(A( x ) @ #i)"
+*/
+simplify
+by contradiction /* from formulas */
+
+
+
+
+
+
+
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 2023bf45660993c250f71bea8f123d870bfb3e82 (with uncommited changes), branch: pr-plainOpenGoals-fix
+Compiled at: 2023-11-21 21:42:44.712168244 UTC
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.2. OK.
+ checking installation: OK.
+
+==============================================================================
+summary of summaries:
+
+analyzed: examples/regression/trace/issue446-1.spthy
+
+  output:          examples/regression/trace/issue446-1.spthy.tmp
+  processing time: 0.05s
+
+  lemma_verified (all-traces): verified (2 steps)
+  lemma_falsified (all-traces): verified (2 steps)
+
+==============================================================================
+*/

case-studies-regression/fast-tests/regression/trace/issue446-2_analyzed.spthy

@@ -0,0 +1,60 @@
+theory MinValueEq begin
+
+// Function signature and definition of the equational theory E
+
+functions: fst/1, pair/2, snd/1
+equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
+
+
+
+
+
+rule (modulo E) AttackerMsg:
+   [ In( x ) ] --[ Value( x ) ]-> [ ]
+
+  /* has exactly the trivial AC variant */
+
+lemma WrongEquality:
+  all-traces
+  "∀ a b #i #j. ((Value( a ) @ #i) ∧ (Value( b ) @ #j)) ⇒ (a = b)"
+/*
+guarded formula characterizing all counter-examples:
+"∃ a b #i #j. (Value( a ) @ #i) ∧ (Value( b ) @ #j) ∧ ¬(a = b)"
+*/
+simplify
+SOLVED // trace found
+
+
+
+
+
+
+
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.9.0
+Maude version 3.2.2
+Git revision: 2023bf45660993c250f71bea8f123d870bfb3e82 (with uncommited changes), branch: pr-plainOpenGoals-fix
+Compiled at: 2023-11-21 21:42:44.712168244 UTC
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.2. OK.
+ checking installation: OK.
+
+==============================================================================
+summary of summaries:
+
+analyzed: examples/regression/trace/issue446-2.spthy
+
+  output:          examples/regression/trace/issue446-2.spthy.tmp
+  processing time: 0.06s
+
+  WrongEquality (all-traces): falsified - found trace (2 steps)
+
+==============================================================================
+*/

examples/regression/trace/issue446-1.spthy

@@ -0,0 +1,25 @@
+theory lemma_falsified_verified
+begin
+
+/*
+* Date: November 2021
+* Comment: Minimal example for a missing check if
+* 'SOLVED' is present with a non-empty but incomplete proof.
+*/
+
+rule A:
+   [ ]
+ --[ A('x')]->
+   [ ]
+
+lemma lemma_verified:
+  all-traces
+  "All x #i. A(x)@i ==> A(x)@i"
+
+lemma lemma_falsified:
+  all-traces
+  "All x #i. A(x)@i ==> A(x)@i"
+simplify
+SOLVED
+
+end

examples/regression/trace/issue446-2.spthy

@@ -0,0 +1,20 @@
+theory MinValueEq
+begin
+
+/*
+* Author: Philip Lukert
+* Date: November 2021
+* Comment: minimal counterexample for issue 329
+*/
+
+rule AttackerMsg:
+    [ In(x) ]
+  --[ Value(x) ]->
+    [ ]
+
+// should fail
+lemma WrongEquality:
+"All a b #i #j. Value(a)@i & Value(b)@j ==> a=b"
+
+
+end

lib/theory/src/Theory/Constraint/Solver/ProofMethod.hs

@@ -244,11 +244,11 @@ execProofMethod ctxt method sys =
       case method of
         Sorry _                                -> return M.empty
         Solved
-          | null (openGoals sys)
+          | null (openGoals sys)  && not (contradictorySystem ctxt sys)
             && finishedSubterms ctxt sys       -> return M.empty
           | otherwise                          -> Nothing
         Unfinishable
-          | null (openGoals sys)
+          | null (openGoals sys)  && not (contradictorySystem ctxt sys)
             && not (finishedSubterms ctxt sys) -> return M.empty
           | otherwise                          -> Nothing
         SolveGoal goal