[isabelle] Proof kernel, Pollack-consistency and faithfulness â Re: Verify the legitimacy of a proof?



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 <lp15 at 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 <lammich at 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,@},@}}_={ at }){{o,@}}_={ at })

## 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,@},@}}_={ at }){{o,@}}_={ at })
# 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,@},@}}_={ at }){{o,@}}_={ at })
# wff      12 :  ((=_=)_=)                                  :=  F  MYDEF

## show MYDEF again by establishing: MYDEF = MYDEF
## Â= MYDEF
Â= F
#                ((=_F)_F)

## Note: truth (usually T) appeared as F!
____________________________________________________






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.