Concerning the previous discussion, I believe there was no talking at cross purposes, as prior to your new reference to [Cohn, 1989] we were discussing within the realm of mathematics only. Especially the design of Mark's HOL Zero, which was chosen as an example by Peter and Makarius, focuses on - level 1: the logical kernel (the logic and its internal representation), and - level 2: the printer and parser (external representation), but [Cohn, 1989, in particular section 6.1., available online at https://doi.org/10.1007/BF00243000 ] mainly discusses the correspondence between the 2nd level (e.g., the mathematical model/description of a microprocessor) and - level 3: the concept/reality (e.g., the intended design or the actual device) which goes beyond mathematics itself.
Some of the recent issues were a) preserving logical dependencies (respectively, its lack in the case of type class instantiation) - https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/msg00020.html which might be used to construe an inconsistency - https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/msg00049.html b) the previous inconsistency, again caused by type classes - p. 2 (example 2) at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf Clearly, these are (should be) matters of the logical kernel. Therefore, it is reasonable to expect the kernel to preserve logical dependencies, and not a "fanciful interpretation of the documentation" - https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/msg00022.html which again is an argument for getting rid of the responsibility for logical consistency, the purpose the logical kernel is designed for. I agree with Peter that the logical kernel (level 1) should be sound independent of whether the user is malicious or not. Concerning the printer and parser (level 2), immunity against a malicious user is desirable, but probably possible only in less interactive provers/checkers like HOL Zero or R0. For this immunity, both I. Freek Wiedijk's notion of Pollack-consistency - http://www.sciencedirect.com/science/article/pii/S157106611200028X/pdf?md5=04ceb92a245b5bde8c4eca0610032293&pid=1-s2.0-S157106611200028X-main.pdf II. and Mark's notion of faithfulness - http://www.proof-technologies.com/papers/hzsyntax_itp2016.pdf should be implemented, as was done for R0. In these papers, both authors actually assume the role of the malicious user in order to examine the various systems. For Isabelle, I have attached an exploit of the type class instantiation such that the 'taint' of the inconsistency in hidden, but still the "sorry" workaround has to be used. For R0, I have attached an implementation of Mark's scenario: "A printer that printed false as true and true as false might be Pollack-consistent but would not be faithful." http://www.proof-technologies.com/papers/hzsyntax_itp2016.pdf (p. 2) (This is not possible in standard mode, i.e., without explicitly passing the flag "–allow-definition-removal" and with the standard definitions in "basics.r0.txt" either as first command line argument or included at the beginning of the file.) ____________________________________________________ Ken Kubota http://doi.org/10.4444/100 Commands: ./R0 --allow-definition-removal no_faithfulness.r0.txt ./R0 --allow-definition-removal no_faithfulness.r0.txt > no_faithfulness.r0.out.txt ./R0 basics.r0.txt no_faithfulness.r0.txt > Am 10.07.2017 um 19:40 schrieb Lawrence Paulson <l...@cam.ac.uk>: > > I think that we are talking at cross purposes here. Of course we want our > systems to be sound, and a kernel architecture is a great help in this, as we > have known for 40 years. But even with a kernel architecture, it is easy for > a result to be misrepresented. See e.g. > >> Avra Cohn. The Notion of Proof in Hardware Verification. J. Autom. >> Reasoning5(2): 127-139 (1989) > > The proof kernel is no defence whatever against misrepresentation or > misunderstanding, so it’s important that formal documents are openly > available for inspection. > > Larry Paulson > > >> On 10 Jul 2017, at 10:10, Peter Lammich <lamm...@in.tum.de> wrote: >> >> On Sa, 2017-07-08 at 19:59 +0100, Lawrence Paulson wrote: >>> "We have been given a proof of X; Is it credible?" >> >> At this point, I second Ken. Although having human-readable machine >> checked proofs is certainly a nice feature to get an idea of how a >> proof works, the main points to check should be the statement of the >> theorem, including the definitions (syntax tweaks, etc) it uses, as >> well as the axioms its proof uses. Then, one relies on the logical >> inference kernel that the proof is actually correct. >> In particular, auxiliary lemmas and definitions only used for the >> proof, but not in the main statement of the theorem, should be >> irrelevant for trusting the theorem. >> >> This principle should, in first place, be independent of whether the >> user is malicious or not. However, in Isabelle, the malicious user has >> a lot of possibilities to hide tweaks from a reviewer, while, in >> HOLZero, these possibilities are very limited (if existent at all). >> >> >> Actually, Isabelle contains many tools in this spirit, for example, >> even the simplifier or classical reasoner apply some transformations on >> the theorems provided to them. More high-level tools like function >> package or datatype package even do really complex proofs, completely >> hidden from the user. >> >> -- >> Peter ____________________________________________________ Scratch.thy ____________________________________________________ (* check which oracles a theorem depends on from the ML level *) (* source: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/msg00019.html *) theory Scratch imports Main keywords "check_sorry" :: diag begin ML ‹ val get_oracles = Proofterm.all_oracles_of o Proofterm.strip_thm o Thm.proof_body_of val contains_sorry = exists (fn (a, _) => a = "Pure.skip_proof") o get_oracles fun report_sorry ctxt = if Context_Position.is_visible ctxt then Output.report [Markup.markup Markup.bad "Proof arises from sorry oracle!"] else (); fun check_sorry ctxt th = if contains_sorry th then report_sorry ctxt else () fun check_sorry_cmd thm_ref st = let val ctxt = Toplevel.context_of st val th = Proof_Context.get_fact_single ctxt thm_ref in check_sorry ctxt th end val _ = Outer_Syntax.command @{command_keyword check_sorry} "Check theorem for sorry" (Parse.thm >> (fn (th, _) => Toplevel.keep (check_sorry_cmd th))); › (* Usage: *) lemma one_add_1_eq_3: "1 + 1 = 3" sorry check_sorry HOL.refl check_sorry one_add_1_eq_3 (* hide the 'taint' of a theorem by going through a type class instantiation *) (* source: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/msg00020.html *) class foo = semiring_1 + assumes foo: "1 + 1 = 3" instance nat :: foo by intro_classes (rule one_add_1_eq_3) lemmas one_add_1_eq_3' = foo [where ?'a = nat] check_sorry one_add_1_eq_3' (* inconsistency without explicit dependency on sorry *) (* new (no source) *) lemma incons_one_add_1_eq_3: "(1::nat) + 1 = 3 ∧ 1 + 1 ≠ 3" sorry class incons_foo = semiring_1 + assumes incons_foo: "1 + 1 = 3 ∧ 1 + 1 ≠ 3" instance nat :: incons_foo by intro_classes (rule incons_one_add_1_eq_3) lemmas false' = incons_foo [where ?'a = nat] check_sorry false' theorem False using false' by auto ____________________________________________________ no_faithfulness.r0.txt ____________________________________________________ ## read some standard definitions including T and F << definitions1.r0.txt ## define symbol 'MYDEF' as truth (T), ## and also show the full definition of truth (===) ## := MYDEF T := MYDEF T ## definition of truth (T) in Q0: Q=Q ## https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu ## definition of truth (T) in R0: === ## http://www.owlofminerva.net/files/formulae.pdf (p. 359) ## now show MYDEF by establishing: MYDEF = MYDEF ## (the program will automatically use the shortest label, in this case T) ## §= MYDEF §= MYDEF ## remove definition labels T and F := T := F ## (maliciously) attach definition label F to truth (===) := F ((={{{o,@},@}}_={@}){{o,@}}_={@}) ## show MYDEF again by establishing: MYDEF = MYDEF ## §= MYDEF §= MYDEF ## Note: truth (usually T) appeared as F! ____________________________________________________ no_faithfulness.r0.out.txt ____________________________________________________ ## read some standard definitions including T and F << definitions1.r0.txt ## define symbol 'MYDEF' as truth (T), ## and also show the full definition of truth (===) ## := MYDEF T := MYDEF ((={{{o,@},@}}_={@}){{o,@}}_={@}) # wff 12 : ((=_=)_=) := MYDEF T ## definition of truth (T) in Q0: Q=Q ## https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu ## definition of truth (T) in R0: === ## http://www.owlofminerva.net/files/formulae.pdf (p. 359) ## now show MYDEF by establishing: MYDEF = MYDEF ## (the program will automatically use the shortest label, in this case T) ## §= MYDEF §= T # ((=_T)_T) ## remove definition labels T and F := T := F ## (maliciously) attach definition label F to truth (===) := F ((={{{o,@},@}}_={@}){{o,@}}_={@}) # wff 12 : ((=_=)_=) := F MYDEF ## show MYDEF again by establishing: MYDEF = MYDEF ## §= MYDEF §= F # ((=_F)_F) ## Note: truth (usually T) appeared as F! ____________________________________________________ ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
