Email Gateway (Aug 22 2022 at 15:45): Email Gateway (Aug 22 2022 at 15:45):From: Ken Kubota <mail@kenkubota.de>
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 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
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
<< definitions1.r0.txt
:= MYDEF T
§= MYDEF
:= T
:= F
:= F ((={{{o,@},@}}_={@}){{o,@}}_={@})
§= MYDEF
no_faithfulness.r0.out.txt
<< definitions1.r0.txt
:= MYDEF ((={{{o,@},@}}_={@}){{o,@}}_={@})
§= T
:= T
:= F
:= F ((={{{o,@},@}}_={@}){{o,@}}_={@})
§= F
Last updated: Apr 30 2024 at 01:06 UTC