From 7b034c8eff1a5e41395b8eb69564ef3978c5d923 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Mon, 7 Dec 2020 20:54:04 +0200 Subject: [PATCH 01/39] BUG: recompute operator level info in parametrized instantiation Otherwise the already computed weights of an operator can rely on the arity of the operator before the dependence on parameters of the definition (`Foo(x) == INSTANCE Inner`) is added to the instantiated operator signature. Parametric instantiation changes the arity of operators, so the weights list needs to be recomputed, based on the arity after instantiation has been performed. --- src/module/m_elab.ml | 11 ++++--- .../Level_of_parametric_INSTANCE_test.tla | 31 +++++++++++++++++++ 2 files changed, 38 insertions(+), 4 deletions(-) create mode 100644 test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla diff --git a/src/module/m_elab.ml b/src/module/m_elab.ml index 3223751ee..442a9c5e6 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -237,14 +237,16 @@ let lambdify_definition cx df = | _ -> assert false in let expr = match expr.core with | Lambda _ -> expr (* arity < _, ... > *) - | _ -> lambdify_expr cx expr (* arity _ *) + | _ -> (* arity _ *) + let expr = lambdify_expr cx expr in + Expr.Levels.rm_expr_level cx expr in let core = match df.core with | Operator (name, _) -> Operator (name, expr) | Bpragma (name, _, backend_args) -> Bpragma (name, expr, backend_args) | _ -> assert false in let df = core @@ df in - df + Expr.Levels.rm_level df let get_sequent expr = match expr.core with @@ -255,7 +257,7 @@ let get_sequent expr = match expr.core with let lambdify_sequent cx (sq: Expr.T.sequent) = let sq_expr = noprops (Sequent sq) in let expr = lambdify_expr cx sq_expr in - (* let expr = sq in *) + let expr = Expr.Levels.rm_expr_level cx expr in get_sequent expr @@ -377,7 +379,7 @@ let resub_for n niargs iargs inst = let lambdify e inst niargs = (* Add additional lambdas if needed. *) - match e.core with + Expr.Levels.rm_level begin match e.core with | Lambda (vs, le) -> let ivs = List.map (fun v -> (v, Shape_expr)) @@ -392,6 +394,7 @@ let lambdify e inst niargs = inst.core.inst_args in Lambda (ivs, e) @@ e end + end let rec localize body body_len iname niargs iargs not_complained inst local = diff --git a/test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla b/test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla new file mode 100644 index 000000000..dd959793f --- /dev/null +++ b/test/fast/enabled_cdot/Level_of_parametric_INSTANCE_test.tla @@ -0,0 +1,31 @@ +---- MODULE Level_of_parametric_INSTANCE_test ---- +(* Test if the level weights of operators are +updated in case they have been computed before +parametric instantiation. + +No fingerprints are used in this test to ensure +that the level computation is performed. +*) + +---- MODULE Inner ---- +VARIABLE x + +Foo == x +====================== + +(* This horizontal line tests that the test script +`test/TOOLS/do_one_test` correctly reasons about +nesting of submodules. +*) +-------------------------------------------------- + +M(x) == INSTANCE Inner + +THEOREM TRUE +<1>1. M!Foo(TRUE) => M!Foo(TRUE) + OBVIOUS +<1> QED + +================================================== +command: ${TLAPM} --nofp --toolbox 0 0 ${FILE} +nostderr: ending abnormally From 3c899a502d9cb433f6cc37f9333e34072285f7a6 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Dec 2020 19:26:40 +0200 Subject: [PATCH 02/39] BUG: lambdify ENABLED in operators with arguments --- src/module/m_elab.ml | 2 +- .../ENABLED_INSTANCE_op_with_args_test.tla | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 test/fast/enabled_cdot/ENABLED_INSTANCE_op_with_args_test.tla diff --git a/src/module/m_elab.ml b/src/module/m_elab.ml index 442a9c5e6..e23867681 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -236,7 +236,7 @@ let lambdify_definition cx df = | Bpragma (_, expr, _) -> expr | _ -> assert false in let expr = match expr.core with - | Lambda _ -> expr (* arity < _, ... > *) + | Lambda _ (* arity < _, ... > *) | _ -> (* arity _ *) let expr = lambdify_expr cx expr in Expr.Levels.rm_expr_level cx expr diff --git a/test/fast/enabled_cdot/ENABLED_INSTANCE_op_with_args_test.tla b/test/fast/enabled_cdot/ENABLED_INSTANCE_op_with_args_test.tla new file mode 100644 index 000000000..ec1016832 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLED_INSTANCE_op_with_args_test.tla @@ -0,0 +1,18 @@ +---- MODULE ENABLED_INSTANCE_op_with_args_test ---- +EXTENDS TLAPS + +---- MODULE Inner ---- +VARIABLE x, y + +A(z) == ENABLED (x' # y') + +====================== + +VARIABLE x + +M == INSTANCE Inner WITH y <- x + +THEOREM M!A(x) +BY ExpandENABLED DEF M!A + +=================================================== From ab897dc51c596100f2f35ca5380ad69b1000c3e7 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Dec 2020 19:48:17 +0200 Subject: [PATCH 03/39] TST: add tests for `ENABLED` with `INSTANCE` --- .../ENABLED_INSTANCE_nullary_op_test.tla | 18 ++++++++++++++++++ ...ABLED_INSTANCE_nullary_op_two_vars_test.tla | 18 ++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_test.tla create mode 100644 test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_two_vars_test.tla diff --git a/test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_test.tla b/test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_test.tla new file mode 100644 index 000000000..112224bc0 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_test.tla @@ -0,0 +1,18 @@ +---- MODULE ENABLED_INSTANCE_nullary_op_test ---- +EXTENDS TLAPS + +---- MODULE Inner ---- +VARIABLE x + +A == ENABLED (x') + +====================== + +VARIABLE x + +M == INSTANCE Inner + +THEOREM M!A +BY ExpandENABLED DEF M!A + +================================================= diff --git a/test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_two_vars_test.tla b/test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_two_vars_test.tla new file mode 100644 index 000000000..5f52a666e --- /dev/null +++ b/test/fast/enabled_cdot/ENABLED_INSTANCE_nullary_op_two_vars_test.tla @@ -0,0 +1,18 @@ +---- MODULE ENABLED_INSTANCE_nullary_op_two_vars_test ---- +EXTENDS TLAPS + +---- MODULE Inner ---- +VARIABLE x, y + +A == ENABLED (x' # y') + +====================== + +VARIABLE x + +M == INSTANCE Inner WITH y <- x + +THEOREM M!A +BY ExpandENABLED DEF M!A + +========================================================== From e30f941dcd6af0ad4381c7301ef54c4716f4b710 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Mon, 7 Dec 2020 22:41:54 +0200 Subject: [PATCH 04/39] TST: correctly detect end of module This change ensures that the testing commands are read after the closing horizontal rule (`=====*`) of the module. To do this, the nesting depth of submodules is tracked, by incrementing the counter `submodule_nesting_depth` when encountering a module opening (`-----*\s*MODULE`), and decrementing this counter when encountering a module closing (`=====*`). Commands are read after the module's end. Previously, commands were read after the first module closing (`=====*`), which results in errors in the presence of submodules. --- test/TOOLS/do_one_test | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/test/TOOLS/do_one_test b/test/TOOLS/do_one_test index 212a05a26..8706f963e 100755 --- a/test/TOOLS/do_one_test +++ b/test/TOOLS/do_one_test @@ -35,13 +35,22 @@ BEGIN { check_command = ""; failed = 0; stretch = ENVIRON["STRETCH"]; + submodule_nesting_depth = 0; } # remove trailing CR from input line { sub (/\r$/, ""); } +phase == 0 && /^----[-]*[ ]*MODULE/ { + submodule_nesting_depth++; + next; +} + phase == 0 && /^====/ { - phase = 1; + submodule_nesting_depth--; + if (submodule_nesting_depth == 0){ + phase = 1; + } next; } From 8a5b74a647f79b56d9ff594fc38af9e6fc4d817e Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Dec 2020 03:25:32 +0200 Subject: [PATCH 05/39] BUG: show "VARIABLE" for single variable, "VARIABLES" otherwise. --- src/module/m_fmt.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/module/m_fmt.ml b/src/module/m_fmt.ml index 4b56d9939..fe9c7abab 100644 --- a/src/module/m_fmt.ml +++ b/src/module/m_fmt.ml @@ -45,7 +45,7 @@ let rec pp_print_modunit ?(force=false) cx ff mu = match mu.core with | Variables vs -> let (ncx, vs) = adjs cx vs in fprintf ff "@[VARIABLE%s@ %a@]@," - (if vs = [] then "" else "S") + (if ((List.length vs) = 1) then "" else "S") (pp_print_delimited pp_print_string) vs ; ncx | Definition (df, wd, _, ex) -> From c561dbeb24bdaf5bb4965907481e125df647bc21 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Mon, 7 Dec 2020 18:17:01 +0200 Subject: [PATCH 06/39] ENH: add function `print_modules` that prints the names of modules in a module context. --- src/tlapm.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/tlapm.ml b/src/tlapm.ml index 1f8e4896d..a42285538 100644 --- a/src/tlapm.ml +++ b/src/tlapm.ml @@ -468,6 +468,10 @@ let read_new_modules mcx fs = (mcx, mule :: mods) end (mcx, []) fs +let print_modules mcx = + print_string "\nModules loaded so far:\n"; + Sm.iter (fun name mule -> Printf.printf "Module name: \"%s\"\n" name) mcx + let main fs = Params.input_files := List.map Filename.basename fs; let () = @@ -484,6 +488,7 @@ let main fs = Submodules are read below. *) let (mcx, mods) = read_new_modules mcx fs in + (* print_modules mcx; *) if List.length mods = 0 then begin Util.eprintf ~prefix:"FATAL: " "could not read any modules successfully!" ; failwith "fatal error: could not read any modules"; From aa1f39b6e328f5df060b22e3819577ce97afc4c9 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Mon, 7 Dec 2020 18:15:30 +0200 Subject: [PATCH 07/39] BUG: load modules in `EXTENDS` of submodules --- src/module/m_dep.ml | 1 + test/fast/language/EXTENDS_in_submodule_test.tla | 12 ++++++++++++ 2 files changed, 13 insertions(+) create mode 100644 test/fast/language/EXTENDS_in_submodule_test.tla diff --git a/src/module/m_dep.ml b/src/module/m_dep.ml index ea0becc49..155169896 100644 --- a/src/module/m_dep.ml +++ b/src/module/m_dep.ml @@ -40,6 +40,7 @@ let external_deps m = let m = subm.core in locals := Hs.add m.name !locals ; submodules := Sm.add m.name.core subm !submodules; + List.iter (fun s -> deps := Hs.add s !deps) subm.core.extendees; List.iter visit m.body | Anoninst (ins, _) -> ignore (mapper#defn ((), Deque.empty) diff --git a/test/fast/language/EXTENDS_in_submodule_test.tla b/test/fast/language/EXTENDS_in_submodule_test.tla new file mode 100644 index 000000000..21a9a64d7 --- /dev/null +++ b/test/fast/language/EXTENDS_in_submodule_test.tla @@ -0,0 +1,12 @@ +---- MODULE EXTENDS_in_submodule_test ---- +(* Ensure that modules listed in EXTENDS statements +that are contained in submodules are loaded by `tlapm`. +*) + + +---- MODULE Inner ---- +EXTENDS TLAPS + +====================== + +========================================== From 09719c816ccb7f141f94879de70d97e4cc56846f Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Dec 2020 03:22:10 +0200 Subject: [PATCH 08/39] BUG: correctly shift module units when instantiating When instantiating inside a LET, definitions are kept, and other module units omitted. A negative shift is applied to the remaining module units. This negative shift should equal minus the number of hypotheses that the omitted module unit introduces in the context. The number of hypotheses for each module unit is computed by the function `M_t.hyps_of_modunit`. --- src/module/m_elab.ml | 15 ++++++++-- ...NCE_shift_due_to_omitted_modunits_test.tla | 29 +++++++++++++++++++ 2 files changed, 41 insertions(+), 3 deletions(-) create mode 100644 test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla diff --git a/src/module/m_elab.ml b/src/module/m_elab.ml index e23867681..a9db7b9af 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -580,9 +580,18 @@ let anon = object (self : 'self) | mu :: mus -> begin match mu.core with | Definition (df, _, _, _) -> make_defs (df :: sofar) mus - | _ -> - let (_, mus) = M_subst.app_modunits (shift (-1)) mus in - make_defs sofar mus + | Constants _ + | Recursives _ + | Variables _ + | Axiom _ + | Theorem _ + | Submod _ + | Mutate _ + | Anoninst _ -> + let mu_hyps = M_t.hyps_of_modunit mu in + let n_hyps = List.length mu_hyps in + let (_, mus) = M_subst.app_modunits (shift (-n_hyps)) mus in + make_defs sofar mus end in self#defns scx (make_defs [] submus @ dfs) diff --git a/test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla b/test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla new file mode 100644 index 000000000..a83b24d47 --- /dev/null +++ b/test/fast/language/INSTANCE_shift_due_to_omitted_modunits_test.tla @@ -0,0 +1,29 @@ +---- MODULE INSTANCE_shift_due_to_omitted_modunits_test ---- + + +---- MODULE Inner ---- +EXTENDS TLAPS + +VARIABLE y + +A == y' +THEOREM B == []TRUE +====================== + + +VARIABLE z + + +M == INSTANCE Inner WITH y <- z + + +THEOREM + \EE x: + LET Q == INSTANCE Inner WITH y <- x + IN Q!A +OBVIOUS + + +============================================================ +command: ${TLAPM} --toolbox 0 0 ${FILE} +nostderr: Assertion failed From 4d2129ecce8c212557f9e618fb3e1a9a9875ffff Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Sep 2020 16:28:12 +0300 Subject: [PATCH 09/39] REF: add details to error message --- src/expr/e_elab.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/expr/e_elab.ml b/src/expr/e_elab.ml index ca8a47066..8106ee13a 100644 --- a/src/expr/e_elab.ml +++ b/src/expr/e_elab.ml @@ -155,6 +155,11 @@ let let_normalize = let e = Let (ds, e) @@ dest in let e = app_expr (scons op (shift 0)) e in self#expr scx e + | Instance (name, _) -> + Errors.bug ~at:d ( + "Found INSTANCE in Expr.Elab.let_normalize, " ^ + "all INSTANCE statements have been replaced " ^ + "with definitions in Module.Elab ") | _ -> Errors.bug ~at:d "Expr.Elab.let_normalize" end From a4ca6ac8ee101dbd21b41bbbc1887935a0d9d888 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Sep 2020 16:34:07 +0300 Subject: [PATCH 10/39] BUG: handle `INSTANCE` statements within `LET` `Module.Elab` replaces each `INSTANCE` statement with definitions. If the instantiated module extends the module `TLAPS`, then the definitions include backend pragmas (constructor `Bpragma`). --- src/expr/e_elab.ml | 3 +- .../language/INSTANCE_inside_LET_test.tla | 28 +++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) create mode 100644 test/fast/language/INSTANCE_inside_LET_test.tla diff --git a/src/expr/e_elab.ml b/src/expr/e_elab.ml index 8106ee13a..949528e47 100644 --- a/src/expr/e_elab.ml +++ b/src/expr/e_elab.ml @@ -150,7 +150,8 @@ let let_normalize = | Let ([], e) -> self#expr scx e | Let (d :: ds, e) -> begin match d.core with - | Operator (n, nexp) -> + | Operator (n, nexp) + | Bpragma (n, nexp, _) -> let op = self#expr scx nexp in let e = Let (ds, e) @@ dest in let e = app_expr (scons op (shift 0)) e in diff --git a/test/fast/language/INSTANCE_inside_LET_test.tla b/test/fast/language/INSTANCE_inside_LET_test.tla new file mode 100644 index 000000000..2f24fbf37 --- /dev/null +++ b/test/fast/language/INSTANCE_inside_LET_test.tla @@ -0,0 +1,28 @@ +---- MODULE INSTANCE_inside_LET_test ---- +(* Module.Elab` replaces each `INSTANCE` statement +with definitions. If the instantiated module +extends the module `TLAPS`, then the definitions +include backend pragmas (constructor `Bpragma`). + +If the `INSTANCE` definition appears inside a `LET`, +then normalization of `LET` and fingerprints need +to handle `Bpragma` as a case. +*) + + +---- MODULE Inner ---- +EXTENDS TLAPS + +A == TRUE +====================== + + +THEOREM + LET M == INSTANCE Inner + IN M!A + + +THEOREM TRUE +OBVIOUS (* used to raise assertion failure at `Expr.Elab.let_normalize` *) + +========================================= From a5dc90a1a0fc005f3a5313982ddce3432ce61526 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Sep 2020 17:03:11 +0300 Subject: [PATCH 11/39] REF: add details to error message --- src/backend/fingerprints.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index b53177993..258fab48e 100644 --- a/src/backend/fingerprints.ml +++ b/src/backend/fingerprints.ml @@ -516,8 +516,10 @@ and fp_let counthyp countvar stack buf ds e = Stack.push stack (Identvar hint.core, ref false); spin stack ds; ignore(Stack.pop stack) + | Instance _ -> + Errors.bug ~at:d "Backend.Fingerprints.fp_let: INSTANCE 3" | _ -> - Errors.bug ~at:d "Backend.Fingerprint.fp_let: INSTANCE 3" + Errors.bug ~at:d "Backend.Fingerprints.fp_let: other" end in spin stack ds From a87906fa845fd887473fdda4f2be4149a05f96ba Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 8 Sep 2020 17:04:21 +0300 Subject: [PATCH 12/39] BUG: fingerprint `INSTANCE` statements within `LET` `Module.Elab` replaces each `INSTANCE` statement with definitions. If the instantiated module extends the module `TLAPS`, then the definitions include backend pragmas (constructor `Bpragma`). --- src/backend/fingerprints.ml | 3 ++- .../INSTANCE_inside_LET_fingerprint_test.tla | 27 +++++++++++++++++++ 2 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 test/fast/language/INSTANCE_inside_LET_fingerprint_test.tla diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index 258fab48e..74db202b0 100644 --- a/src/backend/fingerprints.ml +++ b/src/backend/fingerprints.ml @@ -510,7 +510,8 @@ and fp_let counthyp countvar stack buf ds e = let rec spin stack = function | [] -> fp_expr counthyp countvar stack buf e | d :: ds -> begin match d.core with - | Operator (hint, e) -> + | Operator (hint, e) + | Bpragma (hint, e, _) -> fp_expr counthyp countvar stack buf e ; Buffer.add_char buf '.' ; Stack.push stack (Identvar hint.core, ref false); diff --git a/test/fast/language/INSTANCE_inside_LET_fingerprint_test.tla b/test/fast/language/INSTANCE_inside_LET_fingerprint_test.tla new file mode 100644 index 000000000..6391d2b55 --- /dev/null +++ b/test/fast/language/INSTANCE_inside_LET_fingerprint_test.tla @@ -0,0 +1,27 @@ +---- MODULE INSTANCE_inside_LET_fingerprint_test ---- +(* Module.Elab` replaces each `INSTANCE` statement +with definitions. If the instantiated module +extends the module `TLAPS`, then the definitions +include backend pragmas (constructor `Bpragma`). + +If the `INSTANCE` definition appears inside a `LET`, +then normalization of `LET` and fingerprints need +to handle `Bpragma` as a case. +*) + + +---- MODULE Inner ---- +EXTENDS TLAPS + +A == TRUE +====================== + + +THEOREM + LET M == INSTANCE Inner + IN M!A +OBVIOUS (* used to raise an assertion failure at: + `Backend.Fingerprints.fp_let: other` *) + + +===================================================== From 30f1415670527ca70b1e19764bb9ade98a3b4139 Mon Sep 17 00:00:00 2001 From: merz Date: Tue, 9 Feb 2021 10:10:29 +0100 Subject: [PATCH 13/39] liveness proof for EWD840 example --- examples/EWD840.tla | 265 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 246 insertions(+), 19 deletions(-) diff --git a/examples/EWD840.tla b/examples/EWD840.tla index 8e6fe545d..d5c346ddc 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 - (* 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,7 +207,7 @@ 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 @@ -219,10 +215,241 @@ LEMMA Inv_implies_Termination == Inv => TerminationDetection <1>. QED BY <1>1 DEF TerminationDetection, terminationDetected +----------------------------------------------------------------------------- +(***************************************************************************) +(* 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 +<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 From 017ebd8a847884bf357d8cf07ea0bd2f017f57e5 Mon Sep 17 00:00:00 2001 From: merz Date: Thu, 18 Feb 2021 08:48:40 +0100 Subject: [PATCH 14/39] fixed typo in Peterson example --- examples/Peterson.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/Peterson.tla b/examples/Peterson.tla index 476637fe2..b81ac9f5b 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 From 737dd12c5b26359f8dd77265b6a5c6a46adab339 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Thu, 12 Nov 2020 14:17:11 +0200 Subject: [PATCH 15/39] DOC: add comments to example and tests --- examples-draft/SimpleExampleWF.tla | 98 +++++++--- test/fast/enabled_cdot/Cdot_test.tla | 52 +++++ test/fast/enabled_cdot/ENABLEDaxioms_test.tla | 177 +++++++++++++----- test/fast/enabled_cdot/Enabled_test.tla | 133 +++++++++++-- .../NestedENABLED_from_AutoUSE_test.tla | 38 ++++ 5 files changed, 420 insertions(+), 78 deletions(-) diff --git a/examples-draft/SimpleExampleWF.tla b/examples-draft/SimpleExampleWF.tla index 67fa23a9d..b3fc9ee2b 100644 --- a/examples-draft/SimpleExampleWF.tla +++ b/examples-draft/SimpleExampleWF.tla @@ -3,73 +3,129 @@ EXTENDS Integers, NaturalsInduction, TLAPS -VARIABLE x +VARIABLE x (* The declaration of a variable named x. *) -Init == x = 0 -Next == x' = x + 1 +Init == x = 0 (* The initial condition asserts that x starts equal to 0. *) +Next == x' = x + 1 (* The action Next asserts that x is incremented by 1. *) -Spec == Init /\ [][Next]_x /\ WF_x(Next) +Spec == Init /\ [][Next]_x /\ WF_x(Next) (* The temporal formula Spec asserts + that variable x starts equal to 0, each step either leaves x unchanged or + increments x by 1, and whenever a step that increments x and changes x + remains possible, such a step eventually occurs. *) THEOREM \A n \in Nat: Spec => <>(x = n) PROOF (* Type invariance. *) -<1> DEFINE Inv == x \in Nat -<1>1. Spec => []Inv - <2>1. Init => Inv +<1> DEFINE Inv == x \in Nat (* The type invariant asserts that x is a natual + number. *) +<1>1. Spec => []Inv (* Spec implies the type invariant, *) + <2>1. Init => Inv (* because the initial condition implies the + type invariant, and *) BY DEF Init, Inv - <2>2. Inv /\ [Next]_x => Inv' + <2>2. Inv /\ [Next]_x => Inv' (* each step that satisfies the action + [Next]_x and starts from a state that satisfies the type invariant + leads to a state that satisfies the type invariant. + In other words, the type invariant is an inductive invariant. *) BY DEF Inv, Next <2> QED BY <2>1, <2>2, PTL DEF Spec -(* Temporal property over which induction is applied. *) +(* Temporal property P over which induction is applied. The formula P(m) +asserts that Spec implies that eventually variable x equals the value m. +In this specification, m is a natural number, and P(m) will be shown to +be valid for every natural number. *) <1> DEFINE P(m) == Spec => <>(x = m) -<1> HIDE DEF P -(* Induction over natural numbers. *) +<1> HIDE DEF P (* We hide the definition of P to reduce the complexity visible + to the back-end solvers. *) +(* Induction over the set of natural numbers. *) <1>2. \A n \in Nat: P(n) - (* Base case for induction. *) + (* Base case for induction. We show that P(0) is TRUE. *) <2>1. P(0) BY PTL DEF P, Spec, Init - (* Inductive case. *) + (* Inductive case. We show that for every natural number, P(n) implies + P(n + 1). Together with the base case P(0), these assertions are the + premises for proving that P(n) holds for every natural number n. *) <2>2. \A n \in Nat: P(n) => P(n + 1) <3>1. SUFFICES ASSUME NEW n \in Nat PROVE (Spec /\ <>(x = n)) => <>(x = n + 1) + (* In this SUFFICES step we prove that it is sufficient to + prove the implication (Spec /\ <>(x = n)) => <>(x = n + 1) + for every natural number n, in order to prove the formula + \A n \in Nat: P(n) => P(n + 1). This becomes more evident if + we expand the definition of P in the formula + \A n \in Nat: P(n) => P(n + 1), which results in the formula + \A n \in Nat: (Spec => <>(x = n)) => (Spec => <>(x = n + 1)). + *) BY <3>1 DEF P - (* If x reaches n then it remains n or increases by 1. *) + (* The temporal formula Spec implies that if x reaches n then + x forever remains n or eventually x increases by 1. We will use this + assertion, together with weak fairness of action Next to prove that + always eventually x increases by 1. *) <3>2. Spec => [] \/ ~ (x = n) - \/ <> \/ [] (x = n) - \/ (x = n + 1) + \/ [] (x = n) + \/ <> (x = n + 1) <4>1. ASSUME Inv /\ [Next]_x PROVE \/ ~ (x = n) \/ (x = n)' \/ (x = n + 1)' + (* The invariant and action [Next]_x imply that starting + from a state where x equls n, next either x equals n or + x equals n + 1. *) BY <4>1 DEF Inv, Next + (* Using reasoning by the propositional temporal logic prover + (PTL) and step <4>1, we deduce that formula Spec implies that + if x reaches n then x either remains indefinitely equal to n + or eventually increases by 1. *) <4> QED BY <1>1, <4>1, PTL DEF Spec (* Spec implies infinitely many Next steps that change x. *) <3>3. Spec => []<><>_x - (* Replacing ENABLED by quantifiers. *) + (* From any state that satisfies the type invariant (x \in Nat), + the action <>_x is enabled, which means that a step that + increments x by 1 and changes x is possible. This assertion is + proved by first converting the expression ENABLED <>_x + to the expression \E u: u = x + 1 /\ u # x by invoking the + proof directive ExpandENABLED (with the definition of operator Next + expanded in the BY DEF statement). *) <4>1. ASSUME Inv PROVE ENABLED <>_x + (* The proof directive ExpandENABLED replaces ENABLED by + rigid existential quantification (\E). *) BY <4>1, ExpandENABLED DEF Next, Inv - (* Enabledness and fairness imply liveness. *) + (* Enabledness and weak fairness imply liveness. The formula + WF_x(Next) can be expanded to + []<>(~ ENABLED <>_x) \/ []<><>_x . + By step <4>1, []Inv implies []ENABLED <>_x, which implies + ~ []<> ~ ENABLED <>_x . Therefore, the conjunction + []Inv /\ WF_x(Next) implies []<><>_x . + *) <4>2. ASSUME []Inv PROVE WF_x(Next) => []<><>_x BY <4>1, <4>2, PTL + (* The temporal formula Spec implies []Inv /\ WF_x(Next), + so by step <4>2 the formula Spec implies []<><_x . *) <4> QED - BY <1>1, <4>1, <4>2 DEF Spec - (* Any <>_x step when x = n changes x so that ~(x = n)'. *) + BY <1>1, <4>2 DEF Spec + (* Any <>_x step when x = n changes x so that ~(x = n)'. + We will use this result together with step <3>2 to show that variable x + does not remain forever equal to n, but x is eventually incremented + by 1. *) <3>4. ASSUME Inv /\ (x = n) /\ <>_x PROVE ~(x = n)' BY <3>4 DEF Inv, Next <3> QED BY <1>1, <3>2, <3>3, <3>4, PTL + (* Using the premises P(0) and \A n \in Nat: P(n) => P(n + 1), + we deduce by the theorem NatInduction that P(n) is valid for every natural + number n. *) <2> QED BY <2>1, <2>2, NatInduction -(* Unhiding the definition of operator P. *) +(* Unhiding the definition of operator P. This step proves the theorem +assertion by making visible the definition of P within the assertion of +step <1>2. *) <1> QED BY <1>2 DEF P diff --git a/test/fast/enabled_cdot/Cdot_test.tla b/test/fast/enabled_cdot/Cdot_test.tla index 24270dc2c..076fbec71 100644 --- a/test/fast/enabled_cdot/Cdot_test.tla +++ b/test/fast/enabled_cdot/Cdot_test.tla @@ -33,11 +33,35 @@ D == /\ x = FALSE /\ x' = FALSE +(* The definitions of the operators C and D are expanded because this is +necessary to apply the proof directive ExpandCdot and prove the assertion. +The definitions of operators A and R are expanded because together they contain +a primed variable in the first argument of \cdot, which is bound by \cdot. +The definition of operator B is expanded because it contains an unprimed +variable within the second argument of \cdot, so this unprimed variable is +bound by \cdot. + +The proof directive ExpandCdot converts C with A, B, and R expanded to the +expression + +\E u: /\ /\ x = FALSE + /\ u = TRUE + /\ /\ u = TRUE + /\ x' = FALSE + +which is equivalent to the definition of operator D. +*) THEOREM C <=> D PROOF BY ExpandCdot, Zenon DEF A, B, R, C, D +(* This theorem differs from the previous one in the presence of the proof +directive AutoUSE. The definitions of the operators A, B, and R are expanded +automatically by AutoUSE, because they contain primed and unrpimed variables in +the first and second arguments of the operator \cdot, respectively. These +expansions ensure sound reasoning about the operator \cdot. +*) THEOREM C <=> D PROOF BY ExpandCdot, AutoUSE, Zenon DEF C, D @@ -61,9 +85,37 @@ D2 == /\ x = TRUE /\ y = FALSE /\ x' = TRUE /\ y' = TRUE +(* The definitions of the operators C2, D2 need to be expanded to prove the +assertion by making the operator \cdot visible to the proof directive +ExpandCdot and the definition of D2 visible to the Zenon backend. +The definitions of A2 and B2 need to be expanded because these operators occur +as first and second argument to \cdot, and contain primed and unprimed +variables, respectively. Application of the proof directive ExpandCdot produces +the expression + +(\E r_0, r_1 : + /\ /\ x = TRUE /\ y = FALSE + /\ r_1 = FALSE /\ r_0 = TRUE + /\ /\ r_1 = FALSE /\ r_0 = TRUE + /\ x' = TRUE /\ y' = TRUE) + <=> (/\ x = TRUE /\ y = FALSE + /\ x' = TRUE /\ y' = TRUE) + +(Internally the symbol # is used instead of underscores in the identifiers +r_0 and r_1, to avoid coincidence with identifiers defined by the user.) +*) THEOREM C2 <=> D2 PROOF BY ExpandCdot, Zenon DEF A2, B2, C2, D2 +(* Similar to the previous theorem, with the difference that the proof +directive AutoUSE is included, which automatically expands the definitions of +the operators A2 and B2. +*) +THEOREM C2 <=> D2 +PROOF +BY ExpandCdot, AutoUSE, Zenon DEF C2, D2 + + ================================================================================ diff --git a/test/fast/enabled_cdot/ENABLEDaxioms_test.tla b/test/fast/enabled_cdot/ENABLEDaxioms_test.tla index 12d41d6c5..2af8a9910 100644 --- a/test/fast/enabled_cdot/ENABLEDaxioms_test.tla +++ b/test/fast/enabled_cdot/ENABLEDaxioms_test.tla @@ -3,26 +3,36 @@ EXTENDS TLAPS +(* This statement declares three variables. *) VARIABLE x, y, z -P == x = 1 -A == x' = 1 /\ y' = 1 -B == z' = 1 -R == y' = 1 /\ x' = 1 +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 + 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. *) -------------------------------------------------------------------------------- -(* Proving - - - P, +(* Proving that a state predicate can be moved outside the scope of ENABLED, +i.e., that from P \in BOOLEAN, - A \in BOOLEAN -|- - (P /\ ENABLED A) <=> ENABLED (P /\ A) + 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. + +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 P /\ ENABLED A @@ -32,11 +42,33 @@ PROOF <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 +(* 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) @@ -47,6 +79,11 @@ PROOF 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 @@ -54,13 +91,19 @@ PROOF BY <1>1, <1>2, <1>3, ENABLEDaxioms -------------------------------------------------------------------------------- -(* Proving - - +(* 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) <=> (ENABLED A /\ ENABLED B) + B \in BOOLEAN, + ENABLED (A /\ B), + A and B have disjoint sets of primed variables +we deduce + (ENABLED A) /\ ENABLED B + +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. *) @@ -72,11 +115,31 @@ PROOF <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 @@ -85,12 +148,23 @@ PROOF <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 -------------------------------------------------------------------------------- +(* 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) @@ -110,16 +184,17 @@ PROOF BY <1>1, <1>2, <1>3, ENABLEDaxioms -------------------------------------------------------------------------------- -(* Proving - - +(* Proving that ENABLED can be factored out of disjunction, i.e., that from A \in BOOLEAN, - B \in BOOLEAN -|- - ENABLED (A \/ B) <=> (ENABLED A \/ ENABLED B) -*) - + B \in BOOLEAN, + (ENABLED A) \/ ENABLED B +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. +*) THEOREM ENABLED (A \/ B) PROOF @@ -138,6 +213,18 @@ PROOF BY <1>1, <1>2, <1>3, ENABLEDaxioms +(* 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 + +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 @@ -151,14 +238,17 @@ PROOF BY <1>1, <1>2, <1>3, ENABLEDaxioms -------------------------------------------------------------------------------- -(* Proving - - +(* 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. *) @@ -175,15 +265,15 @@ PROOF BY <1>1, <1>2, <1>3, ENABLEDaxioms -------------------------------------------------------------------------------- -(* Proving - - +(* Proving that the equivalence of actions implies the equivalence of +enabledness of these actions, i.e., that from A <=> R -|- +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. +*) THEOREM (ENABLED A) <=> ENABLED R PROOF @@ -193,17 +283,18 @@ PROOF BY <1>1, ENABLEDaxioms -------------------------------------------------------------------------------- -(* Proving - - +(* 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 -*) - +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 diff --git a/test/fast/enabled_cdot/Enabled_test.tla b/test/fast/enabled_cdot/Enabled_test.tla index 9e82366ab..2a776e623 100644 --- a/test/fast/enabled_cdot/Enabled_test.tla +++ b/test/fast/enabled_cdot/Enabled_test.tla @@ -3,55 +3,101 @@ EXTENDS TLAPS +(* This statement declares three variables. *) VARIABLE x, y, z -P(u) == u' -Q == y -R == x' +P(u) == u' (* An operator that primes its argument. *) +Q == y (* An operator that equals an unprimed variable. *) +R == x' (* An operator that equals a primed variable. *) + +(* The proof directive ExpandENABLED translates ENABLED x to x . +The formula x = TRUE implies x, hence x = TRUE implies ENABLED x . +*) THEOREM (x = TRUE) => ENABLED x PROOF BY ExpandENABLED +(* The proof directive ExpandENABLED translates ENABLED (x') to \E u: u . +The formula \E u: u is equivalent to TRUE. +*) THEOREM ENABLED (x') PROOF BY ExpandENABLED +(* Reasoning about the expression ENABLED R requires expanding all defined +operators that contain primed variables. The operator R contains the expression +x', which is a primed variable. So we expand R in the BY statement. +The expansion of R happens first, producing the expression ENABLED (x') . +The proof directive ExpandENABLED then translates the expression ENABLED (x') +to \E u: u . +*) THEOREM ENABLED R PROOF BY ExpandENABLED DEF R +(* Instead of listing R in the statement BY ExpandENABLED DEF R, we can write +the proof directive AutoUSE. This tells TLAPS to expand all defined operators +that need to be expanded in order to reason soundly about ENABLED. +In this case the definition of R contains the expression x', which requires +expansion for ensuring soundness, so R is automatically expanded. +*) THEOREM ENABLED R PROOF BY ExpandENABLED, AutoUSE +(* The expression P(x) expands to x'. This is a primed variable, so P(x) needs +to be expanded before converting the operator ENABLED to existential +quantification. The expansion of P is listed here in the statement +BY ExpandENABLED DEF P and produces the expression ENABLED (x'), +which ExpandENABLED converts to \E u: u . +*) THEOREM ENABLED P(x) PROOF BY ExpandENABLED DEF P +(* The need to expand the definition of operator P is detected automatically +when using the proof directive AutoUSE. An explicit expansion of P is +unnecessary. The expression ENABLED P(x) is first converted to ENABLED (x'), +and then converted to \E u: u by the proof directive ExpandENABLED. +*) THEOREM ENABLED P(x) PROOF BY ExpandENABLED, AutoUSE +(* The definition of operator Q contains an unprimed variable, which does not +need to be expanded to soundly reason about ENABLED. So we list only operator +P in the BY DEF statement (because P(x) contains the primed variable x'). + +The expansion of P happens first, producing the expression ENABLED (x' \/ Q). +This expression is then converted to the expression \E u: (u \/ Q) by the +proof directive ExpandENABLED. +*) THEOREM ENABLED (P(x) \/ Q) PROOF BY ExpandENABLED DEF P +(* Similarly to the previous example, the definition of operator P needs to be +expanded, unlike the definition of Q, because P(x) contains the primed variable +x' and Q does not contain primed variables. The necessary expansion (of P) +is performed by the proof directive AutoUSE, to yield the expression +ENABLED (x' \/ Q). ExpandENABLED converts this expression to \E u: (u \/ Q). +*) THEOREM ENABLED (P(x) \/ Q) PROOF @@ -62,9 +108,12 @@ PROOF Yunprimed == y F == ENABLED (z' /\ Yunprimed) G == /\ Yunprimed - /\ \E zprime, yprime: zprime /\ yprime + /\ \E zprime: zprime +(* A proof that expands also Yunprimed, even though this expansion is +unnecessary for ensuring soundness. +*) THEOREM EnabledEliminationWithUnexpanded == F = G PROOF @@ -72,14 +121,23 @@ PROOF (* This proof is sound with the operator Yunprimed expanded or not. *) +(* The definition of operator F needs to be explicitly expanded, so that the +occurrence of the operator ENABLED become visible to the proof directive +ExpandENABLED. The definition of the operator G needs to be expanded to prove +the equivalence. +*) THEOREM F = G PROOF - BY ExpandENABLED, AutoUSE DEF F, G + BY ExpandENABLED DEF F, G -------------------------------------------------------------------------------- +(* The operator Yunprimed needs to be expanded in this example to prove the +equivalence. AutoUSE would not do so, because Yunprimed does not contain any +primed variables. +*) THEOREM ASSUME NEW A, @@ -91,32 +149,59 @@ PROOF -------------------------------------------------------------------------------- -A == (x \in BOOLEAN) /\ (x' = ~ x) -B == ENABLED (x \in BOOLEAN /\ << A >>_x) +A == (x \in BOOLEAN) /\ (x' = ~ x) (* An action. *) +B == ENABLED (x \in BOOLEAN /\ << A >>_x) (* An ENABLED expression defined + using the action A. *) BwithAexpanded == ENABLED /\ x \in BOOLEAN /\ x' = ~ x - /\ x' # x - + /\ x' # x (* An action that is equivalent to B with the definition + of action A expanded. *) +(* The definitions of both A and B need to be expanded to prove this +implication. +*) THEOREM A => B PROOF BY ExpandENABLED DEF A, B +(* Listing A and B in the BY DEF statement is still needed in thise case +even if AutoUSE is present, because the occurrence of A as the first argument +to the implication => is not in the scope of an ENABLED, so it would not be +expanded by AutoUSE, and the occurrence of B also is not in the scope of an +ENABLED. The definition of B contains an ENABLED, but this is not a reason for +AutoUSE to expand B. + +The proof directive AutoUSE would expand the occurrence of action A within +the definition of B, because it is an action in the scope of ENABLED. +However, this expansion of A is performed due to listing A in the BY DEF +statement, before the proof directive AutoUSE is applied. +*) THEOREM A => B PROOF BY ExpandENABLED, AutoUSE DEF A, B +(* Here the operators B and BwithAexpanded need to be explicitly expanded +to prove the equivalence, and the operator A needs to be expanded to ensure +soundness, because A is an action that occurs within the scope of ENABLED in +the definition of B. +*) THEOREM B <=> BwithAexpanded PROOF BY ExpandENABLED DEF A, B, BwithAexpanded +(* By including the proof directive AutoUSE, the operator A need not be +explicitly expanded. The expansion of A within the definition of B is performed +automatically by the proof directive AutoUSE, and then ExpandENABLED converts +the assertion to (\E u: x \in BOOLEAN /\ x \in BOOLEAN /\ u = ~ x /\ u # x) +<=> (\E u: x \in BOOLEAN /\ u = ~ x /\ u # x) . +*) THEOREM B <=> BwithAexpanded PROOF @@ -124,6 +209,9 @@ PROOF -------------------------------------------------------------------------------- +(* This theorem is proved by applying the proof directive ExpandENABLED, +which converts the assertion to (\E u: y /\ u) = (\E u: u /\ y). +*) THEOREM (ENABLED (y /\ x')) = ENABLED (x' /\ y) PROOF @@ -131,25 +219,42 @@ PROOF -------------------------------------------------------------------------------- -C == x' = x -D == ENABLED C +C == x' = x (* An operator that expresses that x remains unchanged. *) +D == ENABLED C (* A state predicate that describes the states from where x + can remain unchanged. *) +(* The operator D is expanded by listing D in the BY DEF statement, because the +definition of D contains an occurence of ENABLED. The expansion of D makes the +ENABLED visible to the proof directive AutoUSE, which expands the operator C, +because C is an action that occurs in the scope of ENABLED within the +definition of operator D. After these expansions take place, the proof +directive ExpandENABLED converts the expression ENABLED (x' = x) to the +expression \E u: (u' = x), which is equivalent to TRUE. +*) THEOREM - C => D + D PROOF - BY ExpandENABLED DEF C, D + BY ExpandENABLED, AutoUSE DEF D -------------------------------------------------------------------------------- - +(* The first ENABLED expression is parsed as (ENABLED y) /\ x', which is +equivalent to y /\ x', which implies ENABLED (y /\ x'), becuase the latter is +equivalent to \E u: y /\ u . +*) THEOREM (ENABLED y /\ x') => ENABLED (y /\ x') PROOF BY ExpandENABLED +(* These two ENABLED expressions are equivalent, as proved by applying the +proof directive ExpandENABLED. For this reason, it is useful to include +parentheses around the argument of ENABLED if it is an expression that contains +operators. +*) THEOREM ((ENABLED y) /\ x') <=> ENABLED y /\ x' PROOF diff --git a/test/fast/enabled_cdot/NestedENABLED_from_AutoUSE_test.tla b/test/fast/enabled_cdot/NestedENABLED_from_AutoUSE_test.tla index 5207884ed..dbf84cd66 100644 --- a/test/fast/enabled_cdot/NestedENABLED_from_AutoUSE_test.tla +++ b/test/fast/enabled_cdot/NestedENABLED_from_AutoUSE_test.tla @@ -18,6 +18,44 @@ I == ENABLED (x /\ H') J == ENABLED (x /\ I') +(* In this example the definitions of operators A, B, C, D, E, F, G, H, I, J +are expanded automatically because they contain primed variables in the scope +of ENABLED. For example, the operator A that occurs primed in B contains the +variable x, which is primed within the scope of ENABLED, so A is expanded +within B. In more detail, the expansions are performed because A is a state +level expression (ENABLED has this expression level) that occurs primed in +the scope of ENABLED, so it could (and does) contain variables in the scope of +a prime within the scope of ENABLED. + +After AutoUSE and ExpandENABLED are applied the resulting expression is + +\E r_0 : + \E r_0_1 : + r_0 + /\ (\E r_0_2 : + r_0_1 + /\ (\E r_0_3 : + r_0_2 + /\ (\E r_0_4 : + r_0_3 + /\ (\E r_0_5 : + r_0_4 + /\ (\E r_0_6 : + r_0_5 + /\ (\E r_0_7 : + r_0_6 + /\ (\E r_0_8 : + r_0_7 + /\ (\E r_0_9 : + r_0_8 + /\ ( + \E r_0_10 : + r_0_9 + /\ r_0_10))))))))) + +(Internally the bound constants are named with the symbol # in the identifier, +for example r#0_1, to avoid coincidence with identifiers defined by the user.) +*) THEOREM ENABLED (J') PROOF From f47164bbe68e20f3dfe891e93cd37eaf8b9d0402 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Wed, 31 Mar 2021 14:41:03 +0200 Subject: [PATCH 16/39] TST: add TLA+ module `LevelComparisonTest` --- .../enabled_cdot/LevelComparison_test.tla | 90 +++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 test/fast/enabled_cdot/LevelComparison_test.tla diff --git a/test/fast/enabled_cdot/LevelComparison_test.tla b/test/fast/enabled_cdot/LevelComparison_test.tla new file mode 100644 index 000000000..86c00542b --- /dev/null +++ b/test/fast/enabled_cdot/LevelComparison_test.tla @@ -0,0 +1,90 @@ +------------------------- MODULE LevelComparison_test -------------------------- +(* Tests for the proof directive LevelComparison. *) +EXTENDS 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 + +================================================================================ From c7ff69d915e5ec2e7792c0a238844efc83db5d03 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Thu, 18 Mar 2021 17:54:28 +0100 Subject: [PATCH 17/39] TST: add TLA+ module `UnsoundCoalescingThmDecl_test` --- .../UnsoundCoalescingThmDecl_test.tla | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 test/fast/enabled_cdot/UnsoundCoalescingThmDecl_test.tla diff --git a/test/fast/enabled_cdot/UnsoundCoalescingThmDecl_test.tla b/test/fast/enabled_cdot/UnsoundCoalescingThmDecl_test.tla new file mode 100644 index 000000000..c8a79043e --- /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 From 6b49822de86651c27cbb3d394a869d0e718d87c5 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Mon, 7 Dec 2020 16:24:21 +0200 Subject: [PATCH 18/39] BUG: fingerprint `AutoUSE` results This change makes fingerprints take into account the result of the proof directive AutoUSE. Previously, fingerprinting was done before any expansion of definitions, normalization, and automated expansion of definitions, expansion of ENABLED and of \cdot. This approach worked correctly for BY DEF definitions, because those definitions were included in the fingerprint as context. With this change, only for proof obligations that include the proof directive AutoUSE, the fingerprint is computed after expansion of definitions, normalization, automated expansion of definitions, expansion of ENABLED, and of \cdot. This change ensures that the proof obligation is fingerprinted with all automatic expansions of definitions applied. A test is added that catches this error. --- src/backend/prep.ml | 41 +++++++++++++------ .../AutoUSE_fingerprint_test.tla | 10 +++++ .../enabled_cdot/AutoUSE_fingerprint/v1.tla | 24 +++++++++++ .../enabled_cdot/AutoUSE_fingerprint/v2.tla | 14 +++++++ 4 files changed, 77 insertions(+), 12 deletions(-) create mode 100644 test/fast/enabled_cdot/AutoUSE_fingerprint/AutoUSE_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/AutoUSE_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/AutoUSE_fingerprint/v2.tla diff --git a/src/backend/prep.ml b/src/backend/prep.ml index 9c15036bf..c5bb46f06 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -1377,18 +1377,35 @@ let ship ob fpout thyout record = The fingerprints include both the assertion and `BY` statement proof directives. *) - let const_fp_ob = - lazy (Fingerprints.write_fingerprint (add_constness ob)) - in - let p = lazy (normalize_expand (Lazy.force const_fp_ob) - fpout thyout record - ~expand_enabled - ~expand_cdot - ~autouse - ~apply_lambdify - ~enabled_axioms - ~level_comparison) - in + let (const_fp_ob, p) = if autouse then begin + let p = + lazy (normalize_expand (add_constness ob) + fpout thyout record + ~expand_enabled + ~expand_cdot + ~autouse + ~apply_lambdify + ~enabled_axioms + ~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) + end else begin + let const_fp_ob = + lazy (Fingerprints.write_fingerprint (add_constness ob)) + in + let p = lazy (normalize_expand (Lazy.force const_fp_ob) + fpout thyout record + ~expand_enabled + ~expand_cdot + ~autouse + ~apply_lambdify + ~enabled_axioms + ~level_comparison) + in + (const_fp_ob, p) + end in let prep_meth m = let ob = Lazy.force const_fp_ob in let m = Method.scale_time m !Params.timeout_stretch in 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 000000000..f6ad7b207 --- /dev/null +++ b/test/fast/enabled_cdot/AutoUSE_fingerprint/AutoUSE_fingerprint_test.tla @@ -0,0 +1,10 @@ +---- MODULE AutoUSE_fingerprint_test ---- + +========================================= +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 3 obligations proved +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..7a784f44e --- /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 000000000..71b41edbd --- /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 + +==================================== From 426a200d190e6e80a09f5e74c0c1cf8e7429b7a3 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sat, 5 Dec 2020 13:48:17 +0200 Subject: [PATCH 19/39] BUG: correct soundness check for proof levels --- src/module/m_elab.ml | 234 ++++++++++++++++++++++++------------------- 1 file changed, 132 insertions(+), 102 deletions(-) diff --git a/src/module/m_elab.ml b/src/module/m_elab.ml index a9db7b9af..a2492a7b0 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -660,6 +660,16 @@ 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 + + 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 @@ -669,8 +679,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 @@ -696,15 +709,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 @@ -724,8 +728,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 @@ -744,9 +762,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 @@ -766,8 +787,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 @@ -781,133 +803,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 `ENABLEDaxioms` in the context *) let found = ref false in let find_proof_directive n hyp = match hyp.core with @@ -918,7 +942,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 = "ENABLEDaxioms") then + found := true | _ -> () end | _ -> () @@ -927,21 +952,18 @@ 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 ENABLEDaxioms\n"; + + if (!found && (!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 @@ -1117,6 +1139,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 *) @@ -1147,8 +1175,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 From aec7bbeb167f0b40f45c3b52cbf36dbf10aebbb0 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sat, 5 Dec 2020 15:59:06 +0200 Subject: [PATCH 20/39] DOC: add PlusCal-like algorithm for soundness check --- src/module/m_elab.ml | 152 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 152 insertions(+) diff --git a/src/module/m_elab.ml b/src/module/m_elab.ml index a2492a7b0..919eda013 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -670,6 +670,158 @@ let rec hyps_level hs = 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 + `ENABLEDaxioms` depends on a fact of too high level, + and fail with a suitable message. + *) + if (HasENABLEDaxioms(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 From 987e425c2793609c034844ec33bdf65e7addab3e Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sat, 5 Dec 2020 13:48:50 +0200 Subject: [PATCH 21/39] ENH: add proof directives `ENABLEDrules` and `ENABLEDrewrites` summary of changes - test fingerprints by running `tlapm` twice - add new proof directive `ENABLEDrules` - rewrite `ENABLEDaxioms` to remove the Boolean typeness assumptions - rewrite two proof rules that previously were in `ENABLEDaxioms` and now are in `ENABLEDrules`, to remove the Boolean typeness assumptions - correct soundness check for `ENABLEDrules` (previously for `ENABLEDaxioms`) - fingerprint the level correctness of proof obligations - revise renaming of variables in `ExpandENABLED` - removal of older implementation of `ENABLEDaxioms` - `ENABLEDaxioms` was not correctly collecting primed variables - use expression level in fingerprint of definition - record name of `Bpragma` in fingerprint - implement rewriting system for `ENABLEDrewrites` - add new proof directive `ENABLEDrewrites` - add test modules --- library/TLAPS.tla | 10 + src/backend/fingerprints.ml | 29 +- src/backend/prep.ml | 87 +- src/expr.mli | 8 +- src/expr/e_action.ml | 898 +++++++++++++----- src/expr/e_action.mli | 6 +- src/expr/e_visit.ml | 134 +-- src/expr/e_visit.mli | 3 +- src/method.ml | 10 + src/method.mli | 2 + src/method_prs.ml | 6 + src/module/m_elab.ml | 23 +- ...ENABLEDaxioms_conj_fingerprinting_test.tla | 10 + .../ENABLEDaxioms_conj_fingerprinting/v1.tla | 16 + .../ENABLEDaxioms_conj_fingerprinting/v2.tla | 15 + ...ENABLEDaxioms_conj_hidden_actions_test.tla | 20 + .../enabled_cdot/ENABLEDaxioms_conj_test.tla | 42 + ...Daxioms_conj_visible_actions_fail_test.tla | 20 + ...NABLEDaxioms_conj_visible_actions_test.tla | 18 + test/fast/enabled_cdot/ENABLEDaxioms_test.tla | 319 +------ ...ites_assignment_level_fingerprint_test.tla | 10 + .../v1.tla | 17 + .../v2.tla | 14 + ...ABLEDrewrites_bpragma_fingerprint_test.tla | 10 + .../v1.tla | 22 + .../v2.tla | 11 + ...EDrewrites_case_level_fingerprint_test.tla | 10 + .../v1.tla | 18 + .../v2.tla | 15 + ...EDrewrites_conj_level_fingerprint_test.tla | 10 + .../v1.tla | 18 + .../v2.tla | 15 + ...Drewrites_exist_level_fingerprint_test.tla | 10 + .../v1.tla | 19 + .../v2.tla | 16 + ...LEDrewrites_mem_level_fingerprint_test.tla | 10 + .../v1.tla | 17 + .../v2.tla | 14 + ...Drewrites_state_level_fingerprint_test.tla | 10 + .../v1.tla | 17 + .../v2.tla | 14 + ...ewrites_ternary_level_fingerprint_test.tla | 10 + .../v1.tla | 19 + .../v2.tla | 16 + .../enabled_cdot/ENABLEDrewrites_test.tla | 167 ++++ .../ENABLEDrules_fingerprint_levels_test.tla | 10 + .../ENABLEDrules_fingerprint_levels/v1.tla | 27 + .../ENABLEDrules_fingerprint_levels/v2.tla | 17 + test/fast/enabled_cdot/ENABLEDrules_test.tla | 52 + .../ExpandENABLED_level_fingerprint_test.tla | 10 + .../ExpandENABLED_level_fingerprint/v1.tla | 17 + .../ExpandENABLED_level_fingerprint/v2.tla | 14 + 52 files changed, 1714 insertions(+), 618 deletions(-) create mode 100644 test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/ENABLEDaxioms_conj_fingerprinting_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDaxioms_conj_hidden_actions_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDaxioms_conj_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_fail_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDaxioms_conj_visible_actions_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/ENABLEDrewrites_assignment_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/ENABLEDrewrites_bpragma_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/ENABLEDrewrites_case_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/ENABLEDrewrites_conj_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/ENABLEDrewrites_exist_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/ENABLEDrewrites_mem_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/ENABLEDrewrites_state_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/ENABLEDrewrites_ternary_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrewrites_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/ENABLEDrules_fingerprint_levels_test.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v1.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/v2.tla create mode 100644 test/fast/enabled_cdot/ENABLEDrules_test.tla create mode 100644 test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/ExpandENABLED_level_fingerprint_test.tla create mode 100644 test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v1.tla create mode 100644 test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/v2.tla diff --git a/library/TLAPS.tla b/library/TLAPS.tla index b52ec259b..e83bb97d0 100644 --- a/library/TLAPS.tla +++ b/library/TLAPS.tla @@ -329,12 +329,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/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index c8de41981..4990a3df5 100644 --- a/src/backend/fingerprints.ml +++ b/src/backend/fingerprints.ml @@ -16,7 +16,7 @@ type ident = | Identhypi of int | Identvar of string | Identhyp of string * string - | IdentBPragma + | IdentBPragma of string ;; (************************) @@ -86,7 +86,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 +250,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 +276,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 +444,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 +481,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 +575,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/prep.ml b/src/backend/prep.ml index c5bb46f06..ebc37ab5b 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -579,6 +579,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" ;; @@ -763,6 +765,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 @@ -889,7 +897,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`. @@ -907,6 +918,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 @@ -915,6 +927,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 @@ -922,13 +935,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 @@ -946,12 +968,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_cdot autouse - apply_lambdify enabled_axioms level_comparison in + 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, @@ -961,7 +996,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 @@ -989,6 +1025,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 @@ -1179,6 +1219,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" -> @@ -1269,6 +1313,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 @@ -1321,6 +1367,14 @@ let add_constness ob = | _ -> 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 | Triv -> true (* FIXME assert false -- trivial results are not in FP *) @@ -1355,6 +1409,10 @@ let ship ob fpout thyout record = (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 @@ -1364,6 +1422,8 @@ let ship ob fpout thyout record = (x <> Method.AutoUSE) && (x <> Method.Lambdify) && (x <> Method.ENABLEDaxioms) && + (x <> Method.ENABLEDrewrites) && + (x <> Method.ENABLEDrules) && (x <> Method.LevelComparison) )) meths in @@ -1379,13 +1439,15 @@ let ship ob fpout thyout record = *) let (const_fp_ob, p) = if autouse then begin let p = - lazy (normalize_expand (add_constness ob) + 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 @@ -1393,7 +1455,7 @@ let ship ob fpout thyout record = (lazy fp_ob, p) 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 @@ -1402,6 +1464,8 @@ let ship ob fpout thyout record = ~autouse ~apply_lambdify ~enabled_axioms + ~enabled_rewrites + ~enabled_rules ~level_comparison) in (const_fp_ob, p) @@ -1414,6 +1478,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 @@ -1430,6 +1495,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; @@ -1464,14 +1530,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/expr.mli b/src/expr.mli index 39f9a25fa..2cd4cc9a6 100644 --- a/src/expr.mli +++ b/src/expr.mli @@ -308,6 +308,8 @@ module Visit : sig method rename : ctx -> hyp -> Util.hint -> hyp * Util.hint method renames : ctx -> hyp list -> Util.hint list -> hyp list * Util.hint list end + + val collect_identifiers: ctx -> expr -> string list end;; module Eq : sig @@ -420,12 +422,15 @@ module Action : sig open T val invert_renaming: ctx -> 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 -> @@ -437,6 +442,7 @@ module Action : sig expand_enabled:bool -> expand_cdot:bool -> autouse:bool -> + used_identifiers: string list -> expr end;; diff --git a/src/expr/e_action.ml b/src/expr/e_action.ml index 10814c50f..6a9746779 100644 --- a/src/expr/e_action.ml +++ b/src/expr/e_action.ml @@ -31,6 +31,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 @@ -478,7 +479,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 @@ -772,21 +773,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 = @@ -803,10 +815,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) @@ -819,7 +831,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, @@ -847,6 +859,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 @@ -941,10 +954,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 @@ -952,7 +966,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_ @@ -1410,237 +1424,668 @@ class expansion_of_action_operators = end -let implication_to_enabled cx expr = - let expr = E_levels.compute_level cx expr in - let found = ref false in - let found_a_type = ref false in - let found_b_type = ref false in - let check_context hyps a b rule = - let a = Option.get a in - let b = Option.get b in - let visitor = object (self: 'self) - inherit [unit] E_visit.iter_visible_hyp +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 hyp (((), cx2) as scx) h = - let shift_n = (Deque.size hyps) - (Deque.size cx2) in - let shift = E_subst.shift shift_n in - begin match h.core with - | Fact (expr, Visible, _) -> - begin match expr.core with - | Apply ({core=Internal ENABLED}, [{core= - Apply ({core=Internal Conj}, [p; q]) - }]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "pconj") - -> - found := true - | Apply ({core=Internal ENABLED}, [{core= - Apply ({core=Internal Disj}, [p; q]) - }]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "abdisj") - -> - found := true - | Apply ({core=Internal Disj}, [ - {core=Apply ({core=Internal ENABLED}, [p])}; - {core=Apply ({core=Internal ENABLED}, [q])} - ]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "abdisj_inverse") - -> - found := true - | Apply ({core=Internal ENABLED}, [{core= - Apply ({core=Internal Conj}, [p; q]) - }]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "abconj") - -> - found := true - | Apply ({core=Internal Conj}, [ - {core=Apply ({core=Internal ENABLED}, [p])}; - {core=Apply ({core=Internal ENABLED}, [q])} - ]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - ((rule = "abconj_inverse") || - (rule = "pconj_inverse")) - -> - found := true - | Apply ({core=Internal Conj}, [p; {core= - Apply ({core=Internal ENABLED}, [q])}]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "pconj_inverse") -> - found := true - | Apply ({core=Internal Equiv}, [p; q]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "equiv") -> - found := true; - found_a_type := true; - found_b_type := true - | Apply ({core=Internal Eq}, [p; q]) when - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "equiv") -> - found := true - | Apply ({core=Internal Mem}, - [p; {core=Internal BOOLEAN}]) when - let p_ = E_subst.app_expr shift p in - (E_eq.expr p_ a) -> - found_a_type := true - | Apply ({core=Internal Mem}, - [q; {core=Internal BOOLEAN}]) when - let q_ = E_subst.app_expr shift q in - (E_eq.expr q_ b) -> - found_b_type := true - | Apply ({core=Internal Implies}, [p; q]) when - (* - print_string "\n"; - print_string (E_fmt.string_of_expr cx2 expr); - print_string (E_fmt.string_of_expr cx2 p); - print_string (E_fmt.string_of_expr cx2 q); - *) - let p_ = E_subst.app_expr shift p in - let q_ = E_subst.app_expr shift q in - (E_eq.expr p_ a) && (E_eq.expr q_ b) && - (rule = "implies") -> - found := true - | _ -> () end - | _ -> () - end; - E_visit.adj scx h - end in - let (_, cx3) = visitor#hyps ((), cx) hyps in - ignore cx3 - (* - print_string (E_fmt.string_of_expr cx3 a); - print_string (E_fmt.string_of_expr cx3 b); - *) - in - let check_active cx_goal expr = - match expr.core with - | 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); - (Some a, Some b, "abdisj_inverse") - | Apply ({core=Internal Disj}, [ - {core=Apply ({core=Internal ENABLED}, [a])}; - {core=Apply ({core=Internal ENABLED}, [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); - (Some a, Some b, "abdisj") - | Apply ({core=Internal ENABLED}, [{core= - Apply ({core=Internal Conj}, [a; b]) - }]) -> - let a_variables = E_visit.collect_primed_vars cx_goal a in - let b_variables = E_visit.collect_primed_vars cx_goal b in - let cap = List.filter - (fun x -> List.mem x a_variables) b_variables in - let isempty = (List.length cap) = 0 in - 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 + 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 - if (a_level = 2) then - (Some a, Some b, "abconj_inverse") - else - (Some a, Some b, "pconj_inverse") + 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 - else + | 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 - (None, None, " ") - end - | Apply ({core=Internal Conj}, [ - {core=Apply ({core=Internal ENABLED}, [a])}; - {core=Apply ({core=Internal ENABLED}, [b])} - ]) -> - let a_variables = E_visit.collect_primed_vars cx_goal a in - let b_variables = E_visit.collect_primed_vars cx_goal b in - let cap = List.filter + 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 - if isempty then - begin - (Some a, Some b, "abconj") - end - else - begin - (None, None, " ") + 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 - | Apply ({core=Internal Conj}, [p; {core= - Apply ({core=Internal ENABLED}, [a])}]) -> - let p_level = E_levels.get_level p in - let a_level = E_levels.get_level a in - if (p_level <= 1) && (a_level <= 2) then - (Some p, Some a, "pconj") + + (* ------------------------------------------------ + 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 - (None, None, " ") + (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])} - ]) -> (Some a, Some b, "equiv") + ]) + -> + (* 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])} - ]) -> (Some a, Some b, "implies") - | Apply ({core=Internal Eq}, [ - {core=Apply ({core=Internal ENABLED}, [a])}; - {core=Apply ({core=Internal ENABLED}, [b])} - ]) -> (Some a, Some b, "equiv") - | _ -> (None, None, " ") + ]) + -> + (* TODO: check ENABLEDaxioms property *) + Apply (noprops (Internal Implies), [a; b]) + + | _ -> expr.core in - match expr.core with - | Sequent sq -> begin - let hyps = sq.context in - let active = sq.active 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 - let (_, cx_goal) = visitor#hyps ((), cx) hyps in - let (a, b, rule) = check_active cx_goal active in - if a <> None then begin - check_context hyps a b rule - end; - let proved = !found && !found_a_type && !found_b_type in - 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 core = (if proved then Internal TRUE else expr.core) in - let active = noprops core in - let sq = {sq with active=active} in - noprops (Sequent sq) - end - | _ -> assert false + 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 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 @@ -1651,7 +2096,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 @@ -1674,7 +2119,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 *) @@ -1700,7 +2146,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 d3777420a..8132ab245 100644 --- a/src/expr/e_action.mli +++ b/src/expr/e_action.mli @@ -22,12 +22,15 @@ val expand_definitions: autouse:bool -> 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 -> @@ -39,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_visit.ml b/src/expr/e_visit.ml index 3817816f4..fa7f45506 100644 --- a/src/expr/e_visit.ml +++ b/src/expr/e_visit.ml @@ -469,94 +469,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 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 - visitor#expr scx e; - set_to_list unprimed_vars - - -let collect_primed_vars cx e = - let primed_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}, [arg]) -> - assert (not prime_scope); - self#expr (true, cx) arg - | Ix n -> - begin - assert (n >= 1); - let hyp = E_t.get_val_from_id cx n in - match hyp.core with - | Flex name -> - let var_name = name.core in - if (prime_scope && - not (Hashtbl.mem primed_vars var_name)) then - Hashtbl.add primed_vars var_name () - | _ -> () - end - | Apply ({core=Internal ENABLED}, _) -> - assert (not prime_scope) - | Apply ({core=Internal Cdot}, [_; arg2]) -> - assert (not prime_scope); - self#expr scx arg2 - | Apply ({core=Internal UNCHANGED}, [arg]) -> - assert (not prime_scope); - let prime_scope_ = true in - let scx_ = (prime_scope_, cx) in - self#expr scx_ arg - | Sub (_, action, subscript) -> - assert (not prime_scope); - self#expr scx action; - let prime_scope_ = true in - let scx_ = (prime_scope_, cx) in - 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 primed_vars + set_to_list identifiers class virtual ['s] map_rename = object (self : 'self) diff --git a/src/expr/e_visit.mli b/src/expr/e_visit.mli index 421ac0fb9..650f9ea6a 100644 --- a/src/expr/e_visit.mli +++ b/src/expr/e_visit.mli @@ -69,5 +69,4 @@ 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_primed_vars: ctx -> expr -> string list +val collect_identifiers: ctx -> expr -> string list diff --git a/src/method.ml b/src/method.ml index 6bbed1904..ae0c544f0 100644 --- a/src/method.ml +++ b/src/method.ml @@ -38,6 +38,8 @@ type t = | AutoUSE | Lambdify | ENABLEDaxioms + | ENABLEDrewrites + | ENABLEDrules | LevelComparison | Trivial ;; @@ -66,6 +68,8 @@ let timeout m = | AutoUSE -> infinity | Lambdify -> infinity | ENABLEDaxioms -> infinity + | ENABLEDrewrites -> infinity + | ENABLEDrules -> infinity | LevelComparison -> infinity | Trivial -> infinity @@ -99,6 +103,8 @@ let scale_time m s = | AutoUSE -> AutoUSE | Lambdify -> Lambdify | ENABLEDaxioms -> ENABLEDaxioms + | ENABLEDrewrites -> ENABLEDrewrites + | ENABLEDrules -> ENABLEDrules | LevelComparison -> LevelComparison | Trivial -> Trivial ;; @@ -132,6 +138,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)" ;; @@ -165,6 +173,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 7b52f4e37..38ce66a34 100644 --- a/src/method.mli +++ b/src/method.mli @@ -27,6 +27,8 @@ type t = | AutoUSE | Lambdify | ENABLEDaxioms + | ENABLEDrewrites + | ENABLEDrules | LevelComparison | Trivial ;; diff --git a/src/method_prs.ml b/src/method_prs.ml index 7892d03d8..24a064c7a 100644 --- a/src/method_prs.ml +++ b/src/method_prs.ml @@ -47,6 +47,8 @@ and isa_method = lazy begin isa_autouse; isa_lambdify; isa_enabledaxioms; + isa_enabledrewrites; + isa_enabledrules; isa_levelcomparison; isa_trivial; ] @@ -122,6 +124,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 919eda013..3b5c5df2c 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -223,10 +223,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 @@ -788,10 +791,10 @@ procedure map_obvious_proof(proof, mapping, cx) { } ; (* This annotation is used later, when processing each proof obligation, to decide whether a step that uses - `ENABLEDaxioms` depends on a fact of too high level, + `ENABLEDrules` depends on a fact of too high level, and fail with a suitable message. *) - if (HasENABLEDaxioms(cx) /\ (max_level > 1)) { + if (HasENABLEDrules(cx) /\ (max_level > 1)) { proof := Annotate(proof, enabledaxioms_property, FALSE) } else { proof := Annotate(proof, enabledaxioms_property, TRUE) @@ -1083,7 +1086,7 @@ let check_enabled_axioms_map = object (self: 'self) Deque.iter check_assumptions cx; level := !max_level; - (* search for proof directive `ENABLEDaxioms` 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 @@ -1094,7 +1097,7 @@ 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, _, _)}, _, _, _) -> - if (name.core = "ENABLEDaxioms") then + if (name.core = "ENABLEDrules") then found := true | _ -> () end @@ -1103,14 +1106,14 @@ let check_enabled_axioms_map = object (self: 'self) | _ -> () in Deque.iter find_proof_directive cx; - + (* if !found then - print_string "Found ENABLEDaxioms\n"; - + print_string "Found ENABLEDrules\n"; + *) if (!found && (!max_level > 1)) then begin Util.eprintf ~at:pf "%s" - ("ENABLEDaxioms depends on assumption of expression " ^ + ("ENABLEDrules depends on assumption of expression " ^ "level > 1"); (* Util.eprintf "%a@" (Proof.Fmt.pp_print_proof (cx, Ctx.dot)) pf @@ -1216,7 +1219,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 | _ -> () 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 000000000..22fc576e7 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDaxioms_conj_fingerprinting/ENABLEDaxioms_conj_fingerprinting_test.tla @@ -0,0 +1,10 @@ +----------------- MODULE ENABLEDaxioms_conj_fingerprinting_test ---------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..128e06c6c --- /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 000000000..336a01861 --- /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 000000000..2f49027fc --- /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 000000000..ade29ca0b --- /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 000000000..d719dba86 --- /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 000000000..930ca06de --- /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 2af8a9910..d3b30b77d 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 +(* This statement declares two variables. *) +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 000000000..74ede2fa3 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_assignment_level_fingerprint/ENABLEDrewrites_assignment_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +------------ 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: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..4fa97e38b --- /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 000000000..8d1559de3 --- /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 000000000..f58513ad8 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_bpragma_fingerprint/ENABLEDrewrites_bpragma_fingerprint_test.tla @@ -0,0 +1,10 @@ +--------------- MODULE ENABLEDrewrites_bpragma_fingerprint_test ---------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..2b49e7dc8 --- /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 000000000..699295d3d --- /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 000000000..20ffca323 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_case_level_fingerprint/ENABLEDrewrites_case_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +-------------- 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: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..b81e449cf --- /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 000000000..4d0e31e08 --- /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 000000000..7bb6cf3f8 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_conj_level_fingerprint/ENABLEDrewrites_conj_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +-------------- 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: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..9eb29b90a --- /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 000000000..8ccbc59e1 --- /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 000000000..56ad7b287 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_exist_level_fingerprint/ENABLEDrewrites_exist_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +------------- 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: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..c750bf104 --- /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 000000000..d83d36794 --- /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 000000000..49168883b --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_mem_level_fingerprint/ENABLEDrewrites_mem_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +--------------- 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: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..4080e951a --- /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 000000000..2c38940b9 --- /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 000000000..37f3c97b7 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_state_level_fingerprint/ENABLEDrewrites_state_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +-------------- 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: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..90fe37f33 --- /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 000000000..0f1eae195 --- /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 000000000..a97a58131 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrewrites_ternary_level_fingerprint/ENABLEDrewrites_ternary_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +------------ 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: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..6719147a3 --- /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 000000000..1dda6ffc0 --- /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 000000000..501f84fe2 --- /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 000000000..fe785b012 --- /dev/null +++ b/test/fast/enabled_cdot/ENABLEDrules_fingerprint_levels/ENABLEDrules_fingerprint_levels_test.tla @@ -0,0 +1,10 @@ +---- MODULE ENABLEDrules_fingerprint_levels_test ---- + +===================================================== +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 4 obligations proved +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..3bb73e230 --- /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 000000000..df789d9e8 --- /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 000000000..009b62b9d --- /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 000000000..59ade3b66 --- /dev/null +++ b/test/fast/enabled_cdot/ExpandENABLED_level_fingerprint/ExpandENABLED_level_fingerprint_test.tla @@ -0,0 +1,10 @@ +-------------------- MODULE ExpandENABLED_level_fingerprint_test --------------- + +================================================================================ +command: cp v1.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: All 2 obligations proved +command: cp v2.tla temp.tla +command: ${TLAPM} --toolbox 0 0 temp.tla +stderr: obligations failed +command: rm 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 000000000..57957487e --- /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 000000000..1cfb1a6da --- /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 + +================================================================================ From 70b4eaabc6bf0c3fe04e83badba1c0c8677743a5 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Wed, 31 Mar 2021 15:34:48 +0200 Subject: [PATCH 22/39] fixup! fpfile changes These changes are for now kept as a separate commit, in case further rebasing is needed before preparing the pull request for the branch `update_enabled_cdot`. --- src/backend/fpfile.ml | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/src/backend/fpfile.ml b/src/backend/fpfile.ml index 2ad63c4dc..04e8781aa 100644 --- a/src/backend/fpfile.ml +++ b/src/backend/fpfile.ml @@ -14,7 +14,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. *) @@ -48,6 +48,8 @@ module V13 = struct | ExpandCdot | Lambdify | ENABLEDaxioms + | ENABLEDrewrites + | ENABLEDrules | LevelComparison | Trivial @@ -108,6 +110,8 @@ module V13 = struct expandcdotres : sti option; lambdifyres: sti option; enabledaxiomsres: sti option; + enabledrewritesres: sti option; + enabledrulesres: sti option; levelcomparisonres: sti option; };; @@ -235,6 +239,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 @@ -275,6 +281,8 @@ type prover = | Pexpandcdot | Plambdify | Penabledaxioms + | Penabledrewrites + | Penabledrules | Plevelcomparison | Ptrivial ;; @@ -305,6 +313,8 @@ let prover_of_method m = | AutoUSE -> Pautouse | Lambdify -> Plambdify | ENABLEDaxioms -> Penabledaxioms + | ENABLEDrewrites -> Penabledrewrites + | ENABLEDrules -> Penabledrules | LevelComparison -> Plevelcomparison | Trivial -> Ptrivial ;; @@ -433,6 +443,8 @@ let empty = { expandcdotres = None; lambdifyres = None; enabledaxiomsres = None; + enabledrewritesres = None; + enabledrulesres = None; levelcomparisonres = None; };; @@ -461,6 +473,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 ;; @@ -746,6 +760,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 -> @@ -817,6 +835,8 @@ 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; ;; @@ -936,6 +956,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 From 6a4e5f847900954d03b8252366e0d47c6e73976f Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Tue, 25 May 2021 16:51:32 +0200 Subject: [PATCH 23/39] BUG: correct scoping in proof directive `LevelComparison` --- src/expr.mli | 2 +- src/expr/e_level_comparison.ml | 63 +++++++++++++------ src/expr/e_level_comparison.mli | 2 +- ...elComparisonCONSTANT_Module_Scope_test.tla | 25 ++++++++ ...lComparisonCONSTANT_THEOREM_Scope_test.tla | 20 ++++++ .../LevelComparisonSTATE_Scope_test.tla | 18 ++++++ .../enabled_cdot/LevelComparison_test.tla | 24 ++++++- 7 files changed, 133 insertions(+), 21 deletions(-) create mode 100644 test/fast/enabled_cdot/LevelComparisonCONSTANT_Module_Scope_test.tla create mode 100644 test/fast/enabled_cdot/LevelComparisonCONSTANT_THEOREM_Scope_test.tla create mode 100644 test/fast/enabled_cdot/LevelComparisonSTATE_Scope_test.tla diff --git a/src/expr.mli b/src/expr.mli index 2cd4cc9a6..b192168c3 100644 --- a/src/expr.mli +++ b/src/expr.mli @@ -468,7 +468,7 @@ module LevelComparison : sig open 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_level_comparison.ml b/src/expr/e_level_comparison.ml index f68301375..0dfc50f10 100644 --- a/src/expr/e_level_comparison.ml +++ b/src/expr/e_level_comparison.ml @@ -33,21 +33,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) @@ -55,13 +58,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 @@ -74,7 +93,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; @@ -713,15 +732,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; @@ -743,7 +763,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 diff --git a/src/expr/e_level_comparison.mli b/src/expr/e_level_comparison.mli index 734d787f5..00a261e92 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/test/fast/enabled_cdot/LevelComparisonCONSTANT_Module_Scope_test.tla b/test/fast/enabled_cdot/LevelComparisonCONSTANT_Module_Scope_test.tla new file mode 100644 index 000000000..7475fe304 --- /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 000000000..a837eca48 --- /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 000000000..42b1461f3 --- /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 index 86c00542b..428bd82b8 100644 --- a/test/fast/enabled_cdot/LevelComparison_test.tla +++ b/test/fast/enabled_cdot/LevelComparison_test.tla @@ -1,6 +1,6 @@ ------------------------- MODULE LevelComparison_test -------------------------- (* Tests for the proof directive LevelComparison. *) -EXTENDS TLAPS +EXTENDS Integers, TLAPS VARIABLE x @@ -87,4 +87,26 @@ THEOREM 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 + ================================================================================ From 23f6f0b9e092748b68a6c6871d915263ca578a5b Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Wed, 26 May 2021 17:10:52 +0200 Subject: [PATCH 24/39] API: print level comparison message only when verbose --- src/expr/e_level_comparison.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/expr/e_level_comparison.ml b/src/expr/e_level_comparison.ml index 0dfc50f10..5242734fe 100644 --- a/src/expr/e_level_comparison.ml +++ b/src/expr/e_level_comparison.ml @@ -773,9 +773,11 @@ let check_level_change cx expr = inner_hyps cx_hyps cx_goal hyp active in check_context f hyps; let proved = !found in - begin if proved then + begin if proved then begin + if !Params.verbose then Util.printf ~at:expr ~prefix:"[INFO]" "%s" - ("\nProved level comparison\n") + ("Proved level comparison\n") + end else failwith "LevelComparison proof directive did not succeed.\n" end; let core = (if proved then Internal TRUE else expr.core) in From c758c25758c6e9cc98814817aa90c34f07e7fbc3 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Wed, 28 Jul 2021 20:42:15 +0200 Subject: [PATCH 25/39] BUG: correct typo --- src/expr/e_levels.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/expr/e_levels.ml b/src/expr/e_levels.ml index 55f6caa07..ed890f0a7 100644 --- a/src/expr/e_levels.ml +++ b/src/expr/e_levels.ml @@ -350,7 +350,7 @@ class virtual ['s] level_computation = object (self : 'self) | Builtin.SelectSeq -> make_level_info_arity 0 2 | Builtin.OneArg -> (* :> *) - make_level_info_arity 0 1 + make_level_info_arity 0 2 | Builtin.Extend -> (* @@ *) make_level_info_arity 0 2 | Builtin.Print -> From ee56b3de276c74fa5eaf20645d01cd917811af10 Mon Sep 17 00:00:00 2001 From: Martin Date: Fri, 5 Aug 2022 00:11:35 +0200 Subject: [PATCH 26/39] add labeled arguments in call of expand_enabled_cdot to avoid warning in ocaml 4.13 --- src/backend/prep.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/backend/prep.ml b/src/backend/prep.ml index ebc37ab5b..e2c1bff07 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -983,10 +983,10 @@ let normalize_expand ob fpout thyout record let ob = normalize_expr ob in try let ob = expand_enabled_cdot - ob expand_enabled expand_cdot autouse - apply_lambdify enabled_axioms enabled_rewrites - enabled_rules level_comparison - used_identifiers 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, From a963bd37372d8ca0ba627687d80d4116447971aa Mon Sep 17 00:00:00 2001 From: merz Date: Tue, 4 Oct 2022 16:48:14 +0200 Subject: [PATCH 27/39] add example for simple liveness proof, contributed by Andreas Recke --- examples/CountDown.tla | 106 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 106 insertions(+) create mode 100644 examples/CountDown.tla diff --git a/examples/CountDown.tla b/examples/CountDown.tla new file mode 100644 index 000000000..6b8613bfa --- /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 + +============================================================================= From 9a6caddd79b5d2ed6e0d0e2871a7e45bda8c1715 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sat, 31 Aug 2024 19:14:33 +0300 Subject: [PATCH 28/39] Print exception backtraces in LSP. Signed-off-by: Karolis Petrauskas --- lsp/lib/server/handlers.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lsp/lib/server/handlers.ml b/lsp/lib/server/handlers.ml index f4e8f8ea0..4ba133118 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 -> From f002d245c5e20a27ca8acc4de9f4d4a09b92aebd Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 1 Sep 2024 12:57:57 +0300 Subject: [PATCH 29/39] Proofs in `examples/EWD840.tla` fixed. Signed-off-by: Karolis Petrauskas --- examples/EWD840.tla | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/examples/EWD840.tla b/examples/EWD840.tla index 12ce46d7f..778fafeea 100644 --- a/examples/EWD840.tla +++ b/examples/EWD840.tla @@ -173,7 +173,7 @@ LEMMA TypeCorrect == Spec => []TypeOK THEOREM Spec => []TerminationDetection (* 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 @@ -213,7 +213,7 @@ LEMMA Inv_implies_Termination == Inv => TerminationDetection <2>. QED BY <2>4, <2>5 DEF Nodes <1>. QED - BY <1>1 DEF TerminationDetection, terminationDetected + BY <1>1 DEF TerminationDetection, terminationDetected, allInactive ----------------------------------------------------------------------------- (***************************************************************************) @@ -256,7 +256,7 @@ LEMMA EnabledControlled == PROVE PassToken(i) => <>_vars OBVIOUS <2>. QED - BY DEF PassToken, vars, TypeOK + BY DEF PassToken, vars, TypeOK, Nodes <1>3. Controlled <=> <>_vars BY <1>1, <1>2 DEF Controlled <1>4. (ENABLED Controlled) <=> ENABLED <>_vars @@ -312,7 +312,7 @@ LEMMA TerminationRound1 == 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 + <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) @@ -371,7 +371,7 @@ LEMMA TerminationRound2 == 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 + <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) @@ -426,7 +426,7 @@ LEMMA TerminationRound3 == 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 + <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) From 4f4344bcc9a9bddaa3cb6184a963b1bfb5ccc6bf Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 1 Sep 2024 12:59:46 +0300 Subject: [PATCH 30/39] Temporary workaround for making the LSP to work. Signed-off-by: Karolis Petrauskas --- lsp/lib/docs/proof_step.ml | 4 +++- src/backend.mli | 3 +++ src/backend/prep.mli | 2 ++ 3 files changed, 8 insertions(+), 1 deletion(-) diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml index 0e021e01c..768f73d49 100644 --- a/lsp/lib/docs/proof_step.ml +++ b/lsp/lib/docs/proof_step.ml @@ -353,7 +353,9 @@ 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 -> + let o = Tlapm_lib.Backend.Prep.add_expr_level o in (* TODO: Fix this properly. More conditions have to be satisfied. *) + Tlapm_lib.Backend.Fingerprints.write_fingerprint o | Some _ -> o in let o = Obl.of_parsed_obligation o Proof_status.Pending in diff --git a/src/backend.mli b/src/backend.mli index 34aed3965..c88f2eea2 100644 --- a/src/backend.mli +++ b/src/backend.mli @@ -22,6 +22,9 @@ module Types: sig } end +module Prep: sig + val add_expr_level: Proof.T.obligation -> Proof.T.obligation +end module Fingerprints: sig val write_fingerprint: diff --git a/src/backend/prep.mli b/src/backend/prep.mli index 273603d0b..481180b66 100644 --- a/src/backend/prep.mli +++ b/src/backend/prep.mli @@ -28,3 +28,5 @@ val normalize: auto_expand_defs: bool -> obligation *) + +val add_expr_level: obligation -> obligation From cfacd96fb3ee18f4bddbeb6f3739cc9c105b5dac Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 1 Sep 2024 13:37:32 +0300 Subject: [PATCH 31/39] Fix proof in `examples/SimpleMutex.tla`. Signed-off-by: Karolis Petrauskas --- examples/SimpleMutex.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/SimpleMutex.tla b/examples/SimpleMutex.tla index 653f7c485..6296050a8 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 From 77ac33f79a942319bd9013ec6478e290cd60d4fa Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 1 Sep 2024 13:46:47 +0300 Subject: [PATCH 32/39] Fix proof in `examples/SimpleEventually.tla`. Signed-off-by: Karolis Petrauskas --- examples/SimpleEventually.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/SimpleEventually.tla b/examples/SimpleEventually.tla index 04a0d3da8..9ae782dc6 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 From 7f63bdd7766c43e92168d751ae1f682c17a02b55 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Mon, 2 Sep 2024 00:07:11 +0300 Subject: [PATCH 33/39] Properly take the obligation fingerprints in the LSP. Signed-off-by: Karolis Petrauskas --- lsp/lib/docs/proof_step.ml | 4 +- src/backend.mli | 2 +- src/backend/prep.ml | 168 ++++++++++++++++++++----------------- src/backend/prep.mli | 2 +- 4 files changed, 95 insertions(+), 81 deletions(-) diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml index 768f73d49..dfa99dad1 100644 --- a/lsp/lib/docs/proof_step.ml +++ b/lsp/lib/docs/proof_step.ml @@ -353,9 +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 -> - let o = Tlapm_lib.Backend.Prep.add_expr_level o in (* TODO: Fix this properly. More conditions have to be satisfied. *) - 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/src/backend.mli b/src/backend.mli index c88f2eea2..31c37b5ec 100644 --- a/src/backend.mli +++ b/src/backend.mli @@ -23,7 +23,7 @@ module Types: sig end module Prep: sig - val add_expr_level: Proof.T.obligation -> Proof.T.obligation + val prepare_obligation: Proof.T.obligation -> Proof.T.obligation end module Fingerprints: sig diff --git a/src/backend/prep.ml b/src/backend/prep.ml index 81cc23663..18c6b4bc5 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -1453,6 +1453,97 @@ let is_trivial x = try ignore (Lazy.force x); true with Nontrivial -> false +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 + 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_expr_level ob)) + in + let p = lazy (normalize_expand (Lazy.force const_fp_ob) + fpout thyout record + ~expand_enabled + ~expand_cdot + ~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. @@ -1461,82 +1552,7 @@ 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 - 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 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. - *) - let (const_fp_ob, p) = 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) - end else begin - let const_fp_ob = - lazy (Fingerprints.write_fingerprint (add_expr_level ob)) - in - let p = lazy (normalize_expand (Lazy.force const_fp_ob) - fpout thyout record - ~expand_enabled - ~expand_cdot - ~autouse - ~apply_lambdify - ~enabled_axioms - ~enabled_rewrites - ~enabled_rules - ~level_comparison) - in - (const_fp_ob, p) - end in + 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 diff --git a/src/backend/prep.mli b/src/backend/prep.mli index 481180b66..6f116ca7e 100644 --- a/src/backend/prep.mli +++ b/src/backend/prep.mli @@ -29,4 +29,4 @@ val normalize: obligation *) -val add_expr_level: obligation -> obligation +val prepare_obligation: obligation -> obligation From 3a04bf6c4216ee9f532ff217da229f24e0fbf8e5 Mon Sep 17 00:00:00 2001 From: Damien Doligez Date: Tue, 12 Nov 2024 15:57:43 +0100 Subject: [PATCH 34/39] change magic number for fingerprint files Signed-off-by: Damien Doligez --- src/backend/fpfile.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/backend/fpfile.ml b/src/backend/fpfile.ml index 2b81d0d56..8dfe71ea8 100644 --- a/src/backend/fpfile.ml +++ b/src/backend/fpfile.ml @@ -153,8 +153,8 @@ open V13 let fptbl = ref (Hashtbl.create 500 : V13.tbl) -let old_magic_number = 20101013 -let magic_number = 20210223 +let old_magic_numbers = [20101013; 20210223] +let magic_number = 20241112 let write_fp_table oc = output_value oc magic_number; @@ -568,7 +568,7 @@ let load_fingerprints_aux file = if Sys.file_exists file then begin let ic = open_in_bin file in let magic = Marshal.from_channel ic in - if magic = old_magic_number then + if List.mem magic old_magic_numbers then raise(FpFileOlderMagicNumber); if magic <> magic_number then raise(FpFileCorrupted); let v = Marshal.from_channel ic in From 609d46704315a2a9396fdf806ff972ac20a1aa23 Mon Sep 17 00:00:00 2001 From: Damien Doligez Date: Tue, 19 Nov 2024 16:31:38 +0100 Subject: [PATCH 35/39] update comment Signed-off-by: Damien Doligez --- src/backend/fpfile.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/backend/fpfile.ml b/src/backend/fpfile.ml index 8dfe71ea8..684fc2255 100644 --- a/src/backend/fpfile.ml +++ b/src/backend/fpfile.ml @@ -126,7 +126,7 @@ module V13 = struct (* The key is the MD5 converted to hex. *) (* File format: - - magic number as a marshalled integer = 20101013 + - magic number as a marshalled integer = 20241112 - Fpver13 of tbl - any number of (Digest.t, sti list) pairs *) From 671ac9eaaa38a240b9df0b8a918f7f870cea9a99 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 22 Dec 2024 21:12:45 +0200 Subject: [PATCH 36/39] Damien's comments addressed. Co-authored-by: Damien Doligez Signed-off-by: Karolis Petrauskas --- examples/EWD840.tla | 2 +- lsp/lib/server/handlers.ml | 2 +- src/backend/fingerprints.ml | 3 ++- src/expr/e_action.ml | 3 +-- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/examples/EWD840.tla b/examples/EWD840.tla index 778fafeea..e367f00af 100644 --- a/examples/EWD840.tla +++ b/examples/EWD840.tla @@ -132,7 +132,7 @@ Inv == USE NAssumption -(* TypeOK is an inductive invariant *) +(* TypeCorrect is an inductive invariant *) LEMMA TypeCorrect == Spec => []TypeOK <1>. USE DEF TypeOK, Nodes, Color <1>1. Init => TypeOK diff --git a/lsp/lib/server/handlers.ml b/lsp/lib/server/handlers.ml index 4ba133118..b3450d837 100644 --- a/lsp/lib/server/handlers.ml +++ b/lsp/lib/server/handlers.ml @@ -350,8 +350,8 @@ module Make (CB : Callbacks) = struct try handle_jsonrpc_request req state with exc -> let open Jsonrpc.Response.Error in - let exc_str = Printexc.to_string exc in let exc_btr = Printexc.get_backtrace () in + let exc_str = Printexc.to_string exc 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 diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index b98ab458c..90817bb0a 100644 --- a/src/backend/fingerprints.ml +++ b/src/backend/fingerprints.ml @@ -579,7 +579,8 @@ let fingerprint ob = "Level<=1" else "Level>1" - end else "" in + end + else "" in let buf = fp_sequent ob.Proof.T.obl.core in bprintf buf "%s" enabledrules; (* Buffer.output_buffer stdout buf; *) diff --git a/src/expr/e_action.ml b/src/expr/e_action.ml index d32980e65..deebbb924 100644 --- a/src/expr/e_action.ml +++ b/src/expr/e_action.ml @@ -1449,8 +1449,7 @@ let collect_vars cx e primed = match a with | None -> () | Some primed_vars -> - if (not (Hashtbl.mem primed_vars var_name)) then - Hashtbl.add primed_vars var_name () + Hashtbl.replace primed_vars var_name () end | Fresh (_, _, kind, _) -> begin From 9f03ed40319a99aef3851f81d208b0543bebd642 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 22 Dec 2024 22:38:29 +0200 Subject: [PATCH 37/39] Fixes after the merge. Signed-off-by: Karolis Petrauskas --- src/expr/e_visit.ml | 1 + src/module/m_elab.ml | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/expr/e_visit.ml b/src/expr/e_visit.ml index 3532d35eb..37e49cd42 100644 --- a/src/expr/e_visit.ml +++ b/src/expr/e_visit.ml @@ -1514,6 +1514,7 @@ let collect_identifiers cx e = method hyp scx h = begin match h.core with | Fresh (nm, _, _, _) -> add_id nm + | FreshTuply (hints, _) -> List.iter add_id hints | Flex nm -> add_id nm | Defn _ -> () (* handled in the method `self#defn` *) | Fact _ -> () end; diff --git a/src/module/m_elab.ml b/src/module/m_elab.ml index 44d98dbe5..c4ce7b615 100644 --- a/src/module/m_elab.ml +++ b/src/module/m_elab.ml @@ -988,8 +988,10 @@ let check_enabled_axioms_map = object (self: 'self) | Pcase _ | Have _ | Take _ + | TakeTuply _ | Witness _ - | Pick _ -> + | Pick _ + | PickTuply _ -> assert false (* after `Proof.Simplify.simplify` *) | Define dfs -> let (scx, dfs) = self#defns scx dfs in @@ -1057,7 +1059,7 @@ let check_enabled_axioms_map = object (self: 'self) () (* Hidden facts are not usable in the proof, so they do not contribute to the proof level. *) - | Fresh _ | Flex _ -> + | Fresh _ | FreshTuply _ | Flex _ -> () (* Declarations of operators do not have a notion of being usable in the proof, so they do not contribute to the From 07d8ce0d664520e8ca04e92ac9a3b6998e58ead7 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 22 Dec 2024 23:04:45 +0200 Subject: [PATCH 38/39] Printing to stdout breaks the LSP server, so use stderr. Signed-off-by: Karolis Petrauskas --- src/expr/e_action.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/expr/e_action.ml b/src/expr/e_action.ml index fd63a6e0c..695e2acd5 100644 --- a/src/expr/e_action.ml +++ b/src/expr/e_action.ml @@ -130,7 +130,7 @@ let expand_definition hyp expr (Util.eprintf ~at:expr "%s" msg); failwith msg (* SoundnessCheck *) end; - Util.printf ~at:expr ~prefix:"[INFO]: " + Util.eprintf ~at:expr ~prefix:"[INFO]: " "Auto-expanding the definition of operator: %s\n" name; match expr.core with | Apply ({core=Ix n}, args) -> From 50b8e3630a9c28e41d60d93f444a7404d9484c3f Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 22 Jun 2025 17:49:03 +0300 Subject: [PATCH 39/39] Make LSP independent of level calculations. Signed-off-by: Karolis Petrauskas --- lsp/lib/docs/proof_step.ml | 7 ++++++- src/backend.mli | 4 ++-- src/backend/fingerprints.ml | 22 ++++++++++++---------- src/backend/fingerprints.mli | 10 ++++++++++ 4 files changed, 30 insertions(+), 13 deletions(-) diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml index b7c989e85..52f36bc9d 100644 --- a/lsp/lib/docs/proof_step.ml +++ b/lsp/lib/docs/proof_step.ml @@ -392,7 +392,12 @@ 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.Prep.prepare_obligation o + | None -> + (* `Tlapm_lib.Backend.Prep.prepare_obligation o` works too slow here. *) + let fingerprint = + Tlapm_lib.Backend.Fingerprints.fingerprint ~ignore_levels:true o + in + { o with fingerprint = Some fingerprint } | Some _ -> o in let o = Obl.of_parsed_obligation o in diff --git a/src/backend.mli b/src/backend.mli index 31c37b5ec..5339594e2 100644 --- a/src/backend.mli +++ b/src/backend.mli @@ -27,8 +27,8 @@ module Prep: sig end module Fingerprints: sig - val write_fingerprint: - Proof.T.obligation -> Proof.T.obligation + val fingerprint: + ?ignore_levels:bool -> Proof.T.obligation -> string end module Fpfile: sig diff --git a/src/backend/fingerprints.ml b/src/backend/fingerprints.ml index 9bbf7cb94..e870b1d2f 100644 --- a/src/backend/fingerprints.ml +++ b/src/backend/fingerprints.ml @@ -23,8 +23,8 @@ type ident = (************************) module Stack : sig - type 'a t = private { mutable stack : 'a array; mutable length : int } - val create : int -> 'a -> 'a t + type 'a t = private { mutable stack : 'a array; mutable length : int ; ignore_levels : bool } + val create : int -> 'a -> bool -> 'a t val get : 'a t -> int -> 'a val set : 'a t -> int -> 'a -> unit val push : 'a t -> 'a -> unit @@ -33,12 +33,13 @@ module Stack : sig end = struct type 'a t = { mutable stack : 'a array ; - mutable length : int } + mutable length : int ; + ignore_levels : bool } - let create n a = {stack = (Array.make n a); length = 0} + let create n a il = {stack = (Array.make n a); length = 0; ignore_levels = il} - let copy h = let cp = Array.copy h.stack in {stack=cp; length = h.length} + let copy h = let cp = Array.copy h.stack in {stack=cp; length = h.length; ignore_levels = h.ignore_levels} let get h i = Array.get h.stack (h.length -i) @@ -448,7 +449,7 @@ and fp_sequent stack buf sq = if !r then bprintf buf "$Def(%d,%d)" (match v with Identhypi i -> i | _ -> assert false) - (Expr.Levels.get_level e) + (if stack.ignore_levels then -1 else Expr.Levels.get_level e) | Defn ({core = Bpragma (nm, _, _)}, _, Hidden, _) -> Stack.push stack (IdentBPragma nm.core, ref false); spin stack cx; @@ -573,14 +574,14 @@ let print_fp sq buf = Buffer.output_buffer stdout buf; print_string "\nEnd of string used to create fingerprint\n\n" -let fp_sequent sq = +let fp_sequent sq ignore_levels = let buf = Buffer.create 17 in - fp_sequent (Stack.create 5 (No, ref false)) buf sq ; + fp_sequent (Stack.create 5 (No, ref false) ignore_levels) buf sq ; (* print_fp sq buf; *) buf -let fingerprint ob = +let fingerprint ?(ignore_levels=false) ob = let enabledrules = if Expr.T.has_enabledaxioms ob.obl then begin if Expr.T.get_enabledaxioms ob.obl then "Level<=1" @@ -588,8 +589,9 @@ let fingerprint ob = "Level>1" end else "" in - let buf = fp_sequent ob.Proof.T.obl.core in + let buf = fp_sequent ob.Proof.T.obl.core ignore_levels in bprintf buf "%s" enabledrules; + if ignore_levels then bprintf buf ";IgnoreLevels"; (* Buffer.output_buffer stdout buf; *) to_string buf diff --git a/src/backend/fingerprints.mli b/src/backend/fingerprints.mli index 462af4fa2..37ef1b53c 100644 --- a/src/backend/fingerprints.mli +++ b/src/backend/fingerprints.mli @@ -6,3 +6,13 @@ Copyright (C) 2011 INRIA and Microsoft Corporation (* tlapm.ml *) val write_fingerprint: Proof.T.obligation -> Proof.T.obligation + +val fingerprint: + ?ignore_levels:bool -> Proof.T.obligation -> string +(** Returns a fingerprint for an obligation. By default the levels + are expected to be assigned to the expressions in the obligation + and are used when calculating the fingerprint. If [~ignore_levels] + is set to [true], level information will be ignored. This is + only added for calculating a hash of an obligation fast enough + to use it in the LSP server. It must not be used to lookup the + proof state in the actual proof-checking. *)