Configuration blocks in spthy files and a new default oraclename (#512)

* support for config blocks + new default oraclename

Co-authored-by: Nick Moore <nicholas.moore@cs.ox.ac.uk>

* set backup default oracle to ./oracle

- adapted heuristic code to the tactic code
- added backup default oracle code
- improved the default oraclename code
- adapted the terminal and Web client outputs
- fixed bugs w.r.t. oracle name workdir and printed output

* added configblock comparison to regressionTests.py

* fixed errors resulting from the merge

---------

Co-authored-by: Nick Moore <nicholas.moore@cs.ox.ac.uk>
Co-authored-by: rkunnema <robert.kuennemann@cispa.de>

Makefile

@@ -136,6 +136,19 @@ case-studies$(SUBDIR)%_analyzed-seqdfs.spthy: examples/%.spthy $(TAMARIN)
 	mv $<.tmp $@
 	\rm -f $<.out
 
+# individual case studies, special case with default oracle
+case-studies$(SUBDIR)%_analyzed-deforacle.spthy: examples/%.spthy $(TAMARIN)
+	mkdir -p case-studies$(SUBDIR)regression/trace
+	# Use -N3, as the fourth core is used by the OS and the console
+	cd examples/regression/trace && $(TAMARIN) defaultoracle.spthy --prove +RTS -N3 -RTS -odefaultoracle.spthy.tmp >defaultoracle.spthy.out
+	# We only produce the target after the run, otherwise aborted
+	# runs already 'finish' the case.
+	printf "\n/* Output\n" >>$<.tmp
+	cat $<.out >>$<.tmp
+	echo "*/" >>$<.tmp
+	mv $<.tmp $@
+	\rm -f $<.out
+
 
 ## Observational Equivalence
 ############################
@@ -367,7 +380,7 @@ ake-bp-case-studies:	$(AKE_BP_CS_TARGETS)
 ## Features
 ###########
 
-FEATURES_CASE_STUDIES=cav13/DH_example.spthy features//multiset/counter.spthy features//multiset/NumberSubtermTests.spthy features//private_function_symbols/NAXOS_eCK_PFS_private.spthy features//private_function_symbols/NAXOS_eCK_private.spthy features//injectivity/injectivity.spthy features//macros/MacroExample.spthy features//macros/MacroGlobalVarNSPK3.spthy features//macros/MacroWithRestrictionCRxor.spthy
+FEATURES_CASE_STUDIES=cav13/DH_example.spthy features//multiset/counter.spthy features//multiset/NumberSubtermTests.spthy features//private_function_symbols/NAXOS_eCK_PFS_private.spthy features//private_function_symbols/NAXOS_eCK_private.spthy features//injectivity/injectivity.spthy features//configuration/configuration.spthy features//macros/MacroExample.spthy features//macros/MacroGlobalVarNSPK3.spthy features//macros/MacroWithRestrictionCRxor.spthy
 
 FEATURES_CS_TARGETS=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies$(SUBDIR),$(FEATURES_CASE_STUDIES)))
 
@@ -416,9 +429,11 @@ REGRESSION_TARGETS=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies$(SUBD
 SEQDFS_CASE_STUDIES=seqdfsneeded.spthy
 SEQDFS_TARGETS=$(subst .spthy,_analyzed-seqdfs.spthy,$(addprefix case-studies$(SUBDIR)regression/trace/,$(SEQDFS_CASE_STUDIES)))
 
+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)
+regression-case-studies:	$(REGRESSION_TARGETS) $(SEQDFS_TARGETS) $(DEFAULTORACLE_CASE_TARGETS)
 	grep "verified\|falsified\|processing time" case-studies$(SUBDIR)regression/trace/*.spthy
 
 
@@ -476,7 +491,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) $(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) $(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/features/configuration/configuration_analyzed.spthy

@@ -0,0 +1,59 @@
+theory TestConfiguration 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
+
+
+
+
+
+configuration: "--auto-sources --stop-on-trace=BFS"
+
+rule (modulo E) Testing:
+   [ Fr( x ) ] --[ Test( x ) ]-> [ F1( x ) ]
+
+  /* has exactly the trivial AC variant */
+
+lemma test_lemma:
+  exists-trace "∃ x #i. Test( x ) @ #i"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ x #i. (Test( x ) @ #i)"
+*/
+simplify
+SOLVED // trace found
+
+
+
+
+
+
+
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.2
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.2. OK.
+ checking installation: OK.
+
+==============================================================================
+summary of summaries:
+
+analyzed: examples/features//configuration/configuration.spthy
+
+  output:          examples/features//configuration/configuration.spthy.tmp
+  processing time: 0.03s
+
+  test_lemma (exists-trace): verified (2 steps)
+
+==============================================================================
+*/

case-studies-regression/fast-tests/regression/trace/defaultoracle_analyzed-deforacle.spthy

