Merge pull request #69 from kframework/hyperproperties-4

Another Hyperproperties stuff

prover/build

@@ -29,6 +29,7 @@ other_md_files = [ 'lang/smt-lang.md'
                  , 'strategies/duplicate.md'
                  , 'strategies/instantiate-universals.md'
                  , 'strategies/inst-exists.md'
+                 , 'strategies/introduce-lemma.md'
                  , 'strategies/intros.md'
                  , 'strategies/knaster-tarski.md'
                  , 'strategies/matching.md'

prover/drivers/base.md

@@ -67,6 +67,7 @@ module DRIVER-BASE
   imports STRATEGY-DUPLICATE
   imports STRATEGY-INSTANTIATE-UNIVERSALS
   imports STRATEGY-INST-EXISTS
+  imports STRATEGY-INTRODUCE-LEMMA
   imports STRATEGY-INTROS
   imports STRATEGY-SMT
   imports STRATEGY-SEARCH-BOUND

prover/lang/kore-lang.md

@@ -549,6 +549,7 @@ where the term being unfolded has been replace by `#hole`.
   rule subst(X:Variable,Y:Variable,V) => X    requires X =/=K Y
   rule subst(X:SetVariable,Y:SetVariable,V) => X requires X =/=K Y
   rule subst(X:Variable,P:Pattern, V) => X    requires notBool(isVariable(P) orBool isVariableName(P))
+  rule subst(X:SetVariable,P:Pattern, V) => X requires notBool isSetVariable(P)
   rule subst(I:Int, X, V) => I
   rule subst(\top(),_,_)=> \top()
   rule subst(\bottom(),_,_) => \bottom()

prover/prover.md

@@ -9,6 +9,7 @@ requires "strategies/core.k"
 requires "strategies/duplicate.k"
 requires "strategies/instantiate-universals.k"
 requires "strategies/inst-exists.k"
+requires "strategies/introduce-lemma.k"
 requires "strategies/intros.k"
 requires "strategies/knaster-tarski.k"
 requires "strategies/matching.k"
@@ -89,6 +90,9 @@ module STRATEGIES-EXPORTED-SYNTAX
                     | "propagate-exists-through-application" Int
                     | "propagate-predicate-through-application" "(" Pattern "," Int ")"
                     | "propagate-conjunct-through-exists" "(" Int "," Int ")"
+                    | "introduce-lemma" "(" AxiomName ":" Pattern "," "by:" Strategy ")"
+                    | "axiom-equals-top" "(" AxiomName ")"
+                    | "simplify.flatten-ands"
 
   syntax RewriteDirection ::= "->" | "<-"
 

prover/strategies/apply-equation.md

@@ -113,6 +113,7 @@ module STRATEGY-APPLY-EQUATION
                       ( term: T
                       , pattern: L
                       , variables: getUniversallyQuantifiedVariables(H)
+                                   ++Patterns getSetVariables(H)
                       , index: Idx
                       )
         , to: R
@@ -137,7 +138,7 @@ module STRATEGY-APPLY-EQUATION
          , by: Ss
          )
          => instantiateAssumptions(GId, Subst, P)
-         ~> createSubgoalsWithStrategies(strats: Ss, result: noop)
+         ~> createSubgoalsWithStrategies(strats: Ss, result: success)
        ...</k>
        <claim>
          _ => cool(heated: Heated, term: substMap(R, Subst))
@@ -149,17 +150,17 @@ module STRATEGY-APPLY-EQUATION
                    "," "result:" Strategy
                    ")"
 
