Re: [isabelle] Isabelle Foundation & Certification



Hello Larry, list,

On 09-16, Larry Paulson wrote:
> It would be interesting to find out how these problems were identified: whether they were looked for out of curiosity, or whether on the other hand they manifested themselves in the course of an actual proof.

I can give more detail for the case of EURO-MILS: We were made aware of 
"Isabelle Isar-Reference Manual (Version 2013-2, pp. 103): "It is at
the discretion of the user to avoid malformed theory specifications!"[1]
Hence first attempt was to rule out use of "consts"[2].
This resulted in people even becoming more curious and playing 
with Kuncar/Popescu.
Moreover, it has been pointed out that even if we rule out "consts" and "defs" in our theories then it is still used e.g. in HOL.thy[3] (probably without 
overloading, but it is hard to judge for me).

The task at hand is not only convincing ourselves (arguably when proving some 
property oneself one usually/sometimes gets a feeling for what is correct
and what not) but also others (who have limited resources).

To give an example: in attached System_Is_Secure.thy the first 
derivation of "System_Is_Secure" (theorem System_Is_Secure_1) 
forces to make the assumptions of "A" and "~A" obvious. This makes 
it harder to cheat ourselves or others.

The second derivation of "System_Is_Secure" (theorem System_Is_Secure_2)
hides the assumptions and could be more easy be overlooked.

My working understanding is (correct if that is wrong!) that fixing 
Isabelle would rule out hidden derivations such as System_Is_Secure_2.

[1] http://isabelle.in.tum.de/doc/isar-ref.pdf p 121 
The (unchecked) option disables global dependency checks for this def-
inition, which is occasionally useful for exotic overloading. It is at
the discretion of the user to avoid malformed theory specifications!
[2] http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper.pdf Section 3.1 "Constants. The Isabelle consts command is not used."
[3] http://afp.sourceforge.net/browser_info/current/HOL/HOL/HOL.html
search for "defs"

---------(inlined: System_Is_Secure.thy, also attached)
theory System_Is_Secure
  imports Main
  begin

consts A :: bool
consts System_Is_Secure :: bool

(* formulation with explicit assumptions, easy for reviewer to spot that user made too strong assumptions *)
theorem System_Is_Secure_1: 
  assumes "A" 
  and "~ A"  
  shows System_Is_Secure
proof-
  from assms show ?thesis by simp
qed

(* Kuncar/Popescu: A Consistent Foundation for Isabelle/HOL, ITP 2015 *)
consts c :: bool
typedef T = "{True, c}" by blast
defs c_bool_def: "c::bool == ~ (ALL(x::T) y. x = y)"
 lemma L: "(ALL(x::T) y. x = y) <-> c"
using Rep_T Rep_T_inject Abs_T_inject by blast
lemma MyFalse: False
using L unfolding c_bool_def by auto

theorem MySystem_Is_Secure [simp]: System_Is_Secure
using MyFalse by simp

(* formulation with implicit assumptions, not that easy for reviewer to spot that user made too strong assumptions *)
theorem System_Is_Secure_2: System_Is_Secure by simp

end


best,

-- 
Holger




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