diff --git a/examples/CountDown.tla b/examples/CountDown.tla new file mode 100644 index 00000000..6b8613bf --- /dev/null +++ b/examples/CountDown.tla @@ -0,0 +1,106 @@ +----------------------------- MODULE CountDown ----------------------------- +(***************************************************************************) +(* Example of a counter that counts down from N to 0, together with a *) +(* liveness proof showing that it will eventually reach 0. *) +(* *) +(* Contributed by Andreas Recke. *) +(***************************************************************************) +EXTENDS Naturals, TLC, TLAPS, NaturalsInduction + +---- +\* Input: N is the starting number for the countdown +CONSTANTS N + +\* N must be a natural number +ASSUME NAssumption == N \in Nat + +\* Variable i is the running countdown value +VARIABLES cnt + +---- +\* We define a set S which contains all possible values of the countdown counter +S == 0..N + +---- +\* Init: i starts at N +Init == cnt = N + +\* Next: if cnt is greater than 0, it will be count down by 1 in the next step +Next == cnt > 0 /\ cnt' = cnt-1 + +\* The complete spec. Important here is the fairness property. Otherwise, we +\* would not be able to proof that the count down may reach zero, because it +\* may infinitely stutter at a value larger than zero. +Spec == Init /\ [][Next]_cnt /\ WF_cnt(Next) + +---- +\* Properties of the algorithm +Termination == <>(cnt=0) \* count down reaches zero + +NextEnabled == cnt > 0 \* for rewriting the ENABLED property to something simpler + +TypeInv == cnt \in S + \* the type correctness property is actually fundamental. + \* TLA+ values do not have a type, but proofs require it + +---- +\* Theorems + +\* this lemma ensures that the type of cnt is always correct +LEMMA TypeCorrectness == Spec => []TypeInv +\* From the correct input, ensured by NAssumption, Init leads to a correct type +<1>1. Init => TypeInv + BY NAssumption DEF Init, TypeInv, S +\* The Next transition, here encoded with the "[Next]_cnt" construct, leaves the +\* TypeInv unchanged in the next state +<1>2. TypeInv /\ [Next]_cnt => TypeInv' + BY NAssumption DEF TypeInv, Next, S +<1>3. QED + BY <1>1, <1>2, PTL DEF Spec \* standard invariant reasoning + +---- +\* If the input constant N \in Nat, then we can prove that Spec leads to Termination (cnt=0) +\* We use the DownwardNatInduction rule which actually has the same goal as our algorithm: +\* start with a number N and prove that if fulfills a requirement P(N), i.e. <>cnt=N +\* Then just prove that for each n \in 1..N, where P(n) is fulfilled, the requirement P(n-1) +\* is fulfilled, i.e. <>cnt=(n-1) +\* This then proves, if cnt can be in 0..N that P(0) will be reached, i.e. <>cnt=0; which +\* equals Termination +THEOREM WillReachZero == Spec => Termination +PROOF +\* The liveness proof uses an intermediate predicate for downward induction +\* Note that P(0) just expresses the assertion of the theorem. +<1> DEFINE P(m) == Spec => <>(cnt = m) +<1> HIDE DEF P +<1>2. P(0) + <2>1. P(N) +\* Start condition - this is actually obvious. We show that initialization fulfills the first goal + BY PTL DEF P, Spec, Init + <2>2. \A n \in 1..N : P(n) => P(n-1) +\* prove: for all intermediate goals, the next goal will be reached + <3>1. SUFFICES + ASSUME NEW n \in 1 .. N + PROVE Spec /\ <>(cnt = n) => <>(cnt = n-1) +\* Reformulation replacing the quantifier by a constant +\* Note that `Spec' remains in the conclusion so that PTL finds only "boxed" hypotheses in the QED step + BY DEF P + <3>2. (cnt=n) /\ [Next]_cnt => (cnt=n)' \/ (cnt=n-1)' + BY DEF Next +\* WF1 rule, step 1 + <3>3. (cnt=n) /\ <>_cnt => (cnt=n-1)' + BY DEF Next +\* WF1 rule, step 2 + <3>4. (cnt=n) => ENABLED <>_cnt + BY ExpandENABLED DEF Next +\* WF1 rule, step 3 + <3> QED + BY <3>1, <3>2, <3>3, <3>4, PTL DEF Spec +\* Now we can conclude the WF1 rule reasoning + <2> QED + BY NAssumption, <2>1, <2>2, DownwardNatInduction, Isa +\* taking the facts <2>1 and <2>2, downward natural induction works +<1> QED + BY <1>2, PTL DEF P, Termination +\* and finally, we can prove the overall goal to show that the spec/algorithm terminates + +============================================================================= diff --git a/examples/EWD840.tla b/examples/EWD840.tla index 8647e3ac..778fafee 100644 --- a/examples/EWD840.tla +++ b/examples/EWD840.tla @@ -1,5 +1,5 @@ ------------------------------- MODULE EWD840 ------------------------------- -EXTENDS Naturals, TLAPS +EXTENDS Naturals, NaturalsInduction, TLAPS CONSTANT N ASSUME NAssumption == N \in Nat \ {0} @@ -96,18 +96,20 @@ NeverChangeColor == [][ \A i \in Nodes : UNCHANGED color[i] ]_vars (* Main safety property: if there is a white token at node 0 then every *) (* node is inactive. *) (***************************************************************************) +allInactive == \A i \in Nodes : ~ active[i] + terminationDetected == /\ tpos = 0 /\ tcolor = "white" /\ color[0] = "white" /\ ~ active[0] TerminationDetection == - terminationDetected => \A i \in Nodes : ~ active[i] + terminationDetected => allInactive (***************************************************************************) (* Liveness property: termination is eventually detected. *) (***************************************************************************) Liveness == - (\A i \in Nodes : ~ active[i]) ~> terminationDetected + allInactive ~> terminationDetected (***************************************************************************) (* The following property says that eventually all nodes will terminate *) @@ -119,26 +121,27 @@ AllNodesTerminateIfNoMessages == <>[][~ \E i \in Nodes : SendMsg(i)]_vars => <>(\A i \in Nodes : ~ active[i]) +----------------------------------------------------------------------------- (***************************************************************************) -(* Dijkstra's invariant *) +(* The formal proof of the safety property, based on Dijkstra's invariant. *) (***************************************************************************) Inv == \/ P0:: \A i \in Nodes : tpos < i => ~ active[i] \/ P1:: \E j \in 0 .. tpos : color[j] = "black" \/ P2:: tcolor = "black" ------------------------------------------------------------------------------ +USE NAssumption (* TypeOK is an inductive invariant *) -LEMMA TypeOK_inv == Spec => []TypeOK -<1>. USE NAssumption DEF TypeOK, Nodes, Color +LEMMA TypeCorrect == Spec => []TypeOK +<1>. USE DEF TypeOK, Nodes, Color <1>1. Init => TypeOK BY DEF Init <1>2. TypeOK /\ [Next]_vars => TypeOK' (* FIXME: Although each of the steps below is proved instantly, the attempt to prove the assertion all at once fails?? - BY NAssumption DEF Next, vars, TypeOK, Nodes, Color, Controlled, Environment, - InitiateProbe, PassToken, SendMsg, Deactivate + BY DEF Next, vars, Controlled, Environment, InitiateProbe, + PassToken, SendMsg, Deactivate *) <2> SUFFICES ASSUME TypeOK, [Next]_vars @@ -168,24 +171,17 @@ LEMMA TypeOK_inv == Spec => []TypeOK THEOREM Spec => []TerminationDetection -<1> USE NAssumption (* Type information about the constants will be needed ! *) - (* Dijkstra's invariant implies correctness *) <1>1 Inv => TerminationDetection - BY DEF Inv, TerminationDetection, terminationDetected, Nodes - + BY DEF Inv, TerminationDetection, terminationDetected, Nodes, allInactive (* Dijkstra's invariant is (trivially) established by the initial condition *) <1>2 Init => Inv BY DEF Init, Inv - (* Dijkstra's invariant is inductive relative to the type invariant *) <1>3 TypeOK /\ Inv /\ [Next]_vars => Inv' BY DEF Inv, TypeOK, Next, vars, Controlled, Environment, InitiateProbe, PassToken, SendMsg, Deactivate, Nodes, Color - -<1> QED - BY <1>1, <1>2, <1>3, TypeOK_inv, PTL DEF Spec - +<1> QED BY <1>1, <1>2, <1>3, TypeCorrect, PTL DEF Spec (* If the one-line proof of step <1>1 above is too obscure, @@ -211,18 +207,249 @@ LEMMA Inv_implies_Termination == Inv => TerminationDetection <2>4. CASE i = 0 BY <2>4, <1>1 <2>5. CASE i \in 1 .. N-1 - <3>1. tpos < i BY tpos=0, <2>5, NAssumption + <3>1. tpos < i BY tpos=0, <2>5 <3>. QED BY <3>1, <2>3 <2>. QED BY <2>4, <2>5 DEF Nodes <1>. QED - BY <1>1 DEF TerminationDetection, terminationDetected + BY <1>1 DEF TerminationDetection, terminationDetected, allInactive + +----------------------------------------------------------------------------- +(***************************************************************************) +(* The liveness proof. *) +(* We have to show that after all nodes have terminated, node 0 will *) +(* eventually detect termination. In order for this to happen, the token *) +(* will have to perform up to 3 rounds of the ring. The first round simply *) +(* takes it back to node 0, the second round paints all nodes white, *) +(* while the token may be black, and the third round verifies that all *) +(* nodes are still white, so the token returns white. *) +(* The proof becomes a little simpler if we set it up as a proof by *) +(* contradiction and assume that termination will never be declared. *) +(* In particular, node 0 will then always pass on the token. *) +(* The formula BSpec gathers all boxed formulas used in the proof. *) +(***************************************************************************) +BSpec == /\ []TypeOK + /\ [](~terminationDetected) + /\ [][Next]_vars + /\ WF_vars(Controlled) + +(***************************************************************************) +(* We first establish the enabledness conditions of the action for which *) +(* fairness is asserted. *) +(***************************************************************************) + +ControlledEnabled == +\/ /\ tpos = 0 + /\ tcolor = "black" \/ color[0] = "black" +\/ \E i \in Nodes \ {0} : + /\ tpos = i + /\ ~ active[i] \/ color[i] = "black" \/ tcolor = "black" + +LEMMA EnabledControlled == + ASSUME TypeOK + PROVE ENABLED <>_vars <=> ControlledEnabled +<1>1. InitiateProbe <=> <>_vars + BY DEF InitiateProbe, vars, TypeOK +<1>2. \A i \in Nodes \ {0} : PassToken(i) <=> <>_vars + <2>. SUFFICES ASSUME NEW i \in Nodes \ {0} + PROVE PassToken(i) => <>_vars + OBVIOUS + <2>. QED + BY DEF PassToken, vars, TypeOK, Nodes +<1>3. Controlled <=> <>_vars + BY <1>1, <1>2 DEF Controlled +<1>4. (ENABLED Controlled) <=> ENABLED <>_vars + BY <1>3, ENABLEDrules +<1>5. ENABLED Controlled + <=> \/ ENABLED InitiateProbe + \/ \E i \in Nodes \ {0} : ENABLED PassToken(i) + <2>1. Controlled <=> + InitiateProbe \/ (\E i \in Nodes \ {0} : PassToken(i)) + BY DEF Controlled + <2>2. (ENABLED Controlled) <=> + ENABLED (InitiateProbe \/ (\E i \in Nodes \ {0} : PassToken(i))) + BY <2>1, ENABLEDrules + <2>3. ENABLED (InitiateProbe \/ (\E i \in Nodes \ {0} : PassToken(i))) + <=> ENABLED InitiateProbe + \/ ENABLED \E i \in Nodes \ {0} : PassToken(i) + BY ENABLEDaxioms + <2>4. (ENABLED \E i \in Nodes \ {0} : PassToken(i)) + <=> \E i \in Nodes \ {0} : ENABLED PassToken(i) + BY ENABLEDaxioms + <2>. QED + BY <2>2, <2>3, <2>4 +<1>6. ControlledEnabled!1 <=> ENABLED InitiateProbe + BY ExpandENABLED, Zenon DEF InitiateProbe, TypeOK +<1>7. \A i \in Nodes \ {0} : ControlledEnabled!2!(i) <=> ENABLED PassToken(i) + BY ExpandENABLED, Zenon DEF PassToken, TypeOK +<1>. QED + BY <1>4, <1>5, <1>6,<1>7 DEF ControlledEnabled +(***************************************************************************) +(* If all nodes are inactive, the token must eventually arrive at node 0. *) +(***************************************************************************) +LEMMA TerminationRound1 == + BSpec => (allInactive ~> (allInactive /\ tpos = 0)) +<1>. DEFINE P(n) == allInactive /\ n \in Nodes /\ tpos = n + Q == P(0) + R(n) == BSpec => [](P(n) => <>Q) +<1>1. \A n \in Nat : R(n) + <2>1. R(0) + BY PTL + <2>2. ASSUME NEW n \in Nat + PROVE R(n) => R(n+1) + <3>. DEFINE Pn == P(n) Pn1 == P(n+1) + <3>. USE DEF TypeOK, allInactive, Nodes + <3>1. TypeOK /\ Pn1 /\ [Next]_vars => Pn1' \/ Pn' + BY DEF Next, vars, Controlled, Environment, InitiateProbe, PassToken, Deactivate, SendMsg + <3>2. TypeOK /\ Pn1 /\ <>_vars => Pn' + BY DEF Controlled, InitiateProbe, PassToken, vars + <3>3. TypeOK /\ Pn1 => ENABLED <>_vars + BY EnabledControlled DEF ControlledEnabled + <3>. HIDE DEF Pn1 + <3>4. R(n) => (BSpec => [](Pn1 => <>Q)) + BY <3>1, <3>2, <3>3, PTL DEF BSpec + <3>. QED BY <3>4 DEF Pn1 + <2>. HIDE DEF R + <2>. QED BY <2>1, <2>2, NatInduction +<1>2. BSpec => []((\E n \in Nat : P(n)) => <>Q) + <2>. HIDE DEF P, Q + <2>1. BSpec => [](\A n \in Nat : P(n) => <>Q) + BY <1>1 + <2>2. (\A n \in Nat : P(n) => <>Q) <=> ((\E n \in Nat : P(n)) => <>Q) + OBVIOUS + <2>. QED BY <2>1, <2>2, PTL +<1>3. TypeOK => (allInactive => \E n \in Nat : P(n)) + BY DEF allInactive, TypeOK, Nodes +<1>. QED BY <1>2, <1>3, TypeCorrect, PTL DEF BSpec + +(***************************************************************************) +(* Moreover, if all nodes are inactive and the token is at node 0 but *) +(* termination cannot be detected, it will eventually return to node 0 *) +(* in a state where all nodes are white. *) +(***************************************************************************) +allWhite == \A i \in Nodes : color[i] = "white" + +LEMMA TerminationRound2 == + BSpec => ((allInactive /\ tpos = 0) + ~> (allInactive /\ tpos = 0 /\ allWhite)) +<1>. DEFINE P(n) == /\ allInactive /\ n \in Nodes /\ tpos = n + /\ color[0] = "white" + /\ \A m \in n+1 .. N-1 : color[m] = "white" + Q == P(0) + R(n) == BSpec => [](P(n) => <>Q) +<1>1. BSpec => ((allInactive /\ tpos = 0) ~> \E n \in Nat : P(n)) + <2>. DEFINE S == allInactive /\ tpos = 0 + T == P(N-1) + <2>. USE DEF TypeOK, allInactive, Nodes + <2>1. TypeOK /\ S /\ [Next]_vars => S' \/ T' + BY DEF Next, vars, Controlled, Environment, InitiateProbe, PassToken, Deactivate, SendMsg + <2>2. TypeOK /\ S /\ <>_vars => T' + BY DEF Controlled, InitiateProbe, PassToken, vars + <2>3. TypeOK /\ ~terminationDetected /\ S => ENABLED <>_vars + BY EnabledControlled DEF ControlledEnabled, terminationDetected, Color + <2>4. T => \E n \in Nat : P(n) + OBVIOUS + <2>. HIDE DEF T + <2>5. QED BY <2>1, <2>2, <2>3, <2>4, PTL DEF BSpec +<1>2. \A n \in Nat : R(n) + <2>1. R(0) + BY PTL + <2>2. ASSUME NEW n \in Nat + PROVE R(n) => R(n+1) + <3>. DEFINE Pn == P(n) Pn1 == P(n+1) + <3>. USE DEF TypeOK, allInactive, Nodes + <3>1. TypeOK /\ Pn1 /\ [Next]_vars => Pn1' \/ Pn' + BY DEF Next, vars, Controlled, Environment, InitiateProbe, PassToken, Deactivate, SendMsg + <3>2. TypeOK /\ Pn1 /\ <>_vars => Pn' + BY DEF Controlled, InitiateProbe, PassToken, vars + <3>3. TypeOK /\ Pn1 => ENABLED <>_vars + BY EnabledControlled DEF ControlledEnabled + <3>. HIDE DEF Pn1 + <3>4. R(n) => (BSpec => [](Pn1 => <>Q)) + BY <3>1, <3>2, <3>3, PTL DEF BSpec + <3>. QED BY <3>4 DEF Pn1 + <2>. HIDE DEF R + <2>. QED BY <2>1, <2>2, NatInduction +<1>3. BSpec => []((\E n \in Nat : P(n)) => <>Q) + <2>. HIDE DEF P, Q + <2>1. BSpec => [](\A n \in Nat : P(n) => <>Q) + BY <1>2 + <2>2. (\A n \in Nat : P(n) => <>Q) <=> ((\E n \in Nat : P(n)) => <>Q) + OBVIOUS + <2>. QED BY <2>1, <2>2, PTL +<1>4. Q => allInactive /\ tpos = 0 /\ allWhite + BY DEF allWhite, Nodes +<1>. QED BY <1>1, <1>3, <1>4, PTL + +(***************************************************************************) +(* Finally, if all nodes are inactive and white, and the token is at *) +(* node 0, eventually a white token will be at node 0 while all nodes are *) +(* still white. *) +(***************************************************************************) +LEMMA TerminationRound3 == + BSpec => (allInactive /\ tpos = 0 /\ allWhite) ~> terminationDetected +<1>. DEFINE P(n) == /\ allInactive /\ n \in Nodes /\ tpos = n + /\ allWhite /\ tcolor = "white" + Q == P(0) + R(n) == BSpec => [](P(n) => <>Q) +<1>1. BSpec => ((allInactive /\ tpos = 0 /\ allWhite) ~> \E n \in Nat : P(n)) + <2>. DEFINE S == allInactive /\ tpos = 0 /\ allWhite + T == P(N-1) + <2>. USE DEF TypeOK, allInactive, Nodes, allWhite + <2>1. TypeOK /\ S /\ [Next]_vars => S' \/ T' + BY DEF Next, vars, Controlled, Environment, InitiateProbe, PassToken, Deactivate, SendMsg + <2>2. TypeOK /\ S /\ <>_vars => T' + BY DEF Controlled, InitiateProbe, PassToken, vars + <2>3. TypeOK /\ ~terminationDetected /\ S => ENABLED <>_vars + BY EnabledControlled DEF ControlledEnabled, terminationDetected, Color + <2>4. T => \E n \in Nat : P(n) + OBVIOUS + <2>. HIDE DEF T + <2>5. QED BY <2>1, <2>2, <2>3, <2>4, PTL DEF BSpec +<1>2. \A n \in Nat : R(n) + <2>1. R(0) + BY PTL + <2>2. ASSUME NEW n \in Nat + PROVE R(n) => R(n+1) + <3>. DEFINE Pn == P(n) Pn1 == P(n+1) + <3>. USE DEF TypeOK, allInactive, Nodes, allWhite + <3>1. TypeOK /\ Pn1 /\ [Next]_vars => Pn1' \/ Pn' + BY DEF Next, vars, Controlled, Environment, InitiateProbe, PassToken, Deactivate, SendMsg + <3>2. TypeOK /\ Pn1 /\ <>_vars => Pn' + BY DEF Controlled, InitiateProbe, PassToken, vars + <3>3. TypeOK /\ Pn1 => ENABLED <>_vars + BY EnabledControlled DEF ControlledEnabled + <3>. HIDE DEF Pn1 + <3>4. R(n) => (BSpec => [](Pn1 => <>Q)) + BY <3>1, <3>2, <3>3, PTL DEF BSpec + <3>. QED BY <3>4 DEF Pn1 + <2>. HIDE DEF R + <2>. QED BY <2>1, <2>2, NatInduction +<1>3. BSpec => []((\E n \in Nat : P(n)) => <>Q) + <2>. HIDE DEF P, Q + <2>1. BSpec => [](\A n \in Nat : P(n) => <>Q) + BY <1>2 + <2>2. (\A n \in Nat : P(n) => <>Q) <=> ((\E n \in Nat : P(n)) => <>Q) + OBVIOUS + <2>. QED BY <2>1, <2>2, PTL +<1>4. Q => terminationDetected + BY DEF allInactive, allWhite, terminationDetected, Nodes +<1>. QED BY <1>1, <1>3, <1>4, PTL + + +(***************************************************************************) +(* The liveness property follows from the above lemmas by simple temporal *) +(* reasoning. *) +(***************************************************************************) +THEOREM Live == Spec => Liveness +BY TypeCorrect, TerminationRound1, TerminationRound2, TerminationRound3, PTL + DEF Spec, Fairness, BSpec, Liveness ============================================================================= \* Modification History -\* Last modified Wed Jan 08 15:06:01 CET 2020 by merz +\* Last modified Tue Feb 09 09:57:46 CET 2021 by merz \* Last modified Fri May 30 23:04:12 CEST 2014 by shaolin \* Last modified Wed May 21 11:36:56 CEST 2014 by jael \* Created Mon Sep 09 11:33:10 CEST 2013 by merz diff --git a/examples/Peterson.tla b/examples/Peterson.tla index 4b4f6012..fa62c5f4 100644 --- a/examples/Peterson.tla +++ b/examples/Peterson.tla @@ -92,7 +92,7 @@ MutualExclusion == ~(pc[0] = "cs" /\ pc[1] = "cs") NeverCS == pc[0] # "cs" -Wait(i) == (pc[0] = "a3a") \/ (pc[0] = "a3b") +Wait(i) == (pc[i] = "a3a") \/ (pc[i] = "a3b") CS(i) == pc[i] = "cs" Fairness == WF_vars(proc(0)) /\ WF_vars(proc(1)) FairSpec == Spec /\ Fairness diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index 04a0d3da..9ae782dc 100644 --- a/examples/SimpleEventually.tla +++ b/examples/SimpleEventually.tla @@ -26,7 +26,7 @@ THEOREM System => <>(x = TRUE) BY <2>1, <2>2, PTL <1>3. ASSUME TypeOK /\ ~(x = TRUE) PROVE ENABLED <>_x - BY <1>3, ExpandENABLED DEF Next + BY <1>3, ExpandENABLED DEF Next, TypeOK <1>4. ASSUME <>_x PROVE (x = TRUE)' BY <1>4 DEF Next diff --git a/examples/SimpleMutex.tla b/examples/SimpleMutex.tla index 653f7c48..6296050a 100644 --- a/examples/SimpleMutex.tla +++ b/examples/SimpleMutex.tla @@ -113,7 +113,7 @@ THEOREM Invariance == TypeOK /\ Inv /\ Next => TypeOK' /\ Inv' /\ 1-j \in {0, 1} /\ i # j => /\ 1-i = j /\ 1-j = i - BY IsaM("auto") + OBVIOUS <2>2. USE DEF TypeOK, Inv <2>3. CASE a(i) BY <2>1, <1>3, <2>3 DEF a diff --git a/library/TLAPS.tla b/library/TLAPS.tla index c250a674..59f41cf0 100644 --- a/library/TLAPS.tla +++ b/library/TLAPS.tla @@ -339,12 +339,22 @@ AllIsaT(X) == TRUE (*{ (* which is a form before introducing rigid quantifiers. *) (* The pragma Lambdify is sound for occurrences of ENABLED and \cdot *) (* that are not nested. *) +(* *) +(* The pragma ENABLEDaxioms invokes axioms about the operator ENABLED. *) +(* *) +(* The pragma ENABLEDrules invokes two proof rules about the operator *) +(* ENABLED. *) +(* *) +(* The pragma LevelComparison allows proofs that change only the levels *) +(* of declared operators, or rename declared operators. *) (**************************************************************************) ExpandENABLED == TRUE (*{ by (prover:"expandenabled") }*) ExpandCdot == TRUE (*{ by (prover:"expandcdot") }*) AutoUSE == TRUE (*{ by (prover:"autouse") }*) Lambdify == TRUE (*{ by (prover:"lambdify") }*) ENABLEDaxioms == TRUE (*{ by (prover:"enabledaxioms") }*) +ENABLEDrewrites == TRUE (*{ by (prover:"enabledrewrites") }*) +ENABLEDrules == TRUE (*{ by (prover:"enabledrules") }*) LevelComparison == TRUE (*{ by (prover:"levelcomparison") }*) (* The operators EnabledWrapper and CdotWrapper occur in an intermediate *) diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml index 0e021e01..dfa99dad 100644 --- a/lsp/lib/docs/proof_step.ml +++ b/lsp/lib/docs/proof_step.ml @@ -353,7 +353,7 @@ let of_module (mule : Tlapm_lib.Module.T.mule) prev : t option = proof status between the modifications. *) let o = match o.fingerprint with - | None -> Tlapm_lib.Backend.Fingerprints.write_fingerprint o + | None -> Tlapm_lib.Backend.Prep.prepare_obligation o | Some _ -> o in let o = Obl.of_parsed_obligation o Proof_status.Pending in diff --git a/lsp/lib/server/handlers.ml b/lsp/lib/server/handlers.ml index f4e8f8ea..4ba13311 100644 --- a/lsp/lib/server/handlers.ml +++ b/lsp/lib/server/handlers.ml @@ -351,7 +351,8 @@ module Make (CB : Callbacks) = struct with exc -> let open Jsonrpc.Response.Error in let exc_str = Printexc.to_string exc in - Eio.traceln "LSP request failed with exception %s" exc_str; + let exc_btr = Printexc.get_backtrace () in + Eio.traceln "LSP request failed with exception %s, backtrace:\n%s" exc_str exc_btr; reply_error req Code.InternalError exc_str state) | Response resp -> handle_jsonrpc_response resp state | Batch_call sub_packets -> diff --git a/src/backend.mli b/src/backend.mli index 34aed396..31c37b5e 100644 --- a/src/backend.mli +++ b/src/backend.mli @@ -22,6 +22,9 @@ module Types: sig } end +module Prep: sig + val prepare_obligation: Proof.T.obligation -> Proof.T.obligation +end module Fingerprints: sig val write_fingerprint: diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index 90d9fd0e..b98ab458 100644 --- a/src/backend/fingerprints.ml +++ b/src/backend/fingerprints.ml @@ -16,8 +16,7 @@ type ident = | Identhypi of int | Identvar of string | Identhyp of string * string - | IdentBPragma - + | IdentBPragma of string (************************) (***** Stack module ******) @@ -86,7 +85,7 @@ let print_stack h = | Identhypi i -> Printf.sprintf " @%d@ Identhypi [%d]" (l-n) i | Identhyp (kind, s) -> Printf.sprintf " @%d@ Identhyp [%s,%s]" (l-n) kind s | Identvar s -> Printf.sprintf " @%d@ Identvar [%s]" (l-n) s - | IdentBPragma -> "Identpragma" + | IdentBPragma s -> Printf.sprintf "Identpragma [%s]" s | No -> Printf.sprintf " @%d@ [NO]" (l-n) end in Array.iteri (fun i (v,r) -> Printf.printf "%s (%s);" (to_st v i) (string_of_bool !r)) h.Stack.stack; Printf.printf "\n%!" @@ -250,7 +249,7 @@ let rec fp_expr counthyp countvar stack buf e = incr countvar | Identhypi i -> bprintf buf "$HYP(%d)" i | Identvari i -> bprintf buf "$PRM(%d)" i - | IdentBPragma -> () + | IdentBPragma s -> bprintf buf "$BPragma(%s)" s end | Opaque s -> Buffer.add_string buf s | Internal bin -> fp_bin buf bin @@ -276,7 +275,7 @@ let rec fp_expr counthyp countvar stack buf e = | Ix n -> begin match Stack.get stack n with - | IdentBPragma,_ -> () + | IdentBPragma s, _ -> bprintf buf "$BPragma(%s)" s | _ -> bprintf buf "$OpApp(%a;%a)" fps o (list fps) es end | _ -> bprintf buf "$OpApp(%a;%a)" fps o (list fps) es @@ -444,9 +443,9 @@ and fp_sequent stack buf sq = if !r then bprintf buf "$Def(%d,%d)" (match v with Identhypi i -> i | _ -> assert false) - (if Expr.Constness.is_const e then 0 else 3) - | Defn ({core = Bpragma _}, _, Hidden, _) -> - Stack.push stack (IdentBPragma, ref false); + (Expr.Levels.get_level e) + | Defn ({core = Bpragma (nm, _, _)}, _, Hidden, _) -> + Stack.push stack (IdentBPragma nm.core, ref false); spin stack cx; ignore (Stack.pop stack) | Defn ({core = Instance _}, _, Hidden, _) -> assert false @@ -481,8 +480,8 @@ and fp_sequent stack buf sq = bprintf buf "$Def(%d;%a)" (match v with Identhypi i -> i | _ -> assert false) (fp_expr counthyp countvar stack) e - | Defn ({core = Bpragma _}, _, Visible, _) -> - Stack.push stack (IdentBPragma, ref false); + | Defn ({core = Bpragma (nm, _, _)}, _, Visible, _) -> + Stack.push stack (IdentBPragma nm.core, ref false); spin stack cx; ignore (Stack.pop stack) | Defn ({core = Instance _}, _, Visible, _) -> assert false @@ -575,7 +574,16 @@ let fp_sequent sq = let fingerprint ob = - to_string (fp_sequent ob.Proof.T.obl.core) + let enabledrules = if Expr.T.has_enabledaxioms ob.obl then + begin if Expr.T.get_enabledaxioms ob.obl then + "Level<=1" + else + "Level>1" + end else "" in + let buf = fp_sequent ob.Proof.T.obl.core in + bprintf buf "%s" enabledrules; + (* Buffer.output_buffer stdout buf; *) + to_string buf (* adds its fingerprint to an obligation *) let write_fingerprint ob = diff --git a/src/backend/fpfile.ml b/src/backend/fpfile.ml index 912a5a1f..2b81d0d5 100644 --- a/src/backend/fpfile.ml +++ b/src/backend/fpfile.ml @@ -24,7 +24,7 @@ module V13 = struct (* introduced on 2019- in revision *) (* Adds the cases "ExpandENABLED", "ExpandCdot", "AutoUSE", "Lambdify", - "ENABLEDaxioms", "LevelComparison" + "ENABLEDaxioms", "ENABLEDrewrites", "ENABLEDrules", "LevelComparison" to type meth. *) @@ -59,6 +59,8 @@ module V13 = struct | ExpandCdot | Lambdify | ENABLEDaxioms + | ENABLEDrewrites + | ENABLEDrules | LevelComparison | Trivial @@ -115,6 +117,8 @@ module V13 = struct expandcdotres : sti option; lambdifyres: sti option; enabledaxiomsres: sti option; + enabledrewritesres: sti option; + enabledrulesres: sti option; levelcomparisonres: sti option; } @@ -239,6 +243,8 @@ and meth_to_Vx m = | M.ExpandCdot -> ExpandCdot | M.Lambdify -> Lambdify | M.ENABLEDaxioms -> ENABLEDaxioms + | M.ENABLEDrewrites -> ENABLEDrewrites + | M.ENABLEDrules -> ENABLEDrules | M.LevelComparison -> LevelComparison | M.Trivial -> Trivial @@ -280,6 +286,8 @@ type prover = | Pexpandcdot | Plambdify | Penabledaxioms + | Penabledrewrites + | Penabledrules | Plevelcomparison | Ptrivial @@ -311,6 +319,8 @@ let prover_of_method m = | AutoUSE -> Pautouse | Lambdify -> Plambdify | ENABLEDaxioms -> Penabledaxioms + | ENABLEDrewrites -> Penabledrewrites + | ENABLEDrules -> Penabledrules | LevelComparison -> Plevelcomparison | Trivial -> Ptrivial @@ -440,6 +450,8 @@ let empty = { expandcdotres = None; lambdifyres = None; enabledaxiomsres = None; + enabledrewritesres = None; + enabledrulesres = None; levelcomparisonres = None; } @@ -468,6 +480,8 @@ let add_to_record r st = | NTriv (_, ExpandCdot) -> {r with expandcdotres = Some st} | NTriv (_, Lambdify) -> {r with lambdifyres = Some st} | NTriv (_, ENABLEDaxioms) -> {r with enabledaxiomsres = Some st} + | NTriv (_, ENABLEDrewrites) -> {r with enabledrewritesres = Some st} + | NTriv (_, ENABLEDrules) -> {r with enabledrulesres = Some st} | NTriv (_, LevelComparison) -> {r with levelcomparisonres = Some st} | _ -> r @@ -754,6 +768,10 @@ let print_sti_13 (st, d, pv, zv, iv) = printf "Lambdify definitions"; | V13.ENABLEDaxioms -> printf "ENABLED axioms"; + | V13.ENABLEDrewrites -> + printf "ENABLED rewrites"; + | V13.ENABLEDrules -> + printf "ENABLED rules"; | V13.LevelComparison -> printf "Level Comparison"; | V13.Trivial -> @@ -825,9 +843,10 @@ let print_fp_line_13r fp str = print_sti_opt "ExpandCdot" str.V13.expandcdotres; print_sti_opt "Lambdify" str.V13.lambdifyres; print_sti_opt "ENABLED axioms" str.V13.enabledaxiomsres; + print_sti_opt "ENABLED rewrites" str.V13.enabledrewritesres; + print_sti_opt "ENABLED rules" str.V13.enabledrulesres; print_sti_opt "LevelComparison" str.V13.levelcomparisonres - let print_fp_line_13l fp stil = printf " %s :\n" fp; List.iter print_sti_13 stil @@ -945,6 +964,8 @@ and vx_to_meth m = | AutoUSE -> Some M.AutoUSE | Lambdify -> Some M.Lambdify | ENABLEDaxioms -> Some M.ENABLEDaxioms + | ENABLEDrewrites -> Some M.ENABLEDrewrites + | ENABLEDrules -> Some M.ENABLEDrules | LevelComparison -> Some M.LevelComparison | Trivial -> Some M.Trivial diff --git a/src/backend/prep.ml b/src/backend/prep.ml index 00d94257..18c6b4bc 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -641,6 +641,8 @@ let get_prover_name m = | Method.AutoUSE -> "AutoUSE" | Method.Lambdify -> "Lambdify" | Method.ENABLEDaxioms -> "ENABLEDaxioms" + | Method.ENABLEDrewrites -> "ENABLEDrewrites" + | Method.ENABLEDrules -> "ENABLEDrules" | Method.LevelComparison -> "LevelComparison" | Method.Trivial -> "Trivial" @@ -828,6 +830,12 @@ let prove_with ob org_ob meth save = (* FIXME add success fuction *) | Method.ENABLEDaxioms -> print_string "(* ... unexpected application of `ENABLED` axioms *)\n"; assert false + | Method.ENABLEDrewrites -> + print_string "(* ... unexpected application of `ENABLED` rewrites *)\n"; + assert false + | Method.ENABLEDrules -> + print_string "(* ... unexpected application of `ENABLED` rules *)\n"; + assert false | Method.LevelComparison -> print_string "(* ... unexpected level comparison *)\n"; assert false @@ -954,7 +962,10 @@ let expand_enabled_cdot ob ~(autouse: bool) ~(apply_lambdify: bool) ~(enabled_axioms: bool) - ~(level_comparison: bool) = + ~(enabled_rewrites: bool) + ~(enabled_rules: bool) + ~(level_comparison: bool) + ~(used_identifiers: string list) = (* Instantiate modules, use de Bruijn indices, expand action operators, automatically expand definitions necessary for soundness of expanding the operators `ENABLED` and `\cdot`. @@ -972,6 +983,7 @@ let expand_enabled_cdot ob ~expand_enabled:expand_enabled ~expand_cdot:expand_cdot ~autouse:autouse + ~used_identifiers:used_identifiers end else if apply_lambdify then begin let cx = Deque.empty in @@ -980,6 +992,7 @@ let expand_enabled_cdot ob ~lambdify_enabled:apply_lambdify ~lambdify_cdot:apply_lambdify ~autouse:autouse + ~used_identifiers:used_identifiers end else if level_comparison then begin let cx = Deque.empty in @@ -987,13 +1000,22 @@ let expand_enabled_cdot ob cx expr end else if enabled_axioms then begin + let cx = Deque.empty in + Expr.Action.enabled_axioms cx expr + end + else if enabled_rewrites then begin + let cx = Deque.empty in + Expr.Action.enabled_rewrites cx expr + end + else if enabled_rules then begin + (* TODO: rename property to enabledrules *) if Expr.T.has_enabledaxioms expr then begin - print_string "expr has ENABLEDaxioms property ===\n"; + (* print_string "expr has ENABLEDrules property ===\n"; *) if not (Expr.T.get_enabledaxioms ob.obl) then - failwith "ENABLEDaxioms depends on assumptions of level > 1 \n\n" + failwith "ENABLEDrules depends on assumptions of level > 1 \n\n" end; let cx = Deque.empty in - Expr.Action.implication_to_enabled cx expr + Expr.Action.enabled_rules cx expr end else expr @@ -1011,17 +1033,25 @@ let normalize_expand ob fpout thyout record ~(autouse: bool) ~(apply_lambdify: bool) ~(enabled_axioms: bool) + ~(enabled_rewrites: bool) + ~(enabled_rules: bool) ~(level_comparison: bool) = + let used_identifiers = + let expr = expr_from_obl ob in + let cx = Deque.empty in + let identifiers = Expr.Visit.collect_identifiers cx expr in + (* + print_string "Identifiers:\n"; + List.iter (fun v -> print_string v; print_string ", ") identifiers; + *) + identifiers in let ob = normalize_expr ob in try let ob = expand_enabled_cdot - ob - ~expand_enabled:expand_enabled - ~expand_cdot:expand_cdot - ~autouse:autouse - ~apply_lambdify:apply_lambdify - ~enabled_axioms:enabled_axioms - ~level_comparison:level_comparison in + ob ~expand_enabled ~expand_cdot ~autouse + ~apply_lambdify ~enabled_axioms ~enabled_rewrites + ~enabled_rules ~level_comparison + ~used_identifiers in (ob, true) with Failure msg -> (* `msg` is the message from soundness checks, @@ -1031,7 +1061,8 @@ let normalize_expand ob fpout thyout record *) begin assert (expand_enabled || expand_cdot || apply_lambdify - || enabled_axioms || level_comparison); + || enabled_axioms || enabled_rewrites + || enabled_rules || level_comparison); (* !cleanup (); *) (* let warnings: string = Errors.get_warnings () in *) let warnings = (msg ^ "\nObligation:\n\n") in @@ -1059,6 +1090,10 @@ let normalize_expand ob fpout thyout record Method.Lambdify end else if enabled_axioms then begin Method.ENABLEDaxioms + end else if enabled_rewrites then begin + Method.ENABLEDrewrites + end else if enabled_rules then begin + Method.ENABLEDrules end else begin assert level_comparison; Method.LevelComparison @@ -1252,6 +1287,10 @@ let compute_meth def args usept = Method.Lambdify | Some "enabledaxioms" -> Method.ENABLEDaxioms + | Some "enabledrewrites" -> + Method.ENABLEDrewrites + | Some "enabledrules" -> + Method.ENABLEDrules | Some "levelcomparison" -> Method.LevelComparison | Some "trivial" -> @@ -1342,6 +1381,8 @@ let find_meth ob = (x <> Method.AutoUSE) && (x <> Method.Lambdify) && (x <> Method.ENABLEDaxioms) && + (x <> Method.ENABLEDrewrites) && + (x <> Method.ENABLEDrules) && (x <> Method.LevelComparison) )) meths in @@ -1393,6 +1434,13 @@ let add_constness ob = | {core = Expr.T.Sequent sq} -> {ob with obl = sq @@ ob.obl} | _ -> assert false +let add_expr_level ob = + let e = noprops (Expr.T.Sequent ob.obl.core) in + let cx = Deque.empty in + let e = Expr.Levels.compute_level cx e in + match e with + | {core=Expr.T.Sequent sq} -> {ob with obl = sq @@ ob.obl} + | _ -> assert false let is_success st = match st with @@ -1405,53 +1453,73 @@ let is_trivial x = try ignore (Lazy.force x); true with Nontrivial -> false -(* This function is called on every obligation in the range selected by the - user. It produces a [Schedule.t] that represents the job of proving this - obligation. -*) -let ship ob fpout thyout record = - vprintf "(* trying obligation %d generated from %s *)\n" (Option.get ob.id) - (Util.location ~cap:false ob.obl); - begin try - print_obl_and_msg ob "Proof obligation before `find_meth`:\n"; - let ob = find_meth ob in +let prepare_obligation_with_effects ob fpout thyout record print = + if print then begin + print_obl_and_msg ob "Proof obligation before `find_meth`:\n" + end; + let ob = find_meth ob in + if print then begin print_obl_and_msg ob "Proof obligation after `find_meth`:\n"; - Toolbox.print_ob_provers ob; - let meths = get ob.obl Proof.T.Props.meth in - let expand_enabled = List.exists - (fun x -> (x = Method.ExpandENABLED)) meths in - let expand_cdot = List.exists - (fun x -> (x = Method.ExpandCdot)) meths in - let autouse = List.exists - (fun x -> (x = Method.AutoUSE)) meths in - let apply_lambdify = List.exists - (fun x -> (x = Method.Lambdify)) meths in - let enabled_axioms = List.exists - (fun x -> (x = Method.ENABLEDaxioms)) meths in - let level_comparison = List.exists - (fun x -> (x = Method.LevelComparison)) meths in - let meths = List.filter - (fun x -> ( - (x <> Method.ExpandENABLED) && - (x <> Method.ExpandCdot) && - (x <> Method.AutoUSE) && - (x <> Method.Lambdify) && - (x <> Method.ENABLEDaxioms) && - (x <> Method.LevelComparison) - )) - meths in - assert ((List.length meths) > 0); - (* compute fingerprint: - The fingerprint is computed before: - - expanding definitions listed in `BY DEF` - - normalizing expressions - - auto-expanding definitions for sound `ENABLED`, `\cdot` expansion - - replacing `ENABLED` and `\cdot` with rigid quantification - The fingerprints include both the assertion and `BY` statement - proof directives. - *) + Toolbox.print_ob_provers ob + end; + let meths = get ob.obl Proof.T.Props.meth in + let expand_enabled = List.exists + (fun x -> (x = Method.ExpandENABLED)) meths in + let expand_cdot = List.exists + (fun x -> (x = Method.ExpandCdot)) meths in + let autouse = List.exists + (fun x -> (x = Method.AutoUSE)) meths in + let apply_lambdify = List.exists + (fun x -> (x = Method.Lambdify)) meths in + let enabled_axioms = List.exists + (fun x -> (x = Method.ENABLEDaxioms)) meths in + let enabled_rewrites = List.exists + (fun x -> (x = Method.ENABLEDrewrites)) meths in + let enabled_rules = List.exists + (fun x -> (x = Method.ENABLEDrules)) meths in + let level_comparison = List.exists + (fun x -> (x = Method.LevelComparison)) meths in + let meths = List.filter + (fun x -> ( + (x <> Method.ExpandENABLED) && + (x <> Method.ExpandCdot) && + (x <> Method.AutoUSE) && + (x <> Method.Lambdify) && + (x <> Method.ENABLEDaxioms) && + (x <> Method.ENABLEDrewrites) && + (x <> Method.ENABLEDrules) && + (x <> Method.LevelComparison) + )) + meths in + assert ((List.length meths) > 0); + (* compute fingerprint: + The fingerprint is computed before: + - expanding definitions listed in `BY DEF` + - normalizing expressions + - auto-expanding definitions for sound `ENABLED`, `\cdot` expansion + - replacing `ENABLED` and `\cdot` with rigid quantification + The fingerprints include both the assertion and `BY` statement + proof directives. + *) + if autouse then begin + let p = + lazy (normalize_expand (add_expr_level ob) + fpout thyout record + ~expand_enabled + ~expand_cdot + ~autouse + ~apply_lambdify + ~enabled_axioms + ~enabled_rewrites + ~enabled_rules + ~level_comparison) in + let (p1, expand_success) = Lazy.force p in + let fp_ob = Fingerprints.write_fingerprint p1 in + let p = lazy (fp_ob, expand_success) in + (lazy fp_ob, p, meths) + end else begin let const_fp_ob = - lazy (Fingerprints.write_fingerprint (add_constness ob)) + lazy (Fingerprints.write_fingerprint (add_expr_level ob)) in let p = lazy (normalize_expand (Lazy.force const_fp_ob) fpout thyout record @@ -1460,8 +1528,31 @@ let ship ob fpout thyout record = ~autouse ~apply_lambdify ~enabled_axioms + ~enabled_rewrites + ~enabled_rules ~level_comparison) in + (const_fp_ob, p, meths) + end + +(* This function is used also in the LSP server to get the fingerprint for + an obligation with the ENABLED and Cdot expanded properly. +*) +let prepare_obligation ob = + Out_channel.with_open_bin "/dev/null" (fun discard_out -> + let discard_rec _ _ = () in + let fp_ob, p, meths = prepare_obligation_with_effects ob discard_out discard_out discard_rec false in + Lazy.force fp_ob) + +(* This function is called on every obligation in the range selected by the + user. It produces a [Schedule.t] that represents the job of proving this + obligation. +*) +let ship ob fpout thyout record = + vprintf "(* trying obligation %d generated from %s *)\n" (Option.get ob.id) + (Util.location ~cap:false ob.obl); + begin try + let const_fp_ob, p, meths = prepare_obligation_with_effects ob fpout thyout record true in let prep_meth m = let ob = Lazy.force const_fp_ob in let m = Method.scale_time m !Params.timeout_stretch in @@ -1470,6 +1561,7 @@ let ship ob fpout thyout record = assert ((List.length to_print) <= 1); (* some method succeeded in proving ? *) let has_success = List.exists is_success to_print in + (* let with_enabled_and_fp = if (to_do = None) && (not has_success) && expand_enabled then begin match List.hd to_print with @@ -1486,6 +1578,7 @@ let ship ob fpout thyout record = end else false in + *) (* attempting to prove, or noting that proof obligation is trivial *) if has_success then begin List.iter (fun st -> Toolbox.print_old_res ob st false) to_print; @@ -1520,14 +1613,15 @@ let ship ob fpout thyout record = | Some schedule -> schedule (* is trivial *) | None -> (* nontrivial *) begin - if not with_enabled_and_fp then - List.iter (fun st -> Toolbox.print_old_res ob st true) to_print; + List.iter (fun st -> Toolbox.print_old_res ob st true) to_print; if to_print <> [] then record has_success ob; assert (to_do <> Some Method.ExpandENABLED); assert (to_do <> Some Method.ExpandCdot); assert (to_do <> Some Method.AutoUSE); assert (to_do <> Some Method.Lambdify); assert (to_do <> Some Method.ENABLEDaxioms); + assert (to_do <> Some Method.ENABLEDrewrites); + assert (to_do <> Some Method.ENABLEDrules); assert (to_do <> Some Method.LevelComparison); (* try backends only if any expansions of `ENABLED` and `\cdot` that have been requested have been completed successfully. diff --git a/src/backend/prep.mli b/src/backend/prep.mli index 273603d0..6f116ca7 100644 --- a/src/backend/prep.mli +++ b/src/backend/prep.mli @@ -28,3 +28,5 @@ val normalize: auto_expand_defs: bool -> obligation *) + +val prepare_obligation: obligation -> obligation diff --git a/src/expr.mli b/src/expr.mli index 6ab1fa5a..5cf1c31d 100644 --- a/src/expr.mli +++ b/src/expr.mli @@ -636,6 +636,8 @@ module Visit: sig method rename : ctx -> hyp -> Util.hint -> hyp * Util.hint method renames : ctx -> hyp list -> Util.hints -> hyp list * Util.hints end + + val collect_identifiers: ctx -> expr -> string list end @@ -796,17 +798,18 @@ end module Action: sig open T - val invert_renaming: - ctx -> expr -> - expr - val implication_to_enabled: - ctx -> expr -> - expr + + val invert_renaming: ctx -> expr -> expr + val enabled_axioms: ctx -> expr -> expr + val enabled_rewrites: ctx -> expr -> expr + val enabled_rules: ctx -> expr -> expr + val implication_to_enabled: ctx -> expr -> expr val lambdify: ctx -> expr -> lambdify_enabled:bool -> lambdify_cdot:bool -> autouse:bool -> + used_identifiers: string list -> expr val quantify: ctx -> expr -> @@ -818,6 +821,7 @@ module Action: sig expand_enabled:bool -> expand_cdot:bool -> autouse:bool -> + used_identifiers: string list -> expr end @@ -847,7 +851,7 @@ module LevelComparison: sig open T class level_comparison : object method compare: - ctx -> ctx -> + ctx -> ctx -> ctx -> expr -> expr -> bool method expr: diff --git a/src/expr/e_action.ml b/src/expr/e_action.ml index 408b0192..d32980e6 100644 --- a/src/expr/e_action.ml +++ b/src/expr/e_action.ml @@ -34,6 +34,7 @@ module Subst = E_subst module T = E_t open E_t module Visit = E_visit +module StringSet = Util.Coll.Ss type set = (string, unit) Hashtbl.t @@ -481,7 +482,7 @@ let var_to_fresh for constants bound by quantifiers that are introduced for representing `\cdot`. *) - name ^ "#enabled#prime" ^ (string_of_int nesting) + name ^ "#" ^ (string_of_int nesting) let flex_to_fresh_opaque @@ -761,21 +762,32 @@ let shift_indices_after_lambdify (e: expr): expr = visitor#expr s e -let normalize_lambda_signature signature keep_same_names = - let n = List.length signature in +let normalize_lambda_signature signature_ used_identifiers = + (* + let n = List.length signature_ in assert (n >= 1); let names = List.init n (fun i -> param_name ^ string_of_int i) in - let params = List.map (fun (p, _) -> p.core) signature in + *) + let mk_id name i = name ^ "_" ^ (string_of_int i) in + let map_id (p, _) = + let (name, depth) = match (String.split_on_char '#' p.core) with + | [name; depth] -> (name, depth) + | _ -> assert false in + let f i = List.mem (mk_id name i) used_identifiers in + let i = ref (int_of_string depth) in + while (f !i) do + i := !i + 1 + done; + mk_id name !i in + let names = List.map map_id signature_ in + let params = List.map (fun (p, _) -> p.core) signature_ in let mk_parameter name flex_name = let h = noprops name in (* store name for inverse renaming *) let h = assign h variable_name flex_name in let shp = Shape_expr in (h, shp) in - if keep_same_names then - List.map2 mk_parameter params params - else - List.map2 mk_parameter names params + List.map2 mk_parameter names params class normalize_lambda_param_names = @@ -792,10 +804,10 @@ class normalize_lambda_param_names = object (self: 'self) inherit [unit] Visit.map_visible_hyp as super - val mutable _keep_same_names: bool = true + val mutable _used_identifiers: string list = [] - method config keep_same_names = - _keep_same_names <- keep_same_names + method config used_identifiers = + _used_identifiers <- used_identifiers method expr (((), (cx: T.ctx)) as scx) @@ -808,7 +820,7 @@ class normalize_lambda_param_names = assert (fst.core <> temp_bound); let expr_ = self#expr scx expr in let signature = normalize_lambda_signature - signature _keep_same_names in + signature _used_identifiers in let lambda = Lambda (signature, expr_) in let expr_ = noprops lambda in (* without renaming, even without coalescing, @@ -836,6 +848,7 @@ class lambdify_action_operators = val mutable _lambdify_enabled: bool = false val mutable _lambdify_cdot: bool = false + val mutable _used_identifiers: string list = [] (* This class does not introduce quantifiers, it only binds occurrences of variables in the scope of primes within `ENABLED` and the first @@ -930,10 +943,11 @@ class lambdify_action_operators = (e: expr) ~(lambdify_enabled: bool) ~(lambdify_cdot: bool) - ~(keep_same_names: bool): + ~(used_identifiers:string list): expr = _lambdify_enabled <- lambdify_enabled; _lambdify_cdot <- lambdify_cdot; + _used_identifiers <- used_identifiers; let e_ = let scope = (None, None) in self#expr (scope, cx) e in @@ -941,7 +955,7 @@ class lambdify_action_operators = let e_ = E_anon.anon#expr ([], cx) e_ in let e_ = let visitor = new normalize_lambda_param_names in - visitor#config keep_same_names; + visitor#config used_identifiers; visitor#expr ((), cx) e_ in e_ @@ -1399,6 +1413,662 @@ class expansion_of_action_operators = end +let collect_vars cx e primed = + let found_hidden = ref false in + let visitor = + object (self: 'self) + inherit [(set option) * (set option)] + E_visit.iter_visible_hyp as super + + method expr (((a, b), cx) as scx) e = + let inscope = ((a, b) <> (None, None)) in + let recurse_ a b = function + | None -> () + | Some arg -> + let scope = (a, b) in + self#expr (scope, cx) arg in + let expand arg1 arg2 = + recurse_ a None arg1; + recurse_ None b arg2 + in + match e.core with + | Apply ({core=Internal Prime}, [arg]) -> + let scope = (b, None) in + self#expr (scope, cx) arg + | Ix n -> + begin + assert (n >= 1); + let hyp = E_t.get_val_from_id cx n in + let prime_scope = match a with + | None -> false + | _ -> true in + match hyp.core with + | Flex name -> + let var_name = name.core in + begin + match a with + | None -> () + | Some primed_vars -> + if (not (Hashtbl.mem primed_vars var_name)) then + Hashtbl.add primed_vars var_name () + end + | Fresh (_, _, kind, _) -> + begin + match kind with + | Constant -> () + | State -> if prime_scope then + found_hidden := true + | Action + | Temporal + | Unknown -> if inscope then + found_hidden := true + end + | Defn (_, _, Hidden, _) -> + let e_level = E_levels.get_level e in + if ( + (prime_scope && (e_level >= 1)) || + ((not prime_scope) && (e_level >= 2))) then + found_hidden := true + | _ -> () + end + | Apply ({core=Internal ENABLED}, [arg1]) -> + expand (Some arg1) None + | Apply ({core=Internal Cdot}, [arg1; arg2]) -> + expand (Some arg1) (Some arg2) + | Apply ({core=Internal UNCHANGED}, _) + | Sub _ + when inscope -> + let e_ = expand_propositional_action_operators e in + self#expr scx e_ + | _ -> super#expr scx e + end + in + let primed_vars = Hashtbl.create 16 in + let scx = if primed then + ((None, Some primed_vars), cx) + else + ((Some primed_vars, None), cx) in + visitor#expr scx e; + if !found_hidden then + None + else + Some (E_visit.set_to_list primed_vars) + + +let collect_unprimed_vars cx e = + collect_vars cx e false + + +let collect_primed_vars cx e = + collect_vars cx e true + + +let enabled_axioms cx expr = + let expr = E_levels.compute_level cx expr in + + (* TODO: consider including equality (constructor `Eq`) + in addition to equivalence + *) + let check_active cx_goal expr = + begin + let core = match expr.core with + + (* ------------------------------------------------ + ENABLED commutes with existential quantification + + ENABLED (\E i \in S: A(i)) <=> \E i \in S: ENABLED A(i) + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal ENABLED}, [ + {core=Quant ( + Exists, + [(nm_a, Constant, Domain dom_a)], + {core=Apply (a, [{core=Ix 1}])})} + ])}; + {core=Quant ( + Exists, + [(nm_b, Constant, Domain dom_b)], + {core=Apply ({core=Internal ENABLED}, + [{core=Apply (b, [{core=Ix 1}])}])})} + ]) + (* (\E i \in S: ENABLED A(i)) <=> ENABLED (\E i \in S: A(i)) *) + | Apply ({core=Internal Equiv}, [ + {core=Quant ( + Exists, + [(nm_b, Constant, Domain dom_b)], + {core=Apply ({core=Internal ENABLED}, + [{core=Apply (b, [{core=Ix 1}])}])})}; + {core=Apply ({core=Internal ENABLED}, [ + {core=Quant ( + Exists, + [(nm_a, Constant, Domain dom_a)], + {core=Apply (a, [{core=Ix 1}])})} + ])} + ]) when ( + (E_eq.expr dom_a dom_b) && + (E_eq.expr a b) && + ((E_levels.get_level dom_a) <= 1) + ) + -> + Internal TRUE + + (* ------------------------------------------------ + ENABLED distributes over disjunction + + ENABLED (a \/ b) <=> (ENABLED a \/ ENABLED b) + ENABLED (a \/ b) <=> (ENABLED b \/ ENABLED a) + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal ENABLED}, + [{core=Apply ({core=Internal Disj}, [a; b])}] + )}; + {core=Apply ({core=Internal Disj}, [ + {core=Apply ({core=Internal ENABLED}, [c])}; + {core=Apply ({core=Internal ENABLED}, [d])} + ])} + ]) + (* (ENABLED a \/ ENABLED b) <=> ENABLED (a \/ b) + (ENABLED b \/ ENABLED a) <=> ENABLED (a \/ b) + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal Disj}, [ + {core=Apply ({core=Internal ENABLED}, [c])}; + {core=Apply ({core=Internal ENABLED}, [d])} + ])}; + {core=Apply ({core=Internal ENABLED}, + [{core=Apply ({core=Internal Disj}, [a; b])}] + )} + ]) when ( + ((E_eq.expr a c) && (E_eq.expr b d)) || + ((E_eq.expr a d) && (E_eq.expr b c)) ) + -> + let a_level = E_levels.get_level a in + let b_level = E_levels.get_level b in + assert (a_level <= 2); + assert (b_level <= 2); + Internal TRUE + + (* ------------------------------------------------ + ENABLED distributes over conjunction of actions + with disjoint sets of primed variables + + ENABLED (a /\ b) <=> (ENABLED a /\ ENABLED b) + ENABLED (a /\ b) <=> (ENABLED b /\ ENABLED a) + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal ENABLED}, + [{core=Apply ({core=Internal Conj}, [a; b])}] + )}; + {core=Apply ({core=Internal Conj}, [ + {core=Apply ({core=Internal ENABLED}, [c])}; + {core=Apply ({core=Internal ENABLED}, [d])} + ])} + ]) + (* (ENABLED a /\ ENABLED b) <=> ENABLED (a /\ b) + (ENABLED b /\ ENABLED a) <=> ENABLED (a /\ b) + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal Conj}, [ + {core=Apply ({core=Internal ENABLED}, [c])}; + {core=Apply ({core=Internal ENABLED}, [d])} + ])}; + {core=Apply ({core=Internal ENABLED}, + [{core=Apply ({core=Internal Conj}, [a; b])}] + )} + ]) when ( + ((E_eq.expr a c) && (E_eq.expr b d)) || + ((E_eq.expr a d) && (E_eq.expr b c)) ) + -> + let a_variables = collect_primed_vars cx_goal a in + let b_variables = collect_primed_vars cx_goal b in + begin + match (a_variables, b_variables) with + | (Some a_variables, Some b_variables) -> + let cap = List.filter + (fun x -> List.mem x a_variables) b_variables in + let isempty = (List.length cap) = 0 in + (* assert actions *) + let a_level = E_levels.get_level a in + let b_level = E_levels.get_level b in + assert (a_level <= 2); + assert (b_level <= 2); + if isempty then + Internal TRUE + else + expr.core + | _ -> expr.core + end + + (* ------------------------------------------------ + State predicates can be pulled outside ENABLED + + ENABLED (a /\ b) <=> (a /\ ENABLED b) + ENABLED (b /\ a) <=> (a /\ ENABLED b) + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal ENABLED}, + [{core=Apply ({core=Internal Conj}, [c; d])}] + )}; + {core=Apply ({core=Internal Conj}, [ + a; + {core=Apply ({core=Internal ENABLED}, [b])} + ])} + ]) + (* (a /\ ENABLED b) <=> ENABLED (a /\ b) + (a /\ ENABLED b) <=> ENABLED (b /\ a) + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal Conj}, [ + a; + {core=Apply ({core=Internal ENABLED}, [b])} + ])}; + {core=Apply ({core=Internal ENABLED}, + [{core=Apply ({core=Internal Conj}, [c; d])}] + )} + ]) when ( + ((E_eq.expr a c) && (E_eq.expr b d)) || + ((E_eq.expr a d) && (E_eq.expr b c)) ) + -> + let a_level = E_levels.get_level a in + let b_level = E_levels.get_level b in + if (a_level <= 1) && (b_level <= 2) then + Internal TRUE + else + expr.core + | _ -> expr.core + in + core @@ expr + end in + let sq = match expr.core with + | Sequent sq -> sq + | _ -> assert false in + let (_, cx_goal) = + let visitor = object (self: 'self) + inherit [unit] E_visit.iter_visible_hyp + end in + visitor#hyps ((), cx) sq.context in + let new_active = check_active cx_goal sq.active in + let sq = {sq with active=new_active} in + noprops (Sequent sq) + + (* + begin if proved then + Util.printf ~at:expr ~prefix:"[INFO]" "%s" + ("\nProved " ^ rule ^ "\n") + else + failwith "ENABLEDaxioms proof directive did not succeed.\n" end; + *) + + +let collect_top_conjuncts cx e = + (* Return list of conjuncts. *) + let conjuncts = ref Deque.empty in + let visitor = + object (self: 'self) + inherit [unit] E_visit.iter as super + + method expr (((_), cx) as scx) e = + match e.core with + | Apply ({core=Internal Conj}, [a; b]) -> + self#expr scx a; + self#expr scx b + | List (And, es) -> + List.iter (self#expr scx) es + | _ -> + conjuncts := Deque.snoc !conjuncts e + end + in + let scx = ((), cx) in + visitor#expr scx e; + Deque.to_list !conjuncts + + +let group_conjuncts cx conjuncts = + (* compute the primed variables of each conjunct *) + let primed_variables = List.map (collect_primed_vars cx) conjuncts in + (* return single group if any set of primed variables is `None` *) + let has_none = List.exists + (fun x -> match x with + | None -> true + | _ -> false) primed_variables in + if has_none then + [conjuncts] + else + begin + (* split into minimal classes with disjoint sets of primed variables *) + let primed_variables = List.map + (fun x -> match x with + | None -> assert false + | Some x -> StringSet.of_seq (Stdlib.List.to_seq x)) primed_variables in + let vars_conjuncts = List.map2 (fun a b -> (a, [b])) + primed_variables conjuncts in + (* (StringSet, expr list) list *) + let groups: (StringSet.t * (E_t.expr list)) list ref = ref [] in + let f (vars, es) = + let (other, intersecting) = List.partition + (fun (a, b) -> StringSet.disjoint a vars) !groups in + let f (vars_a, es_a) (vars_b, es_b) = + (StringSet.union vars_a vars_b, List.append es_a es_b) in + let merged = List.fold_left f (vars, es) intersecting in + groups := merged :: other in + List.iter f vars_conjuncts; + List.map (fun (vars, es) -> es) !groups + end + + +class enabled_rewriter = + object (self : 'self) + inherit [unit] E_visit.map_visible_hyp as super + + method expr scx oe = + let cx = snd scx in + begin + let core = match oe.core with + + (* ------------------------------------------------ + ENABLED commutes with existential quantification + + ENABLED (\E i \in S: A(i)) --> \E i \in S: ENABLED A(i) + *) + | Apply ({core=Internal ENABLED}, [ + {core=Quant ( + Exists, + [(nm, Constant, Domain dom)], + e)}]) when ((E_levels.get_level dom) <= 1) -> + (* recurse *) + let dom = self#expr scx dom in + let e = + let h = + let bound = Bounded (dom, Visible) in + let h_ = Fresh (nm, Shape_expr, Constant, bound) in + h_ @@ nm in + let scx = + let (s, cx) = scx in + let cx = Deque.snoc cx h in + (s, cx) in + self#expr scx e in + (* form result *) + let enabled_a_core = Apply (noprops (Internal ENABLED), [e]) in + let enabled_a = noprops enabled_a_core in + let core = Quant ( + Exists, + [(nm, Constant, Domain dom)], + enabled_a) in + core + + (* ------------------------------------------------ + ENABLED distributes over disjunction + + ENABLED (a \/ b) --> (ENABLED a) \/ (ENABLED B) + *) + | Apply ({core=Internal ENABLED}, + [{core=Apply ({core=Internal Disj}, [a; b])}]) -> + let a_level = E_levels.get_level a in + let b_level = E_levels.get_level b in + assert (a_level <= 2); + assert (b_level <= 2); + (* recurse *) + let a = self#expr scx a in + let b = self#expr scx b in + (* form result *) + let enabled_a_core = Apply (noprops (Internal ENABLED), [a]) in + let enabled_b_core = Apply (noprops (Internal ENABLED), [b]) in + let enabled_a = noprops enabled_a_core in + let enabled_b = noprops enabled_b_core in + let core = Apply (noprops (Internal Disj), [enabled_a; enabled_b]) in + core + + (* ------------------------------------------------ + + ENABLED \/ a + ... + \/ b + --> + \/ ENABLED a + ... + \/ ENABLED b + *) + | Apply ({core=Internal ENABLED}, + [{core=List (Or, es)}]) -> + (* recurse *) + let es = List.map (self#expr scx) es in + (* form result *) + let enabled_disjuncts = List.map + (fun e -> + let enabled = Apply (noprops (Internal ENABLED), [e]) in + let enabled = noprops enabled in + enabled) + es in + let core = List (Or, enabled_disjuncts) in + core + + (* ------------------------------------------------ + ENABLED distributes within the ternary conditional + + ENABLED (IF p THEN a ELSE b) --> IF p THEN ENABLED a ELSE ENABLED B + *) + | Apply ({core=Internal ENABLED}, + [{core=If (p, a, b)}]) when ((E_levels.get_level p) <= 1) -> + (* recurse *) + let p = self#expr scx p in + let a = self#expr scx a in + let b = self#expr scx b in + (* form result *) + let enabled_a_core = Apply (noprops (Internal ENABLED), [a]) in + let enabled_b_core = Apply (noprops (Internal ENABLED), [b]) in + let enabled_a = noprops enabled_a_core in + let enabled_b = noprops enabled_b_core in + let core = If (p, enabled_a, enabled_b) in + core + + (* ------------------------------------------------ + ENABLED distributes within the CASE conditional + + ENABLED (CASE + p1 -> a1 + [] ... + [] pk -> ak + [ [] OTHER -> b ]) --> + CASE + p1 -> ENABLED a1 + [] ... + [] pk -> ENABLED ak + [ [] OTHER -> ENABLED b ] + *) + | Apply ({core=Internal ENABLED}, + [{core=Case (arms, other)}]) -> + let constants = List.filter + (fun (p, a) -> (E_levels.get_level p) <= 1) arms in + let all_constants = ((List.length constants) = (List.length arms)) in + (* recurse *) + (* resursion occurs after getting the expression levels, + so that we do not have to recompute them here for the + newly mapped expressions + *) + let arms = List.map + (fun (p, a) -> + (self#expr scx p, self#expr scx a)) + arms in + let other = Option.map + (fun x -> self#expr scx x) other in + (* form result *) + if all_constants then + begin + let new_arms = List.map + (fun (p, a) -> + let enabled_a_core = Apply ( + noprops (Internal ENABLED), [a]) in + let enabled_a = noprops enabled_a_core in + (p, enabled_a)) arms in + let new_other = Option.map (fun x -> + let enabled_other_core = Apply ( + noprops (Internal ENABLED), [x]) in + let enabled_other = noprops enabled_other_core in + enabled_other) other in + let core = Case (new_arms, new_other) in + core + end + else + Case (arms, other) + + (* ------------------------------------------------ + ENABLED distributes over conjunction of actions + with disjoint sets of primed variables + + ENABLED (a /\ ... /\ b) --> ENABLED a /\ ... /\ ENABLED b + where a, ..., b have disjoint sets of primed variables + *) + | Apply ({core=Internal ENABLED}, + [({core=Apply ({core=Internal Conj}, es)} as expr)]) + | Apply ({core=Internal ENABLED}, + [({core=List (And, es)} as expr)]) -> + let conjuncts = collect_top_conjuncts cx expr in + (* recurse *) + let conjuncts = List.map (self#expr scx) conjuncts in + (* form result *) + let groups: E_t.expr list list = group_conjuncts cx conjuncts in + let enabled_conjuncts = List.map + (fun es -> + let conj = (if ((List.length es) > 1) then + List (And, es) + else + (List.hd es).core) + in + let conj = noprops conj in + let enabled = Apply (noprops (Internal ENABLED), [conj]) in + let enabled = noprops enabled in + enabled) groups in + let core = (if ((List.length enabled_conjuncts) > 1) then + List (And, enabled_conjuncts) + else + (List.hd enabled_conjuncts).core) + in + core + + (* ------------------------------------------------ + State predicates can be pulled outside ENABLED + + ENABLED a --> a + *) + | Apply ({core=Internal ENABLED}, [a]) + when ((E_levels.get_level a) <= 1) -> + (self#expr scx a).core + + (* ------------------------------------------------ + Assignments are satisfiable + + ENABLED (x' = t) --> TRUE + when t is a constant or state function + *) + | Apply ({core=Internal ENABLED} as enabled_op, + [{core=Apply ({core=Internal Eq} as eq_op, + [{core=Apply ({core=Internal Prime}, + [{core=Ix n}])} as xp; t])}]) + when ((E_levels.get_level t) <= 1) -> + let hyp = T.get_val_from_id cx n in + begin match hyp.core with + | Flex _ -> Internal TRUE + | _ -> + let t = self#expr scx t in + let eq = Apply (eq_op, [xp; t]) in + Apply (enabled_op, [noprops eq]) + end + + (* ------------------------------------------------ + Satisfiability of set containment + + ENABLED (x' \in S) --> S # {} + *) + | Apply ({core=Internal ENABLED} as enabled_op, + [{core=Apply ({core=Internal Mem} as mem_op, + [{core=Apply ({core=Internal Prime}, + [{core=Ix n}])} as xp; t])}]) + when ((E_levels.get_level t) <= 1) -> + let hyp = T.get_val_from_id cx n in + begin match hyp.core with + | Flex _ -> Apply (noprops (Internal Neq), [ + t; + noprops (SetEnum []) + ]) + | _ -> + let t = self#expr scx t in + let mem = Apply (mem_op, [xp; t]) in + Apply (enabled_op, [noprops mem]) + end + + | _ -> (super#expr scx oe).core + in + let expr = noprops core in + let expr = E_levels.compute_level cx expr in + expr + end + +end + + +let enabled_rewrites cx expr = + let expr = E_levels.compute_level cx expr in + let visitor = new enabled_rewriter in + let scx = ((), cx) in + let old_expr = ref expr in + let new_expr = ref (visitor#expr scx !old_expr) in + while (not (E_eq.expr !new_expr !old_expr)) do + (* + print_string (E_fmt.string_of_expr cx !old_expr); + print_string (E_fmt.string_of_expr cx !new_expr); + *) + old_expr := !new_expr; + new_expr := visitor#expr scx !old_expr + done; + !new_expr + + +let enabled_rules cx expr = + let expr = E_levels.compute_level cx expr in + (* TODO: consider including equality (constructor `Eq`) + in addition to equivalence + *) + let check_active cx_goal expr = + begin + let core = match expr.core with + (* Proof rule + A <=> B |- ENABLED A <=> ENABLED B + *) + | Apply ({core=Internal Equiv}, [ + {core=Apply ({core=Internal ENABLED}, [a])}; + {core=Apply ({core=Internal ENABLED}, [b])} + ]) + -> + (* TODO: check ENABLEDaxioms property *) + Apply (noprops (Internal Equiv), [a; b]) + + (* Proof rule + A => B |- ENABLED A => ENABLED B + *) + | Apply ({core=Internal Implies}, [ + {core=Apply ({core=Internal ENABLED}, [a])}; + {core=Apply ({core=Internal ENABLED}, [b])} + ]) + -> + (* TODO: check ENABLEDaxioms property *) + Apply (noprops (Internal Implies), [a; b]) + + | _ -> expr.core + in + core @@ expr + end in + let sq = match expr.core with + | Sequent sq -> sq + | _ -> assert false in + let (_, cx_goal) = + let visitor = object (self: 'self) + inherit [unit] E_visit.iter_visible_hyp + end in + visitor#hyps ((), cx) sq.context in + let new_active = check_active cx_goal sq.active in + let sq = {sq with active=new_active} in + noprops (Sequent sq) + let implication_to_enabled cx expr = let expr = E_levels.compute_level cx expr in let found = ref false in @@ -1625,11 +2295,11 @@ let implication_to_enabled cx expr = end | _ -> assert false - let lambdify cx e ~(lambdify_enabled:bool) ~(lambdify_cdot:bool) - ~(autouse:bool) = + ~(autouse:bool) + ~(used_identifiers:string list) = let e = E_levels.rm_expr_level cx e in let e = E_levels.compute_level cx e in let e = expand_definitions cx e @@ -1640,7 +2310,7 @@ let lambdify cx e let e = visitor#expand cx e ~lambdify_enabled:lambdify_enabled ~lambdify_cdot:lambdify_cdot - ~keep_same_names:false in + ~used_identifiers:used_identifiers in let visitor = new check_arity in visitor#expr ((), cx) e; e @@ -1663,7 +2333,8 @@ let expand_action_operators (e: expr) ~(expand_enabled: bool) ~(expand_cdot: bool) - ~(autouse: bool): + ~(autouse: bool) + ~(used_identifiers: string list): expr = assert (expand_enabled || expand_cdot); (* compute expression level information *) @@ -1689,7 +2360,7 @@ let expand_action_operators let e_ = visitor#expand cx e_ ~lambdify_enabled:expand_enabled ~lambdify_cdot:expand_cdot - ~keep_same_names:true in + ~used_identifiers:used_identifiers in let visitor = new replace_action_operators_with_quantifiers in let e_ = visitor#replace cx e_ ~expand_enabled:expand_enabled diff --git a/src/expr/e_action.mli b/src/expr/e_action.mli index f78e8b76..0b919bd9 100644 --- a/src/expr/e_action.mli +++ b/src/expr/e_action.mli @@ -22,11 +22,15 @@ val expand_definitions: expr val expand_propositional_action_operators: expr -> expr val implication_to_enabled: ctx -> expr -> expr +val enabled_axioms: ctx -> expr -> expr +val enabled_rewrites: ctx -> expr -> expr +val enabled_rules: ctx -> expr -> expr val lambdify: ctx -> expr -> lambdify_enabled:bool -> lambdify_cdot:bool -> autouse:bool -> + used_identifiers:string list -> expr val quantify: ctx -> expr -> @@ -38,4 +42,5 @@ val expand_action_operators: expand_enabled:bool -> expand_cdot:bool -> autouse:bool -> + used_identifiers: string list -> expr diff --git a/src/expr/e_level_comparison.ml b/src/expr/e_level_comparison.ml index 49d4538d..9cc2550d 100644 --- a/src/expr/e_level_comparison.ml +++ b/src/expr/e_level_comparison.ml @@ -31,21 +31,24 @@ ASSUME PROVE goal -the algorithm checks that goal results from expr1 or expr2 by a renaming of +the algorithm checks that `goal` results from `expr2` by a renaming of identifiers that does not increase the levels of the identifiers. -If an identifier is renamed, then it is assumed that the identifier before -renaming is declared in declarations2. This ensures correct instantiation -of universal quantifiers, outside of the quantifier scope. +If an identifier is renamed, then it is asserted that the identifier before +renaming is declared in `declarations2`. This ensures correct instantiation +of universal (metatheoretic) quantifiers, outside of the quantifier scope. -If an identifier is not renamed, then the original identifier can occur in -either declarations1 or declarations2. If the identifier occurs in declarations1 -then the identifier is the same declaration in both expr1 and goal or -expr2 and goal. There is no substitution for that identifier in this case. +If an identifier is not renamed, then there are two cases: -If the original identifier occurs in declarations2, then the identical -identifier in goal is from declarations3, and the substitution is sound. +- the identifier is declared in `declarations1`, so it is the same + operator in both `expr2` and `goal`. (`declarations1` includes + module-scope declarations, because the above sequent shows + a proof obligation within `tlapm`). +- the identifier is declared in both `declarations2` and `declarations3`, + so the operator in `expr2` that is declared in `declarations2` is + substituted by an operator of the same name that is declared in + `declarations3`. This substitution is sound. *) class level_comparison = object (self : 'self) @@ -53,13 +56,29 @@ class level_comparison = object (self : 'self) val mutable ctx2: ctx = Deque.empty val mutable op_mapping: string StringMap.t = StringMap.empty - method compare ctx1_ ctx2_ expr1 expr2 = + method compare inner_hyps ctx1_ ctx2_ expr1 expr2 = ctx1 <- ctx1_; ctx2 <- ctx2_; op_mapping <- StringMap.empty; let res = self#expr ctx1_ ctx2_ expr1 expr2 in + (* ensure that all renamed identifiers are declared + within the assumptions of the sequent that appears + as assumption. This ensures that the renaming happens + outside the scope of those declarations. + + All declarations in the nested sequent must be + instantiated. This is required syntactically, + because the consequent cannot itself be a sequent. + Thus, there are no declarations before any renamed ones + that would remain. So the renaming can be justified + by instantiation of declarations in the order that + they appear. + *) let all = ref true in let check (key: string) (value: string) = + (* key: source identifier + value: target identifier + *) if not (key = value) then begin let found = ref false in Deque.iter begin @@ -72,7 +91,7 @@ class level_comparison = object (self : 'self) | Fact _ -> () | _ -> assert false (* Defn ( Recursive | Instance | Bpragrama ) *) - end ctx1; + end inner_hyps; all := !all && !found end in StringMap.iter check op_mapping; @@ -743,15 +762,16 @@ let check_level_change cx expr = | Fact (expr, Visible, _) -> begin match expr.core with | Sequent sq -> - let hyps = sq.context in + let inner_hyps = sq.context in let active = sq.active in let visitor = object (self: 'self) inherit [unit] E_visit.iter_visible_hyp end in - let (_, cx_goal) = visitor#hyps ((), cx2) hyps in - found := !found || (checker cx_goal active) - | _ -> - found := !found || (checker cx2 expr) + let (_, cx_goal) = visitor#hyps + ((), cx2) inner_hyps in + found := !found || ( + checker inner_hyps cx_goal active) + | _ -> () end | _ -> () end; @@ -773,7 +793,14 @@ let check_level_change cx expr = end in let (_, cx_goal) = visitor#hyps ((), cx) hyps in let visitor = new level_comparison in - let f cx_hyps hyp = visitor#compare cx_hyps cx_goal hyp active in + (* cx_hyps: context of source sequent + hyp: goal of source sequent + + cx_goal: context of target sequent + active: goal of target sequent + *) + let f inner_hyps cx_hyps hyp = visitor#compare + inner_hyps cx_hyps cx_goal hyp active in check_context f hyps; let proved = !found in begin if proved then begin diff --git a/src/expr/e_level_comparison.mli b/src/expr/e_level_comparison.mli index 734d787f..00a261e9 100644 --- a/src/expr/e_level_comparison.mli +++ b/src/expr/e_level_comparison.mli @@ -4,7 +4,7 @@ open E_t class level_comparison : object - method compare : ctx -> ctx -> expr -> expr -> bool + method compare : ctx -> ctx -> ctx -> expr -> expr -> bool method expr : ctx -> ctx -> expr -> expr -> bool method exprs : ctx -> ctx -> expr list -> expr list -> bool diff --git a/src/expr/e_visit.ml b/src/expr/e_visit.ml index 269f225f..fea00460 100644 --- a/src/expr/e_visit.ml +++ b/src/expr/e_visit.ml @@ -1228,47 +1228,58 @@ let set_to_list table = Stdlib.List.of_seq seq -let collect_unprimed_vars cx e = - let unprimed_vars = Hashtbl.create 16 in +let collect_identifiers cx e = + (* Return a `string list` of all declared and + defined identifiers in the context `cx` and the expression `e`. + *) + let identifiers = Hashtbl.create 16 in + let add_id v = Hashtbl.replace identifiers v.core () in + let add_ids vs = List.iter add_id vs in let visitor = object (self: 'self) - inherit [bool] iter_visible_hyp as super - - method expr (((prime_scope: bool), cx) as scx) e = - match e.core with - | Apply ({core=Internal Prime}, _) -> - assert (not prime_scope) - | Ix n -> - assert (n >= 1); - assert (not prime_scope); - let hyp = E_t.get_val_from_id cx n in - begin match hyp.core with - | Flex name -> - let var_name = name.core in - Hashtbl.replace unprimed_vars var_name () - | _ -> () - end - | Apply ({core=Internal ENABLED}, _) -> - if (not prime_scope) then - self#expr scx e - | Apply ({core=Internal Cdot}, [arg1; _]) -> - assert (not prime_scope); - self#expr scx arg1 - | Apply ({core=Internal UNCHANGED}, [arg]) -> - assert (not prime_scope); - self#expr scx arg - | Sub (_, action, subscript) -> - assert (not prime_scope); - self#expr scx action; - self#expr scx subscript - | _ -> super#expr scx e - end - in - let prime_scope = false in - let scx = (prime_scope, cx) in + inherit [unit] iter as super + + method expr scx oe = + let vs = match oe.core with + | Lambda (vs, _) -> List.map (fun (v, _) -> v) vs + | Tquant (_, vs, _) -> vs + | Choose (v, _, _) -> [v] + | SetSt (v, _, _) -> [v] + | _ -> [] in + add_ids vs; + super#expr scx oe + + method defn scx df = + let v = match df.core with + | Recursive (nm, _) -> nm + | Operator (nm, _) -> nm + | Bpragma (nm, _, _) -> nm + | Instance (nm, _) -> nm in + add_id v; + super#defn scx df + + method bounds scx bs = + let vs = List.map (fun (v, _, _) -> v) bs in + add_ids vs; + super#bounds scx bs + + method instance scx i = + assert false (* called after `Module.Elab` + expands `INSTANCE` *) + + method hyp scx h = + begin match h.core with + | Fresh (nm, _, _, _) -> add_id nm + | Flex nm -> add_id nm + | Defn _ -> () (* handled in the method `self#defn` *) + | Fact _ -> () end; + super#hyp scx h + end in + let scx = ((), Deque.empty) in + ignore (visitor#hyps scx cx); + let scx = ((), cx) in visitor#expr scx e; - set_to_list unprimed_vars - + set_to_list identifiers let collect_primed_vars cx e = let primed_vars = Hashtbl.create 16 in diff --git a/src/expr/e_visit.mli b/src/expr/e_visit.mli index 21edf711..64ff9705 100644 --- a/src/expr/e_visit.mli +++ b/src/expr/e_visit.mli @@ -98,5 +98,5 @@ class virtual ['s] map_rename : object end val set_to_list: ('a, 'b) Hashtbl.t -> 'a list -val collect_unprimed_vars: ctx -> expr -> string list +val collect_identifiers: ctx -> expr -> string list val collect_primed_vars: ctx -> expr -> string list diff --git a/src/method.ml b/src/method.ml index df4dab6d..98be93d4 100644 --- a/src/method.ml +++ b/src/method.ml @@ -40,6 +40,8 @@ type t = | AutoUSE | Lambdify | ENABLEDaxioms + | ENABLEDrewrites + | ENABLEDrules | LevelComparison | Trivial @@ -69,6 +71,8 @@ let timeout m = | AutoUSE -> infinity | Lambdify -> infinity | ENABLEDaxioms -> infinity + | ENABLEDrewrites -> infinity + | ENABLEDrules -> infinity | LevelComparison -> infinity | Trivial -> infinity @@ -103,6 +107,8 @@ let scale_time m s = | AutoUSE -> AutoUSE | Lambdify -> Lambdify | ENABLEDaxioms -> ENABLEDaxioms + | ENABLEDrewrites -> ENABLEDrewrites + | ENABLEDrules -> ENABLEDrules | LevelComparison -> LevelComparison | Trivial -> Trivial @@ -137,6 +143,8 @@ let pp_print_tactic ff m = | AutoUSE -> fprintf ff "(autouse)" | Lambdify -> fprintf ff "(lambdify)" | ENABLEDaxioms -> fprintf ff "(enabledaxioms)" + | ENABLEDrewrites -> fprintf ff "(enabledrewrites)" + | ENABLEDrules -> fprintf ff "(enabledrules)" | LevelComparison -> fprintf ff "(levelcomparison)" | Trivial -> fprintf ff "(trivial)" @@ -171,6 +179,8 @@ let prover_meth_of_tac tac = | AutoUSE -> (Some "autouse", None) | Lambdify -> (Some "lambdify", None) | ENABLEDaxioms -> (Some "enabledaxioms", None) + | ENABLEDrewrites -> (Some "enabledrewrites", None) + | ENABLEDrules -> (Some "enabledrules", None) | LevelComparison -> (Some "levelcomparison", None) | Trivial -> (Some "trivial", None) diff --git a/src/method.mli b/src/method.mli index cb5ead85..1068efec 100644 --- a/src/method.mli +++ b/src/method.mli @@ -28,6 +28,8 @@ type t = | AutoUSE | Lambdify | ENABLEDaxioms + | ENABLEDrewrites + | ENABLEDrules | LevelComparison | Trivial diff --git a/src/method_prs.ml b/src/method_prs.ml index 33a85733..ebb8bc57 100644 --- a/src/method_prs.ml +++ b/src/method_prs.ml @@ -48,6 +48,8 @@ and isa_method = lazy begin isa_autouse; isa_lambdify; isa_enabledaxioms; + isa_enabledrewrites; + isa_enabledrules; isa_levelcomparison; isa_trivial; ] @@ -125,6 +127,10 @@ and isa_lambdify = ident "lambdify" Lambdify and isa_enabledaxioms = ident "enabledaxioms" ENABLEDaxioms +and isa_enabledrewrites = ident "enabledrewrites" ENABLEDrewrites + +and isa_enabledrules = ident "enabledrules" ENABLEDrules + and isa_levelcomparison = ident "levelcomparison" LevelComparison and isa_trivial = ident "trivial" Trivial diff --git a/src/module/m_elab.ml b/src/module/m_elab.ml index 3420ffb0..44d98dbe 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -225,10 +225,13 @@ let lambdify_expr cx expr = let lambdify_enabled = true in let lambdify_cdot = true in let autouse = true in + let used_identifiers = Expr.Visit.collect_identifiers + cx expr in let expr = Expr.Action.lambdify cx expr ~lambdify_enabled:lambdify_enabled ~lambdify_cdot:lambdify_cdot - ~autouse:autouse in + ~autouse:autouse + ~used_identifiers:used_identifiers in expr @@ -662,6 +665,168 @@ let set_expr vis f cx = end +(* sequent's context level *) +let rec hyps_level hs = + match Deque.front hs with + | None -> 0 + | Some (h, hs) -> + let h_level = Expr.Levels.get_level h in + let hs_level = hyps_level hs in + max h_level hs_level + + +(* +The entry point below is a call `map_proof(proof, mapping, cx)` with `proof` +the proof of a theorem, `mapping = [x \in {} |-> x]` and `cx` the theorem's +context augmented with the hypotheses from the theorem's sequent. + + +HypsLevel(sequent) == + LET S == {LevelOf(hyp): hyp \in sequent.hypotheses} + IN Maximum(S) + + +procedure map_step(step, mapping, cx) { + (* Transform a step. *) + if IsAssertion(step) { + step, level, mapping, cx := map_assertion(step, mapping, cx) + } elif IsSUFFICES(step) { + step, level, mapping, cx := map_suffices(step, mapping, cx) + } elif ... ; + (* The other cases are mainly Use, Hide, + because the tlapm function `Proof.Simplify.simplify` + has transformed the proof steps. *) + return <> +} + + +procedure map_assertion(step, mapping, cx) { + (* Transform step that is an assertion. *) + sequent := step.sequent ; (* get step's sequent *) + proof := step.proof ; (* get step's proof *) + (* compute the level of the sequent, + where a sequent has expression level equal to the maximum + expression level over hypotheses and consequent *) + sequent_level := LevelOf(sequent) ; + (* compute the maximum level over hypotheses *) + hyps_level := HypsLevel(sequent) ; + (* assign to the step the level of its hypotheses + when computing the step's proof level *) + mapping := [mapping EXCEPT ![step.name] = hyps_level] ; + (* compute the level of the step's proof *) + pf_cx := ... ; (* update the context *) + proof, proof_level := map_proof(proof, mapping, pf_cx) ; + (* assign to the step a level for use outside the step's proof *) + level := IF proof_level < 2 + THEN proof_level (* actions can be proved + from state-level or constant-level facts *) + ELSE LET S == {sequent_level, proof_level} + IN Minimum(S); + (* constants or state predicates can be proved + from action-level or temporal-level facts *) + mapping := [mapping EXCEPT ![step.name] = level] ; + step := [ + name |-> step.name, + sequent |-> sequent, + proof |-> proof] ; + cx := ... ; (* update the context *) + return <> +} + + +procedure map_suffices(step, mapping, cx) { + (* Transform steps that are SUFFICES. *) + sequent = step.sequent ; (* get step's sequent *) + proof = step.proof ; (* get step's proof *) + (* compute the level of the sequent and of its hypotheses *) + sequent_level := LevelOf(sequent) ; + hyps_level := HypsLevel(sequent) ; + (* assign to the step its level + when computing the step's proof level *) + mapping := [mapping EXCEPT ![step.name] = sequent_level] ; + pf_cx := ... ; (* update the context *) + proof, proof_level := map_proof(proof, mapping, pf_cx) ; + (* assign to the step the level of its hypotheses + for use outside the step's proof *) + mapping := [mapping EXCEPT ![step.name] = hyps_level] ; + step := [ + name |-> step.name, + sequent |-> sequent, + proof |-> proof] ; + cx := ... ; (* update the context *) + (* return the SUFFICES proof's level as level for + the QED of the old goal (enclosing PROOF) *) + return <> +} + + +procedure map_proof(proof, mapping, cx) { + (* at the stage in tlapm where this soundness check is run, + the proof has been transformed so that all leaf proofs are + OBVIOUS, i.e., all BY proofs have been converted to + USE, HIDE, and OBVIOUS *) + if IsObvious(proof) { + proof, proof_level := map_obvious_proof(proof, mapping, cx) + } else { + proof, proof_level := map_steps_proof(proof, mapping, cx) + } ; + return <> +} + + +procedure map_obvious_proof(proof, mapping, cx) { + max_level := 0 ; + ctx := cx ; + while (Len(ctx) > 0) { + hyp := Head(ctx) ; + ctx := Tail(ctx) ; + if IsVisibleFact(hyp) { + expr := GetExprOfFact(hyp) ; + (* This area is more complex in OCaml, + and is implemented using pattern matching. + This area contained bugs that have been + now corrected (I think). *) + expr_level := LevelOf(expr) ; + max_level := LET S == {expr_level, max_level} + IN Maximum(S) + } + } ; + (* This annotation is used later, when processing each + proof obligation, to decide whether a step that uses + `ENABLEDrules` depends on a fact of too high level, + and fail with a suitable message. + *) + if (HasENABLEDrules(cx) /\ (max_level > 1)) { + proof := Annotate(proof, enabledaxioms_property, FALSE) + } else { + proof := Annotate(proof, enabledaxioms_property, TRUE) + } ; + return <> +} + + +procedure map_steps_proof(proof, mapping, cx) { + remaining_steps := proof ; (* a tuple of steps *) + steps := << >> ; + proof_level := None ; + while (Len(remaining_steps) > 0) { + step := Head(remaining_steps) ; + remaining_steps := Tail(remaining_steps) ; + step, level, mapping, cx := map_step(step, mapping, cx) ; + steps := Append(steps, step) ; + (* The level of the entire proof is equal to + the level of the proof of the first SUFFICES step or to + the level of the QED step *) + if ( (proof_level = None) /\ \/ IsSUFFICES(step) + \/ IsQED(step) ) { + proof_step := level + } + } ; + return <> +} +*) + + let check_enabled_axioms_map = object (self: 'self) inherit [int ref * (Proof.T.step * hyp Deque.dq * int) StringMap.t] Proof.Visit.map as super @@ -671,8 +836,11 @@ let check_enabled_axioms_map = object (self: 'self) | Obvious -> self#check_usable pf scx {facts=[]; defs=[]} false | By (usable, onl) -> + assert false (* after Proof.Simplify.simplify *) + (* let pf = By (self#usable scx usable, onl) @@ pf in self#check_usable pf scx usable onl + *) | Steps (inits, qed) -> let (scx, inits) = self#steps scx inits in let qed_prf = self#proof scx (get_qed_proof qed) in @@ -698,15 +866,6 @@ let check_enabled_axioms_map = object (self: 'self) stepnm @@ st, At false @@ nowhere) @@ st, Proof Always, Visible, Local) @@ st) in - (* sequent's context level *) - let rec hyps_level hs = - match Deque.front hs with - | None -> 0 - | Some (h, hs) -> - let h_level = Expr.Levels.get_level h in - let hs_level = hyps_level hs in - max h_level hs_level - in match st.core with | Forget m -> let nfacts = Deque.size cx in @@ -726,8 +885,22 @@ let check_enabled_axioms_map = object (self: 'self) | Use ({defs = []; facts = [f]}, only) -> let tm = Always in let cx = Deque.snoc cx (Fact (f, Visible, tm) @@ f) in - (((level, sm), cx), - Use ({defs = []; facts = [f]}, only) @@ st) + let scx = ((level, sm), cx) in + let use = Use ({defs = []; facts = [f]}, only) @@ st in + (scx, use) + | Use ({facts = []} as usables, only) -> + let usables_ = self#usable scx usables in + let cx = List.fold_left (set_defn Visible) cx usables.defs in + let scx = ((level, sm), cx) in + let use = Use (usables_, only) @@ st in + (scx, use) + | Use (usables, only) -> + Util.eprintf ~at:st "%s" + ("USE usables with number of facts: " ^ + (string_of_int (List.length usables.facts)) ^ + ", and number of DEFS: " ^ + (string_of_int (List.length usables.defs))); + assert false (* after `Proof.Simplify.simplify` *) | Assert (sq, prf) -> (* ignore (self#sequent scx sq) ; *) let sq_expr = Expr.Levels.compute_level cx (noprops (Sequent sq)) in @@ -746,9 +919,12 @@ let check_enabled_axioms_map = object (self: 'self) let scx = Proof.Visit.bump scx 1 in let scx = adj_step scx in let scx = Proof.Visit.bump scx 1 in + (* visit proof of assertion *) self#proof scx prf in + (* context changes *) let scx = adj_step scx in let scx = Proof.Visit.bump scx 1 in + (* retrieve context *) let ((_, sm), cx) = scx in (* level computation *) let sq_level = Expr.Levels.get_level sq_expr in @@ -768,8 +944,9 @@ let check_enabled_axioms_map = object (self: 'self) *) (* store (assumption) level of sequent and its proof *) let sm = StringMap.add stepnm (st, cx, !level) sm in - (((level, sm), cx), - Assert (sq, prf) @@ st) + let scx = ((level, sm), cx) in + let assertion = Assert (sq, prf) @@ st in + (scx, assertion) | Suffices (sq, prf) -> (* ignore (self#sequent scx sq) ; *) let sq_expr = Expr.Levels.compute_level cx (noprops (Sequent sq)) in @@ -783,133 +960,135 @@ let check_enabled_axioms_map = object (self: 'self) let scx = Proof.Visit.bump scx 1 in let ((_, sm), cx) = scx in let sq_level = Expr.Levels.get_level sq_expr in - level := sq_level; - let sm = StringMap.add stepnm (st, cx, !level) sm in + let sm = StringMap.add stepnm (st, cx, sq_level) sm in let scx = ((proof_level, sm), cx) in self#proof scx prf in + (* assign to the proof that contains this SUFFICES step + (`level := `) the level of the proof of the SUFFICES step, + which is equal to `proof_level` *) + level := !proof_level; let level_hyps = hyps_level sq.context in (* store (assumption) level of sequent context *) let sm = StringMap.add stepnm (st, cx, level_hyps) sm in - let scx = ((proof_level, sm), cx) in + (* Provide fresh `remaining_steps_level` as `ref` to + the following steps, because the level of the proof that + contains this SUFFICES step is equal to the value + above of `proof_level`. + *) + let remaining_steps_level = ref 0 in + let scx = ((remaining_steps_level, sm), cx) in (* context changes *) let scx = Expr.Visit.adjs scx (Deque.to_list sq.context) in let scx = Proof.Visit.bump scx 1 in let scx = adj_step scx in let scx = Proof.Visit.bump scx 1 in - (scx, - Suffices (sq, prf) @@ st) + let suffices = Suffices (sq, prf) @@ st in + (scx, suffices) | Pcase _ | Have _ | Take _ | Witness _ | Pick _ -> assert false (* after `Proof.Simplify.simplify` *) - | _ -> - let sm = StringMap.add stepnm (st, cx, 1) sm in - let scx = ((level, sm), cx) in - super#step scx st + | Define dfs -> + let (scx, dfs) = self#defns scx dfs in + (scx, Define dfs @@ st) method check_usable pf ((level, sm), cx) usables only = + (* The context `cx` contains all usable facts, + because `Proof.Simplify.simplify` has been called. + *) + assert (usables.facts = []); + assert (usables.defs = []); + (* Also, `usables` is empty, because `Proof.Simplif.simplify` + has been called. + *) + assert (not only); (* because this is an `Obvious` proof *) (* computation of proof's assumption expression level *) + let max_level = ref 0 in let check_fact cx fact = begin match fact.core with | Ix n -> begin - let hyp = E_t.get_val_from_id cx n in - let cx_ = Expr.T.cx_front cx n in + let hyp = E_t.get_val_from_id cx n in + let cx_ = Expr.T.cx_front cx n in match hyp.core with + (* TODO: what form do references to the theorem's own + assumptions have at this point in proof processing ? + *) | Fact (expr, Visible, _) -> print_string (Expr.Fmt.string_of_expr cx_ expr); assert false - (* checking referenced steps *) - | Defn ({core=Operator (name, _)}, _, Visible, _) -> + (* checking referenced steps and visible defined operators *) + | Defn ({core=Operator (name, e)}, _, Visible, _) -> (* print_string "Step number:\n"; print_string name.core; *) let nm = name.core in + (* is this a step number ? *) if (String.contains_from nm 0 '<') then begin if (StringMap.mem nm sm) then begin - let (step, cx, step_level) = StringMap.find nm sm in - level := max step_level !level + let (step, cx, step_level) = + StringMap.find nm sm in + max_level := max step_level !max_level end end - | _ -> () + else begin + let e = Expr.Levels.compute_level cx_ e in + let expr_level = Expr.Levels.get_level e in + max_level := max expr_level !max_level + end + (* hidden defined operators, which may be used as symbols + in assumptions *) + | Defn ({core=Operator (name, e)}, _, Hidden, _) -> + let e = Expr.Levels.compute_level cx_ e in + let expr_level = Expr.Levels.get_level e in + max_level := max expr_level !max_level + | Defn ({core=Recursive _}, _, _, _) -> + assert false (* not implemented *) + | Defn ({core=Instance _}, _, _, _) -> + assert false (* INSTANCE expanded + at this point. *) + | Defn ({core=Bpragma _}, _, _, _) -> + () (* Backend pragmas do not contribute + to the proof level, because they are + defined as `TRUE`. *) + | Fact (_, Hidden, _) -> + () (* Hidden facts are not usable in + the proof, so they do not contribute to + the proof level. *) + | Fresh _ | Flex _ -> + () (* Declarations of operators do not have + a notion of being usable in the proof, + so they do not contribute to the + proof level. *) end (* checking of expressions in the BY statement *) | _ -> let fact = Expr.Levels.compute_level cx fact in let expr_level = Expr.Levels.get_level fact in - level := max expr_level !level + max_level := max expr_level !max_level end in (* checking assumptions in the step's context *) - if not only then begin let check_assumptions n hyp = match hyp.core with | Fact ({core=At _}, _, _) -> () (* dummy steps *) + (* theorems, expressions from assumptions *) | Fact (expr, Visible, _) -> let cx_ = Expr.T.cx_front cx ((Deque.size cx) - n) in (* print_string "Fact:\n"; print_string (Expr.Fmt.string_of_expr cx_ expr); + print_string "\n"; *) check_fact cx_ expr | _ -> () in - Deque.iter check_assumptions cx - end; + Deque.iter check_assumptions cx; + level := !max_level; - let max_level = ref 0 in - let check_step cx fact = - begin match fact.core with - | Ix n -> begin - let hyp = E_t.get_val_from_id cx n in - match hyp.core with - | Defn ({core=Operator (name, _)}, _, Visible, _) -> - let nm = name.core in - (* is this a step number ? *) - if (String.contains_from nm 0 '<') then begin - if (StringMap.mem nm sm) then begin - (* print_string ("Found stored step " ^ nm ^ "\n"); *) - let (step, cx, step_level) = StringMap.find nm sm in - max_level := max step_level !max_level - end end - | _ -> () - end - | _ -> - let fact = Expr.Levels.compute_level cx fact in - let expr_level = Expr.Levels.get_level fact in - max_level := max expr_level !max_level - end - in - let check_steps n hyp = - match hyp.core with - (* - | Defn ({core=Operator (name, _)}, _, Visible, _) -> - let nm = name.core in - (* is this a step number ? *) - if (String.contains_from nm 0 '<') then begin - if (StringMap.mem nm sm) then begin - (* print_string ("Found stored step " ^ nm ^ "\n"); *) - let (step, cx, step_level) = StringMap.find nm sm in - (* - if (step_level > 1) && (!max_level <= 1) then - print_string nm; - *) - max_level := max step_level !max_level; - end end - *) - | Fact ({core=At _}, _, _) -> () (* dummy steps *) - | Fact (expr, Visible, _) -> - let cx_ = Expr.T.cx_front cx ((Deque.size cx) - n) in - (* - print_string (Expr.Fmt.string_of_expr cx_ expr); - print_string "\n"; - *) - check_step cx_ expr - | _ -> () - in - (* find proof directive in the context *) + (* search for proof directive `ENABLEDrules` in the context *) let found = ref false in let find_proof_directive n hyp = match hyp.core with @@ -920,7 +1099,8 @@ let check_enabled_axioms_map = object (self: 'self) let hyp = E_t.get_val_from_id cx_ n in match hyp.core with | Defn ({core=Bpragma (name, _, _)}, _, _, _) -> - found := !found || (name.core = "ENABLEDaxioms") + if (name.core = "ENABLEDrules") then + found := true | _ -> () end | _ -> () @@ -928,22 +1108,19 @@ let check_enabled_axioms_map = object (self: 'self) | _ -> () in Deque.iter find_proof_directive cx; - - if !found then begin - (* print_string "Found ENABLEDaxioms\n"; *) - Deque.iter check_steps cx; - if (!max_level > 1) then - begin - Util.eprintf ~at:pf "%s" - ("ENABLEDaxioms depends on assumption of expression " ^ - "level > 1"); - (* - Util.eprintf "%a@" (Proof.Fmt.pp_print_proof (cx, Ctx.dot)) pf - *) - assign pf enabledaxioms false - end - else - assign pf enabledaxioms true + (* + if !found then + print_string "Found ENABLEDrules\n"; + *) + if (!found && (!max_level > 1)) then + begin + Util.eprintf ~at:pf "%s" + ("ENABLEDrules depends on assumption of expression " ^ + "level > 1"); + (* + Util.eprintf "%a@" (Proof.Fmt.pp_print_proof (cx, Ctx.dot)) pf + *) + assign pf enabledaxioms false end else assign pf enabledaxioms true @@ -1044,7 +1221,7 @@ let check_enabled_axioms_usage = object (self: 'self) let hyp = E_t.get_val_from_id cx_ n in match hyp.core with | Defn ({core=Bpragma (name, _, _)}, _, _, _) -> - found := !found || (name.core = "ENABLEDaxioms") + found := !found || (name.core = "ENABLEDrules") | _ -> () end | _ -> () @@ -1119,6 +1296,12 @@ let rec normalize mcx cx m = | None -> (cx, sq) in + (* compute level of sequent *) + let sq_expr = Expr.Levels.compute_level cx (noprops (Sequent sq)) in + let sq = match sq_expr.core with + | Sequent sq -> sq + | _ -> assert false + in (* add the theorem's hypotheses to the context `cx` within the theorem's proof *) @@ -1149,8 +1332,10 @@ let rec normalize mcx cx m = (* ((ref 0, StringMap.empty), cx) pf; *) let has = check_enabled_axioms_usage#find_enabled_axioms cx pf in - let pf = if has then check_enabled_axioms_map#proof - ((ref 0, StringMap.empty), cx) pf else pf in + let pf = if has then begin + check_enabled_axioms_map#proof + ((ref 0, StringMap.empty), cx) pf + end else pf in pf end else diff --git a/test/fast/enabled_cdot/AutoUSE_fingerprint/AutoUSE_fingerprint_test.tla b/test/fast/enabled_cdot/AutoUSE_fingerprint/AutoUSE_fingerprint_test.tla new file mode 100644 index 00000000..7a3e417b --- /dev/null +++ b/test/fast/enabled_cdot/AutoUSE_fingerprint/AutoUSE_fingerprint_test.tla @@ -0,0 +1,11 @@ +---- MODULE AutoUSE_fingerprint_test ---- + +========================================= +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 3 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/AutoUSE_fingerprint/v1.tla b/test/fast/enabled_cdot/AutoUSE_fingerprint/v1.tla new file mode 100644 index 00000000..7a784f44 --- /dev/null +++ b/test/fast/enabled_cdot/AutoUSE_fingerprint/v1.tla @@ -0,0 +1,24 @@ +---- MODULE temp ---- +(* Test that proof obligations with AutoUSE +are fingerprinted after automated expansion +of definitions. + +Run `tlapm` to create fingerprints, +edit the input file to make the proof obligation unprovable, +and re-run `tlapm` to ensure that the saved fingerprint does +not shadow the change of the defined operator `A` that is +expanded by `AutoUSE`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +A == x' = 1 + + +THEOREM ENABLED A +BY ExpandENABLED, AutoUSE + +==================================== diff --git a/test/fast/enabled_cdot/AutoUSE_fingerprint/v2.tla b/test/fast/enabled_cdot/AutoUSE_fingerprint/v2.tla new file mode 100644 index 00000000..71b41edb --- /dev/null +++ b/test/fast/enabled_cdot/AutoUSE_fingerprint/v2.tla @@ -0,0 +1,14 @@ +---- MODULE temp ---- +EXTENDS TLAPS + + +VARIABLE x + + +A == x' # x' + + +THEOREM ENABLED A +BY ExpandENABLED, AutoUSE + +==================================== diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/ENABLEDaxioms_conj_fingerprinting_test.tla b/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/ENABLEDaxioms_conj_fingerprinting_test.tla new file mode 100644 index 00000000..b8598739 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/ENABLEDaxioms_conj_fingerprinting_test.tla @@ -0,0 +1,11 @@ +----------------- MODULE ENABLEDaxioms_conj_fingerprinting_test ---------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -r temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v1.tla b/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v1.tla new file mode 100644 index 00000000..128e06c6 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v1.tla @@ -0,0 +1,16 @@ +----------------- MODULE temp ---------------- +(* Test fingerprint interaction for `ENABLEDaxioms`. *) +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x' +B == y + + +THEOREM ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +BY ENABLEDaxioms DEF A + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v2.tla b/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v2.tla new file mode 100644 index 00000000..336a0186 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v2.tla @@ -0,0 +1,15 @@ +----------------- MODULE temp ---------------- +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x' +B == y' + + +THEOREM ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +BY ENABLEDaxioms DEF A + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_conj_hidden_actions_test.tla b/test/fast/enabled_cdot/ENABLEDaxioms_conj_hidden_actions_test.tla new file mode 100644 index 00000000..2f49027f --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_hidden_actions_test.tla @@ -0,0 +1,20 @@ +------------------ MODULE ENABLEDaxioms_conj_hidden_actions_test --------------- +(* Test that when in `ENABLED (A /\ B)` the operator `A` is hidden and of +action level, then the proof directive `ENABLEDaxioms` does not distribute +`ENABLED` over conjunction. +*) +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x' +B == y' + + +THEOREM ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +BY ENABLEDaxioms + +================================================================================ +stderr: obligations failed diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_conj_test.tla b/test/fast/enabled_cdot/ENABLEDaxioms_conj_test.tla new file mode 100644 index 00000000..ade29ca0 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_test.tla @@ -0,0 +1,42 @@ +-------------------------- MODULE ENABLEDaxioms_conj_test ---------------------- +(* Test a variety of cases for `ENABLED (A /\ B)` using the proof directive +`ENABLEDaxioms`. +*) +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x' +B == y' +C == x + + +THEOREM ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +BY ENABLEDaxioms DEF A, B + + +(* symmetric to the previous theorem *) +THEOREM (ENABLED A /\ ENABLED B) <=> ENABLED (A /\ B) +BY ENABLEDaxioms DEF A, B + + +THEOREM ENABLED (A /\ C) <=> (ENABLED A /\ ENABLED C) +BY ENABLEDaxioms DEF A + + +(* symmetric to the previous theorem *) +THEOREM (ENABLED A /\ ENABLED C) <=> ENABLED (A /\ C) +BY ENABLEDaxioms DEF A + + +THEOREM ENABLED (B /\ C) <=> (ENABLED B /\ ENABLED C) +BY ENABLEDaxioms DEF B + + +(* symmetric to the previous theorem *) +THEOREM (ENABLED B /\ ENABLED C) <=> ENABLED (B /\ C) +BY ENABLEDaxioms DEF B + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_fail_test.tla b/test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_fail_test.tla new file mode 100644 index 00000000..d719dba8 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_fail_test.tla @@ -0,0 +1,20 @@ +------------------ MODULE ENABLEDaxioms_conj_visible_actions_test -------------- +(* Test that when in `ENABLED (A /\ B)` the operators are visible, but have +primed variables in common, then the proof directive `ENABLEDaxioms` does not +distribute `ENABLED` over conjunction. +*) +EXTENDS TLAPS + + +VARIABLE x + + +A == x' +B == x' + + +THEOREM ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +BY ENABLEDaxioms DEF A, B + +================================================================================ +stderr: obligations failed diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_test.tla b/test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_test.tla new file mode 100644 index 00000000..930ca06d --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_test.tla @@ -0,0 +1,18 @@ +------------------ MODULE ENABLEDaxioms_conj_visible_actions_test -------------- +(* Test that when in `ENABLED (A /\ B)` the operators are visible, then the +proof directive `ENABLEDaxioms` distributes `ENABLED` over conjunction. +*) +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x' +B == y' + + +THEOREM ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +BY ENABLEDaxioms DEF A, B + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_test.tla b/test/fast/enabled_cdot/ENABLEDaxioms_test.tla index ae0ed2a4..260a5210 100644 --- a/test/fast/enabled_cdot/ENABLEDaxioms_test.tla +++ b/test/fast/enabled_cdot/ENABLEDaxioms_test.tla @@ -1,310 +1,83 @@ ------------------------- MODULE ENABLEDaxioms_test ---------------------------- -(* Unit tests for the implementation of proof rules about `ENABLED`. *) +(* Unit tests for the implementation of axioms about `ENABLED`. *) EXTENDS TLAPS (* This statement declares three variables. *) -VARIABLE x, y, z +VARIABLE x, y P == x = 1 (* A state predicate. *) -A == x' = 1 /\ y' = 1 (* An action with primed variables. *) -B == z' = 1 (* Another action with primed variables, such that the set of +A == x' = 1 (* An action with a primed variable. *) +B == y' = 1 (* Another action with primed variables, such that the set of primed variables of action A is disjoint from the set of primed variables of action B. *) -R == y' = 1 /\ x' = 1 (* An action equivalent to action A. *) +R(z) == z (* An operator that takes a parameter. *) --------------------------------------------------------------------------------- -(* Proving that a state predicate can be moved outside the scope of ENABLED, -i.e., that from - P \in BOOLEAN, - A \in BOOLEAN, - ENABLED (P /\ A), - P is a state predicate -we deduce - P /\ ENABLED A -The premises P \in BOOLEAN, A \in BOOLEAN, and ENABLED (P /\ A) must appear -as separate proof steps and listed in the BY statement where ENABLEDaxioms -appears. The premise that P is a state predicate is checked automatically by -TLAPS. +-------------------------------------------------------------------------------- +(* ENABLED distributes over disjunction. -If the premises do not appear in this form, then the proof will not -succeed, because TLAPS checks the syntactic form of each premise, including the -levels of the expressions. +In more detail, we deduce + ENABLED (A \/ B) <=> (ENABLED A \/ ENABLED B) *) -THEOREM - ASSUME P - PROVE P /\ ENABLED A -PROOF -<1>1. P \in BOOLEAN - BY DEF P -<1>2. A \in BOOLEAN - BY DEF A -<1>3. ENABLED (P /\ A) - (* With the proof directives ExpandENABLED and AutoUSE the expression - ENABLED (P /\ A) is converted first to ENABLED (P /\ x' = 1 /\ y' = 1) and - then to (\E u, v: P /\ u = 1 /\ v = 1), which is equivalent to P, - so implied by the assumption P (no need to expand the definition of P). - *) - BY ExpandENABLED, AutoUSE -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms +THEOREM ENABLED (A \/ B) <=> (ENABLED A \/ ENABLED B) +BY ENABLEDaxioms +THEOREM (ENABLED A \/ ENABLED B) <=> ENABLED (A \/ B) +BY ENABLEDaxioms -(* Proving that a state predicate can be moved inside the scope of ENABLED, -i.e., that from - P \in BOOLEAN, - A \in BOOLEAN, - P /\ ENABLED A, - P is a state predicate -we deduce - ENABLED (P /\ A) - -The premises P \in BOOLEAN, A \in BOOLEAN and P /\ ENABLED A must appear as -separate proof steps and listed in the BY statement where ENABLEDaxioms appears. -The premise that P is a state predicate is checked automatically by TLAPS. - -If the premises do not appear in this form, then the proof will not succeed, -because TLAPS checks the syntactic form of each premise, including the levels -of the expressions. -*) -THEOREM - ASSUME P - PROVE ENABLED (P /\ A) -PROOF -<1>1. P \in BOOLEAN - BY DEF P -<1>2. A \in BOOLEAN - BY DEF A -<1>3. P /\ ENABLED A - <2>1. ENABLED A - (* AutoUSE expands action A, because it contains primed variables and - is in the scope of ENABLED, to yield the expression - ENABLED (x' = 1 /\ y' = 1). ExpandENABLED converts this expression to - (\E u, v: u = 1 /\ v = 1), which is valid. - *) - BY ExpandENABLED, AutoUSE - <2> QED - BY <2>1 -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms -------------------------------------------------------------------------------- -(* Proving that ENABLED distributes over conjunction for actions with disjoint -sets of primed variables, i.e., that from - A \in BOOLEAN, - B \in BOOLEAN, - ENABLED (A /\ B), - A and B have disjoint sets of primed variables -we deduce - (ENABLED A) /\ ENABLED B +(* ENABLED commutes with existential quantification. -The premises A \in BOOLEAN, B \in BOOLEAN, and ENABLED (A /\ B) must appear as -separate proof steps, and listed in the BY statement where ENABLEDaxioms -appears. The premise that A and B have disjoint sets of primed variables is -checked automatically by TLAPS. +This axiom allows renaming of the bound constant, and +requires that the quantifier bounds be identical and +state predicates or constants, +and that the quantified expressions be identical. *) +THEOREM ENABLED (\E i \in {1, 2}: R(i)) <=> + \E i \in {1, 2}: ENABLED R(i) +BY ENABLEDaxioms +THEOREM (\E i \in {1, 2}: ENABLED R(i)) <=> + ENABLED (\E i \in {1, 2}: R(i)) +BY ENABLEDaxioms -THEOREM - (ENABLED A) /\ ENABLED B -PROOF -<1>1. A \in BOOLEAN - BY DEF A -<1>2. B \in BOOLEAN - BY DEF B -<1>3. ENABLED (A /\ B) - (* The proof directive AutoUSE expands the definitions of operators A and B - because they are actions in the scope of ENABLED. The result is the - expression ENABLED (x' = 1 /\ y' = 1 /\ z' = 1). The proof directive - ExpandENABLED converts this expression to the expression - (\E u, v, w: u = 1 /\ v = 1 /\ w = 1). - *) - BY ExpandENABLED, AutoUSE -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms - - -(* Proving that ENABLED can be factored out of conjunction for actions with -disjoint sets of primed variables, i.e., that from - A \in BOOLEAN, - B \in BOOLEAN, - (ENABLED A) /\ ENABLED B, - A and B have disjoint sets of primed variables -we deduce - ENABLED (A /\ B) - -The premises A \in BOOLEAN, B \in BOOLEAN, and (ENABLED A) /\ ENABLED B must -appear as separate proof steps, and listed in the BY statement where -ENABLEDaxioms appears. The premise that A and B have disjoint sets of primed -variables is checked automatically by TLAPS. -*) -THEOREM - ENABLED (A /\ B) -PROOF -<1>1. A \in BOOLEAN - BY DEF A -<1>2. B \in BOOLEAN - BY DEF B -<1>3. (ENABLED A) /\ (ENABLED B) - (* The proof directive AutoUSE expands the definitions of operators A and B - because they are actions in the scope of ENABLED. The result is the - expression (ENABLED (x' = 1 /\ y' = 1)) /\ (ENABLED (z' = 1)). - The proof directive ExpandENABLED converts this expression to the - expression (\E u, v: u = 1 /\ v = 1) /\ (\E w: w = 1). - *) - BY ExpandENABLED, AutoUSE -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms -------------------------------------------------------------------------------- +(* ENABLED distributes over conjunction of actions +with disjoint sets of primed variables. -(* This theorem is similar to the previous one, with the difference that P -is a state predicate, instead of an action as A was. So the definition of P -does not contain any primed variables, thus its set of primed variables is -obviously disjoint from the set of primed variables of action B. -*) -THEOREM - ASSUME P - PROVE ENABLED (P /\ B) -PROOF -<1>1. P \in BOOLEAN - BY DEF P -<1>2. B \in BOOLEAN - BY DEF B -<1>3. (ENABLED P) /\ ENABLED B - <2>1. ENABLED P - BY ExpandENABLED, AutoUSE - <2>2. ENABLED B - BY ExpandENABLED, AutoUSE - <2> QED - BY <2>1, <2>2 -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms - --------------------------------------------------------------------------------- -(* Proving that ENABLED can be factored out of disjunction, i.e., that from - A \in BOOLEAN, - B \in BOOLEAN, - (ENABLED A) \/ ENABLED B +In more detail, from + A and B have disjoint sets of primed variables we deduce - ENABLED (A \/ B) - -The premises A \in BOOLEAN, B \in BOOLEAN, and (ENABLED A) \/ ENABLED B must -appear as separate proof steps, and be listed in the BY statement where the -proof directive ENABLEDaxioms appears. + ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +The premise that A and B have disjoint sets of primed variables +is automatically checked by TLAPS. +The *) -THEOREM - ENABLED (A \/ B) -PROOF -<1>1. A \in BOOLEAN - BY DEF A -<1>2. B \in BOOLEAN - BY DEF B -<1>3. (ENABLED A) \/ (ENABLED B) - <2>1. ENABLED A - BY ExpandENABLED, AutoUSE - <2>2. ENABLED B - BY ExpandENABLED, AutoUSE - <2> QED - BY <2>1, <2>2 -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms - +THEOREM ENABLED (A /\ B) <=> (ENABLED A /\ ENABLED B) +BY ENABLEDaxioms DEF A, B -(* Proving that ENABLED distributes over the disjunction of actions, i.e., that -from - A \in BOOLEAN, - B \in BOOLEAN, - ENABLED (A \/ B) -we deduce - (ENABLED A) \/ ENABLED B +THEOREM (ENABLED A /\ ENABLED B) <=> ENABLED (A /\ B) +BY ENABLEDaxioms DEF A, B -The premises A \in BOOLEAN, B \in BOOLEAN, ENABLED (A \/ B) need to appear as -separate proof steps, and be listed in the BY statement where the proof -directive ENABLEDaxioms appears. -*) -THEOREM - (ENABLED A) \/ (ENABLED B) -PROOF -<1>1. A \in BOOLEAN - BY DEF A -<1>2. B \in BOOLEAN - BY DEF B -<1>3. ENABLED (A \/ B) - BY ExpandENABLED, AutoUSE -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms -------------------------------------------------------------------------------- -(* Proving that equality of Boolean-valued actions implies equivalence of -enabledness of these actions, i.e., that from - A \in BOOLEAN, - R \in BOOLEAN, - A = R -we deduce - (ENABLED A) <=> (ENABLED R) - -The premises A \in BOOLEAN, R \in BOOLEAN, and A = R must appear as separate -proof steps, and be listed in the BY statement where the proof directive -ENABLEDaxioms appears. -*) - +(* State predicates can be pulled outside of ENABLED. -THEOREM - (ENABLED A) <=> (ENABLED R) -PROOF -<1>1. A \in BOOLEAN - BY DEF A -<1>2. R \in BOOLEAN - BY DEF R -<1>3. A = R - BY DEF A, R -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms - --------------------------------------------------------------------------------- -(* Proving that the equivalence of actions implies the equivalence of -enabledness of these actions, i.e., that from - A <=> R +In more detail, from + P has at most state level we deduce - (ENABLED A) <=> ENABLED R - -The premise A <=> R needs to appear as a separate proof step, and be listed in -the BY statement where the proof directive ENABLEDaxioms appears. + ENABLED (P /\ A) <=> (P /\ ENABLED A) +The premise about the level of P is automatically checked by TLAPS. *) -THEOREM - (ENABLED A) <=> ENABLED R -PROOF -<1>1. A <=> R - BY DEF A, R -<1> QED - BY <1>1, ENABLEDaxioms +THEOREM ENABLED (P /\ A) <=> (P /\ ENABLED A) +BY ENABLEDaxioms --------------------------------------------------------------------------------- -(* Proving that the implication of actions implies the implication of the -enabledness of these actions, i.e., that from - A \in BOOLEAN, - R \in BOOLEAN, - A => R -we deduce - (ENABLED A) => ENABLED R +THEOREM (P /\ ENABLED A) <=> ENABLED (P /\ A) +BY ENABLEDaxioms -The premises A \in BOOLEAN, R \in BOOLEAN, and A => R must appear as separate -proof steps, and be listed in the BY statement where the proof directive -ENABLEDaxioms appears. -*) -THEOREM - (ENABLED A) => ENABLED R -PROOF -<1>1. A \in BOOLEAN - BY DEF A -<1>2. R \in BOOLEAN - BY DEF R -<1>3. A => R - BY DEF A, R -<1> QED - BY <1>1, <1>2, <1>3, ENABLEDaxioms ================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/ENABLEDrewrites_assignment_level_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/ENABLEDrewrites_assignment_level_fingerprint_test.tla new file mode 100644 index 00000000..d57f14b9 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/ENABLEDrewrites_assignment_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +------------ MODULE ENABLEDrewrites_assignment_level_fingerprint_test ---------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v1.tla new file mode 100644 index 00000000..4fa97e38 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v1.tla @@ -0,0 +1,17 @@ +------------ MODULE temp ---------- +(* Test that changing the level of the right-hand side of equality within +`ENABLED` also changes the result of the proof directive `ENABLEDrewrites`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +A == x + + +THEOREM (ENABLED (x' = A)) = TRUE +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v2.tla new file mode 100644 index 00000000..8d1559de --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v2.tla @@ -0,0 +1,14 @@ +------------ MODULE temp ---------- +EXTENDS TLAPS + + +VARIABLE x + + +A == x' + + +THEOREM (ENABLED (x' = A)) = TRUE +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/ENABLEDrewrites_bpragma_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/ENABLEDrewrites_bpragma_fingerprint_test.tla new file mode 100644 index 00000000..4f72c787 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/ENABLEDrewrites_bpragma_fingerprint_test.tla @@ -0,0 +1,11 @@ +--------------- MODULE ENABLEDrewrites_bpragma_fingerprint_test ---------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v1.tla new file mode 100644 index 00000000..2b49e7dc --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v1.tla @@ -0,0 +1,22 @@ +--------------- MODULE temp ---------------- +(* Test that the names of proof directives that appear in the `BY` statement +are recorded in the fingerprint. Recording them ensures that changing the +proof directive(s) that is(are) listed in the `BY` statement also changes the +fingerprint of the proof obligation. + +Previously, the names of proof directives (bpragmas) were not recorded in the +fingerprint. As a result, a proof obligation could be proved in a run of `tlapm` +and the proof directive then changed to a different one, for which the proof +obligation would not get proved, but the fingerprint remained unchanged, so +the proof obligation was erroneously proved by subsequent runs of `tlapm`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +THEOREM ENABLED (x' = 1) +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v2.tla new file mode 100644 index 00000000..699295d3 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v2.tla @@ -0,0 +1,11 @@ +--------------- MODULE temp ---------------- +EXTENDS TLAPS + + +VARIABLE x + + +THEOREM ENABLED (x' = 1) +BY ENABLEDaxioms + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/ENABLEDrewrites_case_level_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/ENABLEDrewrites_case_level_fingerprint_test.tla new file mode 100644 index 00000000..b5ecf44f --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/ENABLEDrewrites_case_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +-------------- MODULE ENABLEDrewrites_case_level_fingerprint_test -------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v1.tla new file mode 100644 index 00000000..b81e449c --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v1.tla @@ -0,0 +1,18 @@ +-------------- MODULE temp -------------- +(* Test that changing the level of the test expression in a `CASE` conditional +also changes the result of the proof directive `ENABLEDrewrites`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +p1 == x +a1 == x' + + +THEOREM (ENABLED CASE p1 -> a1) = CASE p1 -> ENABLED a1 +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v2.tla new file mode 100644 index 00000000..4d0e31e0 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v2.tla @@ -0,0 +1,15 @@ +-------------- MODULE temp -------------- +EXTENDS TLAPS + + +VARIABLE x + + +p1 == x' +a1 == x' + + +THEOREM (ENABLED CASE p1 -> a1) = CASE p1 -> ENABLED a1 +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/ENABLEDrewrites_conj_level_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/ENABLEDrewrites_conj_level_fingerprint_test.tla new file mode 100644 index 00000000..0f957342 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/ENABLEDrewrites_conj_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +-------------- MODULE ENABLEDrewrites_conj_level_fingerprint_test -------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v1.tla new file mode 100644 index 00000000..9eb29b90 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v1.tla @@ -0,0 +1,18 @@ +-------------- MODULE temp -------------- +(* Test that changing the level of the conjuncts in a conjunction within +`ENABLED` also changes the result of the proof directive `ENABLEDrewrites`. +*) +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x +B == y' + + +THEOREM (ENABLED (A /\ B)) = (A /\ ENABLED B) +BY ENABLEDrewrites DEF B + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v2.tla new file mode 100644 index 00000000..8ccbc59e --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v2.tla @@ -0,0 +1,15 @@ +-------------- MODULE temp -------------- +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x' +B == y' + + +THEOREM (ENABLED (A /\ B)) = (A /\ ENABLED B) +BY ENABLEDrewrites DEF B + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/ENABLEDrewrites_exist_level_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/ENABLEDrewrites_exist_level_fingerprint_test.tla new file mode 100644 index 00000000..91dbf2de --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/ENABLEDrewrites_exist_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +------------- MODULE ENABLEDrewrites_exist_level_fingerprint_test -------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v1.tla new file mode 100644 index 00000000..c750bf10 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v1.tla @@ -0,0 +1,19 @@ +------------- MODULE temp -------------- +(* Test that changing the level of the bound in `\E` also changes the result of +the proof directive `ENABLEDrewrites`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +R(i) == x' +C == {1, 2} +W == {x'} + + +THEOREM (ENABLED (\E i \in C: R(i))) = \E i \in C: ENABLED R(i) +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v2.tla new file mode 100644 index 00000000..d83d3679 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v2.tla @@ -0,0 +1,16 @@ +------------- MODULE temp -------------- +EXTENDS TLAPS + + +VARIABLE x + + +R(i) == x' +C == {1, 2} +W == {x'} + + +THEOREM (ENABLED (\E i \in W: R(i))) = \E i \in W: ENABLED R(i) +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/ENABLEDrewrites_mem_level_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/ENABLEDrewrites_mem_level_fingerprint_test.tla new file mode 100644 index 00000000..50bd72e4 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/ENABLEDrewrites_mem_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +--------------- MODULE ENABLEDrewrites_mem_level_fingerprint_test -------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v1.tla new file mode 100644 index 00000000..4080e951 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v1.tla @@ -0,0 +1,17 @@ +--------------- MODULE temp -------------- +(* Test that changing the level of the right-hand side of set membership within +`ENABLED` also changes the result of the proof directive `ENABLEDrewrites`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +A == x + + +THEOREM (ENABLED (x' \in A)) = (A # {}) +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v2.tla new file mode 100644 index 00000000..2c38940b --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v2.tla @@ -0,0 +1,14 @@ +--------------- MODULE temp -------------- +EXTENDS TLAPS + + +VARIABLE x + + +A == x' + + +THEOREM (ENABLED (x' \in A)) = (A # {}) +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/ENABLEDrewrites_state_level_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/ENABLEDrewrites_state_level_fingerprint_test.tla new file mode 100644 index 00000000..c766d4a5 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/ENABLEDrewrites_state_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +-------------- MODULE ENABLEDrewrites_state_level_fingerprint_test ------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v1.tla new file mode 100644 index 00000000..90fe37f3 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v1.tla @@ -0,0 +1,17 @@ +-------------- MODULE temp ------------- +(* Test that changing the level of the argument of `ENABLED` +also changes the result of the proof directive `ENABLEDrewrites`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +A == x + + +THEOREM (ENABLED A) = A +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v2.tla new file mode 100644 index 00000000..0f1eae19 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v2.tla @@ -0,0 +1,14 @@ +-------------- MODULE temp ------------- +EXTENDS TLAPS + + +VARIABLE x + + +A == x' + + +THEOREM (ENABLED A) = A +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/ENABLEDrewrites_ternary_level_fingerprint_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/ENABLEDrewrites_ternary_level_fingerprint_test.tla new file mode 100644 index 00000000..71b5d498 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/ENABLEDrewrites_ternary_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +------------ MODULE ENABLEDrewrites_ternary_level_fingerprint_test ------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v1.tla new file mode 100644 index 00000000..6719147a --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v1.tla @@ -0,0 +1,19 @@ +------------ MODULE temp ------------- +(* Test that changing the level of the test expression in a ternary conditional +also changes the result of the proof directive `ENABLEDrewrites`. +*) +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x +B == x' +C == y' + + +THEOREM (ENABLED (IF A THEN B ELSE C)) = IF A THEN ENABLED B ELSE ENABLED C +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v2.tla new file mode 100644 index 00000000..1dda6ffc --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v2.tla @@ -0,0 +1,16 @@ +------------ MODULE temp ------------- +EXTENDS TLAPS + + +VARIABLE x, y + + +A == x' +B == x' +C == y' + + +THEOREM (ENABLED (IF A THEN B ELSE C)) = IF A THEN ENABLED B ELSE ENABLED C +BY ENABLEDrewrites + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrewrites_test.tla b/test/fast/enabled_cdot/ENABLEDrewrites_test.tla new file mode 100644 index 00000000..501f84fe --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_test.tla @@ -0,0 +1,167 @@ +-------------------------- MODULE ENABLEDrewrites_test ------------------------- +(* Tests for the proof directive `ENABLEDrewrites`. *) +EXTENDS TLAPS + + +VARIABLES x, y, z, w + + +A == x +B == y' +C == x' + + +Rstate(i) == x +Raction(i) == x' +Sconstant == {1, 2} +Sstate == {x} + + +-------------------------------------------------------------------------------- + +THEOREM (ENABLED (\E i \in Sconstant: Rstate(i))) = + \E i \in Sconstant: ENABLED Rstate(i) +BY ENABLEDrewrites + + +THEOREM (ENABLED (\E i \in Sstate: Rstate(i))) = + \E i \in Sstate: ENABLED Rstate(i) +BY ENABLEDrewrites + + +THEOREM (ENABLED (\E i \in Sconstant: Raction(i))) = + \E i \in Sconstant: ENABLED Raction(i) +BY ENABLEDrewrites + + +THEOREM (ENABLED (\E i \in Sstate: Raction(i))) = + \E i \in Sstate: ENABLED Raction(i) +BY ENABLEDrewrites + +-------------------------------------------------------------------------------- + +THEOREM (ENABLED (B \/ C)) = (ENABLED B \/ ENABLED C) +BY ENABLEDrewrites + + +THEOREM + (ENABLED \/ A + \/ B + \/ C) = + \/ ENABLED A + \/ ENABLED B + \/ ENABLED C +BY ENABLEDrewrites + +-------------------------------------------------------------------------------- + +THEOREM (ENABLED (IF A THEN B ELSE C)) = IF A THEN ENABLED B ELSE ENABLED C +BY ENABLEDrewrites + +-------------------------------------------------------------------------------- + +p1 == 1 +p2 == x +a1 == x' +a2 == y' +b == x' /\ y' + + +THEOREM (ENABLED CASE p1 -> a1 [] p2 -> a2 [] OTHER -> b) = + CASE p1 -> ENABLED a1 [] p2 -> ENABLED a2 [] OTHER -> ENABLED b +BY ENABLEDrewrites + +-------------------------------------------------------------------------------- + +c1 == x +c2 == y +c3 == z +c4 == w + +c5 == x' +c6 == y' +c7 == z' +c8 == w' + +c9 == x' /\ y' +c10 == z' /\ w' + + +THEOREM (ENABLED (c1 /\ c2)) = (ENABLED c1 /\ ENABLED c2) +BY ENABLEDrewrites + + +THEOREM (ENABLED (c1 /\ c2 /\ c3 /\ c4)) = + (ENABLED c1 /\ ENABLED c2 /\ ENABLED c3 /\ ENABLED c4) +BY ENABLEDrewrites + + +THEOREM (ENABLED (c1 /\ c6)) = (ENABLED c1 /\ ENABLED c6) +BY ENABLEDrewrites DEF c6 + + +THEOREM (ENABLED (c5 /\ c6 /\ c7 /\ c8)) = + (ENABLED c5 /\ ENABLED c6 /\ ENABLED c7 /\ ENABLED c8) +BY ENABLEDrewrites DEF c5, c6, c7, c8 + + +THEOREM (ENABLED (c5 /\ c6 /\ c9)) = /\ ENABLED /\ y' + /\ y' + /\ ENABLED /\ x' + /\ x' +BY ENABLEDrewrites DEF c5, c6, c9 + + +THEOREM (ENABLED (c9 /\ c10)) = /\ ENABLED x' + /\ ENABLED y' + /\ ENABLED z' + /\ ENABLED w' +BY ENABLEDrewrites DEF c9, c10 + +-------------------------------------------------------------------------------- + +THEOREM (ENABLED x) = x +BY ENABLEDrewrites + +-------------------------------------------------------------------------------- + +THEOREM ENABLED (x' = 1) +BY ENABLEDrewrites + +-------------------------------------------------------------------------------- + +S == {z, w} + + +THEOREM (ENABLED (x' \in S)) = (S # {}) +BY ENABLEDrewrites + +-------------------------------------------------------------------------------- + +THEOREM (ENABLED (ENABLED (B /\ C))') = + ENABLED ((/\ ENABLED C + /\ ENABLED B)') +BY ENABLEDrewrites DEF B, C + + +THEOREM Foo == ENABLED (A /\ B) <=> (x /\ ENABLED B) +BY ENABLEDrewrites DEF A, B + + +THEOREM Bar == (x /\ ENABLED B) <=> x +BY ExpandENABLED DEF B + + +THEOREM FooBar == ENABLED (A /\ B) <=> x +BY Foo, Bar + + +C == x' +D == y' + + +THEOREM ENABLED (C /\ D) <=> (ENABLED C /\ ENABLED D) +BY ENABLEDrewrites DEF C, D + + +================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/ENABLEDrules_fingerprint_levels_test.tla b/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/ENABLEDrules_fingerprint_levels_test.tla new file mode 100644 index 00000000..e15bb352 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/ENABLEDrules_fingerprint_levels_test.tla @@ -0,0 +1,11 @@ +---- MODULE ENABLEDrules_fingerprint_levels_test ---- + +===================================================== +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 4 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v1.tla b/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v1.tla new file mode 100644 index 00000000..3bb73e23 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v1.tla @@ -0,0 +1,27 @@ +---- MODULE temp ---- +(* Test that fingerprints do not mask change of level +of a proof step. + +Run `tlapm` to create fingerprints. +Then, edit this file to change the level of an assumption +from state predicate to action. Re-run `tlapm` to ensure +that the saved fingerprint does not shadow the change of +the level of the assumption, at the proof step that +includes `ENABLEDrules`. +*) +EXTENDS TLAPS + + +VARIABLE x + + +THEOREM + ASSUME x = 1 + PROVE ENABLED (x' = 1) => ENABLED (x' = 1 \/ x' = 2) +<1>1. (x' = 1) => (x' = 1 \/ x' = 2) + OBVIOUS +<1> QED + BY ONLY <1>1, ENABLEDrules + + +===================================================== diff --git a/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v2.tla b/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v2.tla new file mode 100644 index 00000000..df789d9e --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v2.tla @@ -0,0 +1,17 @@ +---- MODULE temp ---- +EXTENDS TLAPS + + +VARIABLE x + + +THEOREM + ASSUME x' = 1 + PROVE ENABLED (x' = 1) => ENABLED (x' = 1 \/ x' = 2) +<1>1. (x' = 1) => (x' = 1 \/ x' = 2) + OBVIOUS +<1> QED + BY ONLY <1>1, ENABLEDrules + + +===================================================== diff --git a/test/fast/enabled_cdot/ENABLEDrules_test.tla b/test/fast/enabled_cdot/ENABLEDrules_test.tla new file mode 100644 index 00000000..009b62b9 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrules_test.tla @@ -0,0 +1,52 @@ +--------------------------- MODULE ENABLEDrules_test --------------------------- +(* Unit tests for the implementation of proof rules about `ENABLED`. *) +EXTENDS TLAPS + + +VARIABLE x (* This statement declares a variable. *) + + +A == x' = 1 /\ x = 1 (* An action. *) +B == x' = x /\ x = 1 (* An action equivalent to action A. *) + +C == x' = 1 (* An action. *) +D == x' = 1 \/ x' = 2 (* An action implied by action C. *) + + +-------------------------------------------------------------------------------- +(* Equivalence of actions entails equivalence of their enabledness. + +In more detail, from + A <=> B +we deduce + ENABLED A <=> ENABLED B +The premise A <=> B needs to be provable where ENABLEDrules is invoked. + +The proof step where ENABLEDrules appears should not depend (directly or +indirectly) on any assumption with level higher than constant or state level +(except through only intermediate steps that have constant or state level). +*) +THEOREM + ENABLED A <=> ENABLED B +BY ENABLEDrules DEF A, B + + +-------------------------------------------------------------------------------- +(* Implication of actions entails implication of their enabledness. + +In more detail, from + A => B +we deduce + ENABLED A => ENABLED B +The premise A => B needs to be provable where ENABLEDrules is invoked. + +The proof step where ENABLEDrules appears should not depend (directly or +indirectly) on any assumption with level higher than constant or state level +(except through only intermediate steps that have constant or state level). +*) +THEOREM + ENABLED C => ENABLED D +BY ENABLEDrules DEF C, D + + +================================================================================ diff --git a/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/ExpandENABLED_level_fingerprint_test.tla b/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/ExpandENABLED_level_fingerprint_test.tla new file mode 100644 index 00000000..27520816 --- /dev/null +++ b/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/ExpandENABLED_level_fingerprint_test.tla @@ -0,0 +1,11 @@ +-------------------- MODULE ExpandENABLED_level_fingerprint_test --------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: rm -f temp.tla +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm -f temp.tla diff --git a/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v1.tla b/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v1.tla new file mode 100644 index 00000000..57957487 --- /dev/null +++ b/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v1.tla @@ -0,0 +1,17 @@ +-------------------- MODULE temp --------------- +(* Test that fingerprints do not affect the correctness of `ExpandENABLED` +when the levels of operators change. +*) +EXTENDS TLAPS + + +VARIABLE x + + +A == x + + +THEOREM ENABLED (x' /\ A) = (\E u: u /\ A) +BY ExpandENABLED + +================================================================================ diff --git a/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v2.tla b/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v2.tla new file mode 100644 index 00000000..1cfb1a6d --- /dev/null +++ b/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v2.tla @@ -0,0 +1,14 @@ +-------------------- MODULE temp --------------- +EXTENDS TLAPS + + +VARIABLE x + + +A == x' + + +THEOREM ENABLED (x' /\ A) = (\E u: u /\ A) +BY ExpandENABLED + +================================================================================ diff --git a/test/fast/enabled_cdot/LevelComparisonCONSTANT_Module_Scope_test.tla b/test/fast/enabled_cdot/LevelComparisonCONSTANT_Module_Scope_test.tla new file mode 100644 index 00000000..7475fe30 --- /dev/null +++ b/test/fast/enabled_cdot/LevelComparisonCONSTANT_Module_Scope_test.tla @@ -0,0 +1,25 @@ +--------------- MODULE LevelComparisonCONSTANT_Module_Scope_test --------------- +(* Test that module-scope `CONSTANT` declarations and associated assumptions +are not usable via the proof directive `LevelComparison`. + +Previously, this was an error, due to the constants being renamed within the +scope of their declaration. This was equivalent to universal instantiation +of a bound constant *within* the scope of the universal quantifier that +binds it. +*) +EXTENDS Naturals, TLAPS + + +CONSTANT n + + +ASSUMPTION nType == n \in Nat + + +THEOREM + ASSUME CONSTANT k + PROVE k \in Nat +BY nType, LevelComparison + +================================================================================ +stderr: obligations failed diff --git a/test/fast/enabled_cdot/LevelComparisonCONSTANT_THEOREM_Scope_test.tla b/test/fast/enabled_cdot/LevelComparisonCONSTANT_THEOREM_Scope_test.tla new file mode 100644 index 00000000..a837eca4 --- /dev/null +++ b/test/fast/enabled_cdot/LevelComparisonCONSTANT_THEOREM_Scope_test.tla @@ -0,0 +1,20 @@ +-------------- MODULE LevelComparisonCONSTANT_THEOREM_Scope_test --------------- +(* Test that theorem-scope `CONSTANT` declarations and associated assumptions +are not usable via the proof directive `LevelComparison` when they do not +appear inside a nested sequent (in the assumptions). +*) +EXTENDS Naturals, TLAPS + + +THEOREM + ASSUME + CONSTANT k, + TRUE, + CONSTANT w, + ASSUME TRUE + PROVE w \in Nat + PROVE k \in Nat +BY LevelComparison + +================================================================================ +stderr: obligations failed diff --git a/test/fast/enabled_cdot/LevelComparisonSTATE_Scope_test.tla b/test/fast/enabled_cdot/LevelComparisonSTATE_Scope_test.tla new file mode 100644 index 00000000..42b1461f --- /dev/null +++ b/test/fast/enabled_cdot/LevelComparisonSTATE_Scope_test.tla @@ -0,0 +1,18 @@ +-------------------- MODULE LevelComparisonSTATE_Scope_test -------------------- +(* Test that `STATE` declarations and associated assumptions are unusable via +the proof directive `LevelComparison` when they do not appear inside a nested +sequent (in the assumptions). +*) +EXTENDS Naturals, TLAPS + + +THEOREM + ASSUME STATE P, P + PROVE TRUE +<1>1. ASSUME STATE Q + PROVE Q + BY LevelComparison +<1> QED + +================================================================================ +stderr: obligations failed diff --git a/test/fast/enabled_cdot/LevelComparison_test.tla b/test/fast/enabled_cdot/LevelComparison_test.tla new file mode 100644 index 00000000..428bd82b --- /dev/null +++ b/test/fast/enabled_cdot/LevelComparison_test.tla @@ -0,0 +1,112 @@ +------------------------- MODULE LevelComparison_test -------------------------- +(* Tests for the proof directive LevelComparison. *) +EXTENDS Integers, TLAPS + + +VARIABLE x + + +(* A theorem about an action-level operator A. *) +THEOREM ActionLevel == + ASSUME + ACTION A + PROVE + <>_x => A +OBVIOUS + + +(* The theorem ActionLevel with action A substituted by a state-level operator +P. The proof cites the theorem ActionLevel and uses the proof directive +LevelComparison to substitute P for A. The proof directive LevelComparison +checks that the substituted operator P has level at most that of the operator +A that it replaces. + +The proof directive LevelComparison works for theorems of this form, +where a formula appears only in the consequent (PROVE) of the sequent, and only +declarations appear in the hypotheses (ASSUME). Any non-nested sequent can be +brought in this form by using implication. +*) +THEOREM + ASSUME + STATE P + PROVE + <