@@ -0,0 +1,67 @@
+theory DefaultOracle 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
+
+
+
+heuristic: o "defaultoracle.oracle" s o "defaultoracle.oracle" p o "defaultoracle.oracle"
+
+rule (modulo E) Rule:
+   [ ] --[ A( ) ]-> [ ]
+
+  /* has exactly the trivial AC variant */
+
+lemma Test1 [heuristic=s o "" i o "" o ""]:
+  exists-trace "∃ #i. A( ) @ #i"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ #i. (A( ) @ #i)"
+*/
+simplify
+SOLVED // trace found
+
+lemma Test2:
+  exists-trace "∃ #i #j. (A( ) @ #i) ∧ (A( ) @ #j)"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ #i #j. (A( ) @ #i) ∧ (A( ) @ #j)"
+*/
+simplify
+SOLVED // trace found
+
+
+
+
+
+
+
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.2
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.2. OK.
+ checking installation: OK.
+
+==============================================================================
+summary of summaries:
+
+analyzed: defaultoracle.spthy
+
+  output:          defaultoracle.spthy.tmp
+  processing time: 0.22s
+
+  Test1 (exists-trace): verified (2 steps)
+  Test2 (exists-trace): verified (2 steps)
+
+==============================================================================
+*/

case-studies-regression/features/configuration/configuration_analyzed.spthy

@@ -0,0 +1,59 @@
+theory TestConfiguration 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
+
+
+
+
+
+configuration: "--auto-sources --stop-on-trace=BFS"
+
+rule (modulo E) Testing:
+   [ Fr( x ) ] --[ Test( x ) ]-> [ F1( x ) ]
+
+  /* has exactly the trivial AC variant */
+
+lemma test_lemma:
+  exists-trace "∃ x #i. Test( x ) @ #i"
+/*
+guarded formula characterizing all satisfying traces:
+"∃ x #i. (Test( x ) @ #i)"
+*/
+simplify
+SOLVED // trace found
+
+
+
+
+
+
+
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.2
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.2. OK.
+ checking installation: OK.
+
+==============================================================================
+summary of summaries:
+
+analyzed: examples/features//configuration/configuration.spthy
+
+  output:          examples/features//configuration/configuration.spthy.tmp
+  processing time: 0.03s
+
+  test_lemma (exists-trace): verified (2 steps)
+
+==============================================================================
+*/

examples/features/configuration/configuration.spthy

@@ -0,0 +1,14 @@
+theory TestConfiguration
+configuration: "--auto-sources --stop-on-trace=BFS"
+begin
+rule Testing:
+  [ Fr(x) ]
+--[ Test(x) ]->
+  [ F1(x) ]
+
+lemma test_lemma:
+  exists-trace
+  "Ex x #i. Test(x) @ i"
+
+end
+

examples/regression/trace/defaultoracle.oracle

@@ -0,0 +1 @@
+#!/usr/bin/env python3

examples/regression/trace/defaultoracle.spthy

@@ -0,0 +1,16 @@
+theory DefaultOracle
+begin
+
+heuristic: osopo
+rule Rule:
+  []--[A()]->[]
+
+lemma Test1 [heuristic=soioo]:
+  exists-trace
+  " Ex #i. A()@i"
+
+lemma Test2:
+  exists-trace
+  " Ex #i #j. A()@i & A()@j"
+
+end

lib/theory/src/ClosedTheory.hs

@@ -401,6 +401,7 @@ prettyClosedTheory thy = if containsManualRuleVariants mergedRules
     mergedRules = mergeOpenProtoRules $ map (mapTheoryItem openProtoRule id) items
     thy' :: Theory SignatureWithMaude ClosedRuleCache OpenProtoRule IncrementalProof ()
     thy' = Theory {_thyName=(L.get thyName thy)
+            ,_thyInFile=(L.get thyInFile thy)
             ,_thyHeuristic=(L.get thyHeuristic thy)
             ,_thyTactic=(L.get thyTactic thy)
             ,_thySignature=(L.get thySignature thy)
@@ -440,6 +441,7 @@ prettyClosedDiffTheory thy = if containsManualRuleVariantsDiff mergedRules
        map (mapDiffTheoryItem id (\(x, y) -> (x, (openProtoRule y))) id id) items
     thy' :: DiffTheory SignatureWithMaude ClosedRuleCache DiffProtoRule OpenProtoRule IncrementalDiffProof IncrementalProof
     thy' = DiffTheory {_diffThyName=(L.get diffThyName thy)
+            ,_diffThyInFile=(L.get diffThyInFile thy)
             ,_diffThyHeuristic=(L.get diffThyHeuristic thy)
             ,_diffThyTactic=(L.get diffThyTactic thy)
             ,_diffThySignature=(L.get diffThySignature thy)

lib/theory/src/Items/TheoryItem.hs

@@ -36,6 +36,9 @@ import Items.ExportInfo
 
 type FormalComment = (String, String)
 
+-- | A configuration block.
+type ConfigBlock = String
+
 -- | TranslationItems can be processes, accountability lemmas, and case tests
 data TranslationElement =
         ProcessItem PlainProcess
@@ -55,6 +58,7 @@ data TheoryItem r p s =
      | LemmaItem (Lemma p)
      | RestrictionItem Restriction
      | TextItem FormalComment
+     | ConfigBlockItem ConfigBlock
      | PredicateItem Predicate
      | MacroItem [Macro]
      | TranslationItem s
@@ -75,6 +79,7 @@ data DiffTheoryItem r r2 p p2 =
      | EitherRestrictionItem (Side, Restriction)
      | DiffMacroItem [Macro]
      | DiffTextItem FormalComment
+     | DiffConfigBlockItem ConfigBlock
      deriving( Show, Eq, Ord, Functor, Generic, NFData, Binary )