|Anonymous | Login | Signup for a new account||2019-05-22 17:56 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002278||Frama-C||Plug-in > wp||public||2017-02-06 13:09||2017-02-06 13:28|
|Platform||Silicon-20161101||OS||Ubuntu 16.04.1 LTS||OS Version|
|Product Version||Frama-C 14-Silicon|
|Target Version||Fixed in Version|
|Summary||0002278: problem with Qed's simplification power|
|Description||Running "frama-c -wp -wp-out wp-out shift.c" on the attached file and inspecting the file "wp-out/typed/foo_post_Alt-Ergo.mlw" shows that lemma "ShiftAssociative" is simplified to "true" (see line 360) by Qed. (The postcondition of foo doesn't matter here, except that it is intentionally unprovable in order to demonstrate the lemma's simplification.)|
This situation doesn't change even when all options to disable Qed functionality (i.e. "-wp-no-bits -wp-no-clean -wp-no-core -wp-no-filter -wp-no-init-summarize-array -wp-no-let -wp-no-pruning -wp-no-simpl -wp-no-simplify-forall -wp-no-simplify-is-cint -wp-no-simplify-type") are given. (In contrast, in the somewhat related issue 0001751, providing option "-wp-no-bits" is sufficient to circumvent the problem.)
While Qed's simplification capabilities are appreciated in general, the disappearance of the lemma can be a problem:
* In many Coq proofs related to C address computation, a similar lemma has to be stated and proven again and again. There seems to be no easy way to make Coq see what is considered trivial by Qed.
* Considering the discussion at https://github.com/OCamlPro/alt-ergo/issues/19, [^] if I understood the Alt-Ergo people right, Alt-Ergo isn't complete on linear arithmetic with arrays (except for quantifier-free formulas). Therefore it sometimes needs trivial lemmas. In the particular example, to make Alt-Ergo prove the goal "reverse", a kind of associtivity property (axiom "arith") is needed that Qed would simplify also to "true", and even Alt-Ergo would.
Generally speaking, Qed should be (configurable such that it is) no stronger than any of the external provers, such as Coq and Alt-Ergo. This would enable the user to provide appropriate prover hints that are not simplified away by Qed. Maybe a command line option to completely switch off Qed is sufficient. As an alternative, a command-line switch could reduce the capabilities of Qed when applied to lemmas, assuming that the user is responsible to give them in an optimal form.
|Tags||No tags attached.|
|Attached Files|| shift.c [^] (157 bytes) 2017-02-06 13:09 [Show Content]
foo_post_Alt-Ergo.mlw [^] (22,728 bytes) 2017-02-06 13:09
edited on: 2017-02-06 13:28
This is a known problem for lemmas.
Actually, we can *not* tune Qed to not be no stronger than SMTs, because this is *precisely* where Qed comes to rescue. Typically, bitwise simplifications are beyond the scope of SMTs, but we can discharge the proofs thanks to (only) Qed. Another example is associativity (typically list-concat) or function-power (typically list-repeat) that can be handled from Qed side, but not easily from SMT one.
However, it is true that we still need to state lemmas to be used by SMTs or Coq, and those lemmas should not be simplified by Qed ! We are looking forward disabling all simplifications when *exporting* lemmas to external provers, but still use all simplifications for proving the lemmas themselves. Hence, "trivial" lemmas get proved by Qed, but are still usable by SMTs.
Before this feature is available (I can't say when), a workaround is to state SMTs lemmas by hand in side library files, and import them through WP-drivers. Typically, have a look at `$(frama-c -print-share-path)/wp/wp.driver` to see how additional library files are imported by WP itself. Drivers are documented in the WP manual, but do not hesitate to require help if needed.
|2017-02-06 13:09||Jochen||New Issue|
|2017-02-06 13:09||Jochen||Status||new => assigned|
|2017-02-06 13:09||Jochen||Assigned To||=> correnson|
|2017-02-06 13:09||Jochen||File Added: shift.c|
|2017-02-06 13:09||Jochen||File Added: foo_post_Alt-Ergo.mlw|
|2017-02-06 13:27||correnson||Note Added: 0006355|
|2017-02-06 13:27||correnson||Note Added: 0006356|
|2017-02-06 13:27||correnson||Status||assigned => acknowledged|
|2017-02-06 13:27||correnson||Note Deleted: 0006356|
|2017-02-06 13:28||correnson||Note Edited: 0006355||View Revisions|
|Copyright © 2000 - 2019 MantisBT Team|