>_x => P +PROOF +BY ActionLevel, LevelComparison + + +(* A temporal operator. *) +Prop(u) == ([]u) => (<>[]u) + + +(* A theorem about the operator Prop, with argument a temporal-level operator P. +*) +THEOREM TemporalLevel == + ASSUME + TEMPORAL P + PROVE + Prop(P) +BY PTL DEF Prop + + +(* The theorem TemporalLevel with operator P renamed to Q. The renaming is +checked by using the proof directive LevelComparison, which checks that Q +substitutes an operator of the same or higher level (in this case same level, +and impossible to have an operator of expression level higher than temporal). +*) +THEOREM + ASSUME + TEMPORAL Q + PROVE + Prop(Q) +BY TemporalLevel, LevelComparison + + +(* The theorem TemporalLevel with the temporal-level operator P substituted by +a state-level operator P. The substitution is checked using the proof directive +LevelComparison, which checks that P substitutes an operator of the same or +higher expression level (in this case higher level). +*) +THEOREM + ASSUME + STATE P + PROVE + Prop(P) +BY TemporalLevel, LevelComparison + + +(* The theorem TemporalLevel with the temporal-level operator P substituted by +a constant-level operator P. The substitution is checked by using the proof +directive LevelComparison, ensuring that P substitutes an operator of the same +or higher expression level (in this case higher level). +*) +THEOREM + ASSUME + CONSTANT P + PROVE + Prop(P) +BY TemporalLevel, LevelComparison + +-------------------------------------------------------------------------------- + +THEOREM + ASSUME + ASSUME CONSTANT n, n \in Nat + PROVE n \in Int, + CONSTANT n, + n \in Nat + PROVE n \in Int +BY LevelComparison + + +THEOREM + ASSUME + ASSUME STATE P, STATE Q, P = Q + PROVE P.a = Q.a + PROVE TRUE +<1>1. ASSUME STATE A, STATE B, A = B + PROVE A.a = B.a + BY LevelComparison +<1> QED + +================================================================================ diff --git a/test/fast/enabled_cdot/UnsoundCoalescingThmDecl_test.tla b/test/fast/enabled_cdot/UnsoundCoalescingThmDecl_test.tla new file mode 100644 index 00000000..c8a79043 --- /dev/null +++ b/test/fast/enabled_cdot/UnsoundCoalescingThmDecl_test.tla @@ -0,0 +1,30 @@ +--------------------- MODULE UnsoundCoalescingThmDecl_test --------------------- +(* An example of substituting an action-level expression for a state predicate +by using coalescing, leading to an unsound proof. +*) +EXTENDS TLAPS + + +THEOREM + ASSUME + VARIABLE x, + x' + PROVE + FALSE +PROOF +<1> HIDE x' +<1>1. ASSUME STATE P + PROVE (ENABLED (P /\ ~ x')) <=> (P /\ ENABLED (~ x')) + BY ENABLEDaxioms +<1> DEFINE P == ~ ~ x' +<1> HIDE DEF P +<1>2. (ENABLED (P /\ ~ x')) <=> (P /\ ENABLED (~ x')) + BY <1>1 (* This proof is unsound. *) + (* This proof fails if coalescing prepends the kind + of declaration to all operator names. + *) +<1> QED + BY <1>2, x', ExpandENABLED DEF P + +================================================================================ +stderr: obligations failed