Re: [isabelle] Isabelle Foundation & Certification



Same posting as parent, this time with attachment attached.

On 09-17, Holger Blasum wrote:
> 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

-- 
Holger Blasum
SYSGO AG Office Mainz
Am Pfaffenstein 14 / D-55270 Klein-Winternheim / Germany
Phone: +49-6136-9948-425 / Fax: +49-6136-9948-10 / SIP:hbl at sysgo.com
E-mail: holger.blasum at sysgo.com / Web: http://www.sysgo.com

Handelsregister/Commercial Registry: HRB Mainz 90 HRB 8066
Vorstand/Executive Board: Knut Degen (CEO), Kai Sablotny (COO)
Aufsichtsratsvorsitzender/Supervisory Board Chairman: Pascal Bouchiat
USt-Id-Nr./VAT-Id-No.: DE 149062328

Meet us at our next events:
http://www.sysgo.com/news-events/events/showsconferences/

Designing with Freescale Seminar
October 1, 2015, Paris - France

MedConf
October 13-16, 2015, Munich - Germany

TRANSRAIL
October 14-15, 2015, Paris - France
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




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