-  rule <k> (#instantiateAssumptionsResult(.Patterns, .Map)
+  rule <k> (#instantiateAssumptionsResult(.Patterns, _)
                ~> createSubgoalsWithStrategies
                   ( strats: .Strategies
                   , result: R))
-               => R
+               => R & noop
        ...</k>
 
-  rule <k> #instantiateAssumptionsResult(P,Ps => Ps, .Map)
+  rule <k> #instantiateAssumptionsResult(P,Ps => Ps, _)
                ~> createSubgoalsWithStrategies
                   ( strats: (S, Ss) => Ss
-                  , result: R => R & subgoal(P, S))
+                  , result: R => subgoal(P, S) & R)
        ...</k>
 
 ```

prover/strategies/apply.md

@@ -32,6 +32,7 @@ module STRATEGY-APPLY
                  terms: G, .Patterns,
                  patterns: getConclusion(A), .Patterns,
                  variables: getUniversallyQuantifiedVariables(A)
+                           ++Patterns getSetVariables(A)
                ),
                Strat
              )
@@ -56,13 +57,13 @@ module STRATEGY-APPLY
                      Strategy, Strategy)
 
   rule <k>
-         #apply2(#instantiateAssumptionsResult(.Patterns, .Map), _, Result)
+         #apply2(#instantiateAssumptionsResult(.Patterns, _), _, Result)
          => Result
        ...</k>
 
   rule <k>
          #apply2(
-           #instantiateAssumptionsResult(P, Ps => Ps, .Map),
+           #instantiateAssumptionsResult(P, Ps => Ps, _),
            Strat,
            Result => Result & subgoal(P, Strat)
          )

prover/strategies/introduce-lemma.md

@@ -0,0 +1,40 @@
+# introduce-lemma
+
+```
+Gamma |- Phi    Gamma U {Phi} |- Psi
+------------------------------------
+Gamma |- Psi
+```
+
+```k
+
+module STRATEGY-INTRODUCE-LEMMA
+  imports PROVER-CORE
+  imports STRATEGIES-EXPORTED-SYNTAX
+
+  rule <k> introduce-lemma(Name : Phi, by: Strat)
+        => subgoal(Name, Phi, Strat)
+        ~> #introduceLemma(Name, Phi)
+           ...
+       </k>
+       <id> GId </id>
+       requires notBool AxiomNameToString(Name) in collectLocalAxiomNames(GId)
+
+  rule <k> (.K => "Name already used!" )
+        ~> introduce-lemma(Name : _, by: _)
+           ...
+       </k>
+       <id> GId </id>
+       requires AxiomNameToString(Name) in collectLocalAxiomNames(GId)
+
+  syntax KItem ::= #introduceLemma(AxiomName, Pattern)
+
+  rule <k> (success ~> #introduceLemma(Name, Phi)) => noop ...</k>
+       <local-context> (.Bag =>
+         <local-decl> axiom Name : Phi </local-decl>
+         ) ...
+       </local-context>
+
+
+endmodule
+```

prover/strategies/reflexivity.md

@@ -4,13 +4,41 @@ module STRATEGY-REFLEXIVITY
   imports PROVER-CORE
   imports STRATEGIES-EXPORTED-SYNTAX
 
+```
+# Reflexivity
+
+```
+      .
+--------------
+Gamma |- X = X
+```
+
+```k
   rule <k> reflexivity => success ...</k>
        <claim> \equals(P, P) </claim>
 
   rule <k> reflexivity => fail ...</k>
        <claim> \equals(P, Q) </claim>
        requires P =/=K Q
+```
+# axiom-equals-top
+
+```
+         .
+--------------------
+Gamma, P |- P = \top
+```
+
+```k
+
+  rule <k> (.K => loadNamed(Name))
+        ~> axiom-equals-top(Name)
+           ...
+       </k>
 
+  // currently, `\top()` desugares to `\and()`
+  rule <k> P ~> axiom-equals-top(_) => success ...</k>
+       <claim> \equals(P, \and(.Patterns) #Or \top()) </claim>
 
 endmodule // STRATEGY-REFLEXIVITY
 ```

prover/strategies/simplification.md

@@ -6,6 +6,8 @@ module STRATEGY-SIMPLIFICATION
   imports STRATEGIES-EXPORTED-SYNTAX
   imports KORE-HELPERS
   imports SYNTACTIC-MATCH-SYNTAX
+  imports VISITOR-SYNTAX
+
 
 ```
 
@@ -307,6 +309,24 @@ Lift `\or`s on the left hand sides of implications
        <k> simplify => noop ... </k>
 ```
 
+#### Simplify ands
+
+```k
+
+  rule <k> simplify.flatten-ands => noop ...</k>
+       <claim> P => visitorResult.getPattern(visitTopDown(flattenAndsVisitor(), P)) </claim>
+
+  syntax Visitor ::= flattenAndsVisitor()
+
+  rule visit(flattenAndsVisitor(), P)
+    => visitorResult(flattenAndsVisitor(), P)
+    requires \and(...) :/=K P
+
+  rule visit(flattenAndsVisitor(), \and(Ps))
+    => visitorResult(flattenAndsVisitor(), maybeAnd(#flattenAnds(Ps)))
+
+```
+
 ### Instantiate Existials
 
 ```

prover/t/axiom-equals-top.kore

@@ -0,0 +1,4 @@
+symbol f() : Int
+axiom a: \equals(f(), 1)
+claim \equals(\equals(f(), 1), \top())
+strategy axiom-equals-top(a)

prover/t/axiom-equals-top.kore.expected

@@ -0,0 +1,32 @@
+<prover>
+  <exit-code>
+    0
+  </exit-code>
+  <goals>
+    <goal>
+      id: ., parent: .
+      <claim>
+        \and ( .Patterns )
+      </claim>
+      <k>
+        .
+      </k>n<expected>
+        .
+      </expected>
+      <local-context>
+        .LocalDeclCellSet
+      </local-context>
+    <trace>
+      .
+    </trace>
+  </goals>
+  <declarations>
+    <declaration>
+      axiom a : \equals ( f ( .Patterns ) , 1 )
+    </declaration> <declaration>
+      axiom ax0 : \equals ( \equals ( f ( .Patterns ) , 1 ) , \and ( .Patterns ) )
+    </declaration> <declaration>
+      symbol f ( .Sorts ) : Int
+    </declaration>
+  </declarations>
+</prover>

prover/t/introduce-lemma.kore

@@ -0,0 +1,3 @@
+claim \equals(1, 1)
+strategy introduce-lemma(H: \equals(1,1), by: reflexivity)
+       . apply(H, fail)

prover/t/introduce-lemma.kore.expected

@@ -0,0 +1,28 @@
+<prover>
+  <exit-code>
+    0
+  </exit-code>
+  <goals>
+    <goal>
+      id: ., parent: .
+      <claim>
+        \and ( .Patterns )
+      </claim>
+      <k>
+        .
+      </k>n<expected>
+        .
+      </expected>
+      <local-context>
+        .LocalDeclCellSet
+      </local-context>
+    <trace>
+      .
+    </trace>
+  </goals>
+  <declarations>
+    <declaration>
+      axiom ax0 : \equals ( 1 , 1 )
+    </declaration>
+  </declarations>
+</prover>

prover/t/simplify-flatten-ands.kore

@@ -0,0 +1,6 @@
+symbol f(Int) : Int
+axiom a: \equals(f(1), 1)
+claim \equals(f(\and(1, \and())), 1)
+strategy simplify.flatten-ands
+       . apply-equation -> a at 0 by []
+       . reflexivity

prover/t/simplify-flatten-ands.kore.expected

@@ -0,0 +1,32 @@
+<prover>
+  <exit-code>
+    0
+  </exit-code>
+  <goals>
+    <goal>
+      id: ., parent: .
+      <claim>
+        \and ( .Patterns )
+      </claim>
+      <k>
+        .
+      </k>n<expected>
+        .
+      </expected>
+      <local-context>
+        .LocalDeclCellSet
+      </local-context>
+    <trace>
+      .
+    </trace>
+  </goals>
+  <declarations>
+    <declaration>
+      axiom a : \equals ( f ( 1 , .Patterns ) , 1 )
+    </declaration> <declaration>
+      axiom ax0 : \equals ( f ( \and ( 1 , \and ( .Patterns ) , .Patterns ) , .Patterns ) , 1 )
+    </declaration> <declaration>
+      symbol f ( Int , .Sorts ) : Int
+    </declaration>
+  </declarations>
+</prover>

prover/utils/syntactic-match.md

@@ -224,6 +224,42 @@ module SYNTACTIC-MATCH-RULES
     => #error("\\equals(_,_) does not match")
     requires \equals(...) :/=K T
 
+  // \member(_,_) matched
+  rule #syntacticMatch( terms:     \member(T1, T2), Ts
+                               => T1 ++Patterns T2 ++Patterns Ts
+                      , patterns:  \member(P1, P2), Ps
+                               => P1 ++Patterns P2 ++Patterns Ps
+                      , variables: _
+                      , subst:     _
+                      )
+
+  // \member(_,_) mismatched
+  rule #syntacticMatch( terms:     T, _
+                      , patterns:  \member(...), _
+                      , variables: _
+                      , subst:     _
+                      )
+    => #error("\\member(_,_) does not match")
+    requires \member(...) :/=K T
+
+  // \subseteq(_,_) matched
+  rule #syntacticMatch( terms:     \subseteq(T1, T2), Ts
+                               => T1 ++Patterns T2 ++Patterns Ts
+                      , patterns:  \subseteq(P1, P2), Ps
+                               => P1 ++Patterns P2 ++Patterns Ps
+                      , variables: _
+                      , subst:     _
+                      )
+
+  // \subseteq(_,_) mismatched
+  rule #syntacticMatch( terms:     T, _
+                      , patterns:  \subseteq(...), _
+                      , variables: _
+                      , subst:     _
+                      )
+    => #error("\\subseteq(_,_) does not match")
+    requires \subseteq(...) :/=K T
+
   // \not(_) matched
   rule #syntacticMatch( terms:     \not(T), Ts
                                => T ++Patterns Ts

prover/utils/visitor.md

@@ -229,6 +229,16 @@ module VISITOR
   rule #visitTopDownTypeof1(visitorResult(V, P1), S)
     => visitorResult(V, \typeof(P1, S))
 
+  // \functionalPattern(_)
+  syntax VisitorResult
+         ::= #visitTopDownFunctionalPattern(VisitorResult) [function]
+
+  rule #visitTopDown(visitorResult(V, \functionalPattern(P)))
+    => #visitTopDownFunctionalPattern(visitTopDown(V, P))
+
+  rule #visitTopDownFunctionalPattern(visitorResult(V, P))
+    => visitorResult(V, \functionalPattern(P))
+
   rule visitorResult.getPattern(visitorResult(_, P)) => P
 
 ```