From 76c05ee4337c8257a3a63f530530a394803208be Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Mon, 27 Apr 2020 21:55:04 +0200
Subject: [PATCH] renamings in order to be consistent with vsste paper
---
C11-BackEnds/AutoCorres_wrapper/ROOT | 4 +-
...IsPrime_TEC.thy => IsPrime_linear_CCT.thy} | 16 ++--
..._linear_CET.thy => IsPrime_linear_TCC.thy} | 14 +--
.../examples/IsPrime_sqrt_CAS.thy | 4 +-
...rime_sqrt_CET.thy => IsPrime_sqrt_TCC.thy} | 90 ++++---------------
5 files changed, 35 insertions(+), 93 deletions(-)
rename C11-BackEnds/AutoCorres_wrapper/examples/{IsPrime_TEC.thy => IsPrime_linear_CCT.thy} (97%)
rename C11-BackEnds/AutoCorres_wrapper/examples/{IsPrime_linear_CET.thy => IsPrime_linear_TCC.thy} (93%)
rename C11-BackEnds/AutoCorres_wrapper/examples/{IsPrime_sqrt_CET.thy => IsPrime_sqrt_TCC.thy} (77%)
diff --git a/C11-BackEnds/AutoCorres_wrapper/ROOT b/C11-BackEnds/AutoCorres_wrapper/ROOT
index df9c7f3c147..83ef64ac739 100644
--- a/C11-BackEnds/AutoCorres_wrapper/ROOT
+++ b/C11-BackEnds/AutoCorres_wrapper/ROOT
@@ -53,9 +53,9 @@ session Isabelle_C_AutoCorres_examples = Isabelle_C_AutoCorres +
"examples/CList"
"examples/FactorialTest"
"examples/FibProof"
- "examples/IsPrime_linear_CET"
+ "examples/IsPrime_linear_TCC"
"examples/IsPrime_sqrt_CAS"
- "examples/IsPrime_sqrt_CET"
+ "examples/IsPrime_sqrt_TCC"
"examples/IsPrime_sqrt_opt_CET"
"examples/IsPrime_TEC"
"examples/ListRev"
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy
similarity index 97%
rename from C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy
rename to C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy
index bad6a44f4f8..449968266d8 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.thy
@@ -65,7 +65,7 @@ supported by Isabelle/C. It is characteristic for this style that developers of
verification teams can be separated, as is required by many certification standards.
\<close>
-theory IsPrime_TEC
+theory IsPrime_linear_CCT
imports
Isabelle_C_AutoCorres.AutoCorres_Wrapper
"HOL-Computational_Algebra.Primes"
@@ -77,19 +77,17 @@ C \<open>
//@ #declare [[AutoCorres]]
#define SQRT_UINT_MAX 65536
- /* We prove locally some facts on this C preprocessor macro, which is internally
- converted into an Isabelle/HOL definition: */
+ /* We prove locally some facts on this C preprocessor macro,
+ which is internally converted into an Isabelle/HOL definition: */
/*@
lemma uint_max_factor [simp]:
"UINT_MAX = SQRT_UINT_MAX * SQRT_UINT_MAX - 1"
by (clarsimp simp: UINT_MAX_def SQRT_UINT_MAX_def)
- */
-
-
- /* in the sequel, we give the definitions and theory relevant for the statement of the invariant */
+ */
/*@
- definition "partial_prime p (n :: nat) \<equiv> (1 < p \<and> (\<forall>i \<in> {2 ..< min p n}. \<not> i dvd p))"
+ definition "partial_prime p (n :: nat) \<equiv>
+ (1 < p \<and> (\<forall>i \<in> {2 ..< min p n}. \<not> i dvd p))"
lemma partial_prime_ge [simp]:
"\<lbrakk> p' \<ge> p \<rbrakk> \<Longrightarrow> partial_prime p p' = prime p"
@@ -258,7 +256,7 @@ C \<open>
/* No factors. */
return 1;
}
- /*@
+ /*@ (* original NICTA proof *)
theorem (in is_prime) is_prime_faster_correct:
notes times_nat.simps(2) [simp del] mult_Suc_right [simp del]
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CET.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_TCC.thy
similarity index 93%
rename from C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CET.thy
rename to C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_TCC.thy
index d0816c64215..7ed16f81d1b 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CET.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_TCC.thy
@@ -48,19 +48,19 @@ chapter \<open>Example: Linear Prime Sample Proof\<close>
text\<open>This example is used to demonstrate Isabelle/C/AutoCorres in a version that keeps
the theory development of the background theory as well as the program annotations completely
\<^emph>\<open>outside\<close> the C source. This particular development style that keeps the program
-separate from its theory we call CET (\<^emph>\<open>Code embedded-in Theory\<close>). It has the
+separate from its theory we call TCC (\<^emph>\<open>Theories Carrying Code\<close>). It has the
advantage that developers of development and verification teams can be separated,
as is required by many certification standards.
-Note that the opposite style that we call TEC (\<^emph>\<open>Theory embedded-in Code\<close>) is also
-supported by Isabelle/C. In TEC style, Programs become a kind of ``proof-carrying (high-level) code''.
-Exports of the C-sources will contain their theory (not only their annotations) as comments
-\<^emph>\<open>inside\<close> which might be also useful in certification as well as advanced
-``proof-carrying code'' securization schemes of server platforms.
+Note that the opposite style that we call CCT (\<^emph>\<open>Code-carrying Theories\<close>) is also
+supported by Isabelle/C. In CCT style, Programs will contain their theory
+(not only their annotations) as comments \<^emph>\<open>inside\<close> which might be also useful
+in certification as well as advanced ``proof-carrying code'' securization
+schemes of server platforms.
Of course, since developments can mix C code and HOL developments in an arbitrary manner,
these two style have to be thought of as extremes in a continuum. \<close>
-theory IsPrime_linear_CET
+theory IsPrime_linear_TCC
imports
Isabelle_C_AutoCorres.AutoCorres_Wrapper
"HOL-Computational_Algebra.Primes"
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
index e39b0249ab2..5a863d1bb1f 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
@@ -196,7 +196,7 @@ C \<open>
if (n < 2) return 0;
for (unsigned i = 2; i < SQRT_UINT_MAX && i * i <= n; i++)
- //@ definition \<comment> \<open>outer\<close> is_prime_inv where [simp]: \<open>is_prime_inv n i s \<equiv> (1 < i \<and> i \<le> n \<and> i \<le> SQRT_UINT_MAX \<and> i * i \<le> SQRT_UINT_MAX * SQRT_UINT_MAX \<and> partial_prime n i)\<close>
+ //@ definition \<comment> \<open>outer\<close> is_prime_inv where [simp]: \<open>is_prime_inv n i s \<equiv> (1 < i \<and> i \<le> n \<and> i \<le> SQRT_UINT_MAX \<and> i * i \<le> SQRT_UINT_MAX * SQRT_UINT_MAX \<and> partial_prime n i)\<close>
//@ invariant \<comment> \<open>inner\<close> \<open>is_prime_inv \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>n\<close>\<close>
//@ measure \<comment> \<open>inner\<close> \<open>\<lambda>(r, s). (Suc \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>n\<close>) * (Suc \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>n\<close>) - r * r\<close>
//@ term \<comment> \<open>outer\<close> \<open>is_prime_inv \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>n\<close> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>i\<close>\<close>
@@ -205,7 +205,7 @@ C \<open>
}
return 1;
}
- //@ install_autocorres is_prime [ ts_rules = nondet, unsigned_word_abs = is_prime ]
+ //@ install_autocorres is_prime [ts_rules=nondet, unsigned_word_abs=is_prime]
\<close>
section\<open>The Results of the AutoCorres Evaluation\<close>
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CET.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_TCC.thy
similarity index 77%
rename from C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CET.thy
rename to C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_TCC.thy
index a023ba1d093..c5e4c2126ae 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CET.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_TCC.thy
@@ -61,7 +61,7 @@ Of course, since developments can mix C code and HOL developments in an arbitrar
these two style have to be thought of as extremes in a continuum. \<close>
-theory IsPrime_sqrt_CET
+theory IsPrime_sqrt_TCC
imports
Isabelle_C_AutoCorres.AutoCorres_Wrapper
"HOL-Computational_Algebra.Primes"
@@ -245,7 +245,7 @@ section\<open>The Correctness Proof \<close>
text\<open>Note that the proof \<^emph>\<open>injects\<close> the loop invariant at the point where the proof
treats the loop.\<close>
-
+(* original NICTA proof *)
theorem (in is_prime) is_prime_faster_correct:
notes times_nat.simps(2) [simp del] mult_Suc_right [simp del]
shows "\<lbrace> \<lambda>s. n \<le> UINT_MAX \<rbrace> is_prime' n \<lbrace> \<lambda>r s. (r \<noteq> 0) \<longleftrightarrow> prime n \<rbrace>!"
@@ -280,87 +280,31 @@ lemma aux9[simp]:
-theorem (in is_prime) is_prime_correct':
- "\<lbrace> \<lambda>\<sigma>. n \<le> UINT_MAX \<rbrace> is_prime' n \<lbrace> \<lambda>res \<sigma>. (res \<noteq> 0) \<longleftrightarrow> prime n \<rbrace>!"
+theorem (in is_prime) is_prime'_correct:
+ "\<lbrace>\<lambda>\<sigma>. n \<le> UINT_MAX\<rbrace> is_prime' n \<lbrace>\<lambda>res \<sigma>.(res \<noteq> 0) \<longleftrightarrow> prime n\<rbrace>!"
proof (rule validNF_assume_pre)
- assume 1 : "n \<le> UINT_MAX"
- have 2 : "n=0 \<or> n=1 \<or> n > 1" by linarith
+ assume * : "n \<le> UINT_MAX"
+ have ** : "n=0 \<or> n=1 \<or> n > 1" by linarith
show ?thesis
- proof (insert 2, elim disjE)
- assume "n=0"
- then show ?thesis by (clarsimp simp: is_prime'_def, wp, auto)
+ proof (insert **, elim disjE)
+ assume "n = 0"
+ then show ?thesis by (clarsimp simp: is_prime'_def, wp, auto)
next
- assume "n=1"
- then show ?thesis by (clarsimp simp: is_prime'_def, wp, auto)
+ assume "n = 1"
+ then show ?thesis by (clarsimp simp: is_prime'_def, wp, auto)
next
assume "1 < n"
then show ?thesis
- apply (unfold is_prime'_def dvd_eq_mod_eq_0 [symmetric] SQRT_UINT_MAX_def [symmetric])
- text\<open>... here is the annotation with the invariant by instantiating @{thm whileLoopE_add_inv}. \<close>
- apply (subst whileLoopE_add_inv [ where I = "\<lambda>r s. is_prime_inv n r s"
- and M = "(\<lambda>(r, s). (Suc n) * (Suc n) - r * r)"])
- using 1 by (wp, auto)
+ apply(unfold is_prime'_def,fold dvd_eq_mod_eq_0 SQRT_UINT_MAX_def)
+ text\<open>... annotation with the invariant and the measure by
+ instantiating @{thm whileLoopE_add_inv}.\<close>
+ apply(subst whileLoopE_add_inv[where I = "is_prime_inv n"
+ and M ="\<lambda>(r,s).(Suc n)*(Suc n)-r*r"])
+ using * by (wp, auto)
qed
qed
-(* TODO : REMOVE HERE; WENT TO CAS *)
-section\<open>A Schematic Presentation for the Automated Proof \<close>
-(* step 0 : "lifting over parameter" over the free variables of the correctness statement: *)
-lemma whileLoopE_inv_lift1 :
- "whileLoopE (B n) (C n) = (\<lambda>x. whileLoopE_inv (B n) (C n) x (I n) (measure' (M n)))"
- by (simp add: whileLoopE_inv_def)
-
-(* step 1 : encapsulating inv and mesure for each loop *)
-definition is_prime_requires : "is_prime_requires n \<equiv> \<lambda>\<sigma>. n \<le> UINT_MAX"
-definition is_prime_ensures : "is_prime_ensures n \<equiv> \<lambda>res \<sigma>. (res \<noteq> 0) \<longleftrightarrow> prime n"
-
-definition is_prime_inv\<^sub>1 : "is_prime_inv\<^sub>1 n \<equiv> \<lambda>r s. is_prime_inv n r s"
-definition is_prime_mesure\<^sub>1 : "is_prime_mesure\<^sub>1 n \<equiv> \<lambda>(r, s). (Suc n) * (Suc n) - r * r"
-
-(* step 2 : specific replacement rule for the loop with the annotated loop *)
-lemmas whileLoopE_invL1 = whileLoopE_inv_lift1 [of _ _ _ "is_prime_inv\<^sub>1" "is_prime_mesure\<^sub>1",
- simplified is_prime_inv\<^sub>1 is_prime_mesure\<^sub>1]
-
-declare prime_ge_2_nat[dest] (* misère, preconfig pour le dernier auto. *)
-
-(* configure the general methods "preparation" and annotate loops. *)
-named_theorems prog_annotations
-declare is_prime.is_prime'_def[prog_annotations]
- is_prime_requires [prog_annotations]
- is_prime_ensures [prog_annotations]
-
-
-named_theorems folds
-declare dvd_eq_mod_eq_0[symmetric,folds]
-declare SQRT_UINT_MAX_def [symmetric,folds]
-
-method prep declares prog_annotations folds =
- (rule validNF_assume_pre, (* always!*)
- unfold prog_annotations folds)
-
-method annotate_loops for n::nat = (prep, subst whileLoopE_invL1[of _ n])
- (* this must be generalized for several loops *)
-
-
-
-(* and now the scheme for an automated proof, provided that sufficient
- background knowledge had been inserted into the prover 'auto'. *)
-
-theorem is_prime_correct'':
- "\<lbrace>\<lambda>\<sigma>. n \<le> UINT_MAX \<rbrace>
- is_prime.is_prime' n
- \<lbrace>\<lambda>res \<sigma>. (res \<noteq> 0) \<longleftrightarrow> prime n \<rbrace>!"
- apply (annotate_loops n)
- by (wp, auto )
-
-(* or also: just another presentation *)
-theorem (in is_prime) is_prime_correct''':
- "\<lbrace>is_prime_requires n\<rbrace> is_prime' n \<lbrace>is_prime_ensures n\<rbrace>!"
- apply (annotate_loops n)
- by (wp, auto )
-
-
end
--
GitLab