Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: jix/sortnetopt
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: v1
Choose a base ref
...
head repository: jix/sortnetopt
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: master
Choose a head ref
  • 4 commits
  • 6 files changed
  • 1 contributor

Commits on Nov 30, 2020

  1. Begin commenting the formal proof

    jix committed Nov 30, 2020
    Copy the full SHA
    9bfefec View commit details

Commits on Dec 1, 2020

  1. Copy the full SHA
    03429c6 View commit details

Commits on Dec 2, 2020

  1. more comments in Huffman.thy

    jix committed Dec 2, 2020
    Copy the full SHA
    43c5eee View commit details

Commits on Dec 9, 2020

  1. link paper on arxiv

    jix committed Dec 9, 2020
    Copy the full SHA
    0b5d09c View commit details
Showing with 396 additions and 155 deletions.
  1. +3 −3 README.md
  2. +27 −27 checker/verified/Checker.thy
  3. +1 −1 checker/verified/Checker_Codegen.thy
  4. +276 −42 checker/verified/Huffman.thy
  5. +65 −58 checker/verified/Sorting_Network.thy
  6. +24 −24 checker/verified/Sorting_Network_Bound.thy
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -14,9 +14,8 @@ This repository contains the following components:
* A formally verified checker for the certificates generated from search
logs, implemented using Haskell and Isabelle/HOL.

I'm currently working on a document explaining the methods used. I will add a
draft to this repository as soon as it is ready. You can also [follow me on
twitter][twitter] for updates about this.
For a full explanation see the [corresponding paper on arXiv][paper]. If you
have any questions feel free to reach out to [me on Twitter][twitter].

## Usage

@@ -105,3 +104,4 @@ formal proof is available in PDF form][document.pdf].
[zst]: https://facebook.github.io/zstd/
[document.pdf]: https://files.jix.one/sortnetopt/document.pdf
[twitter]: https://twitter.com/jix_
[paper]: https://arxiv.org/abs/2012.04400
54 changes: 27 additions & 27 deletions checker/verified/Checker.thy
Original file line number Diff line number Diff line change
@@ -211,7 +211,7 @@ qed

(***)

fun list_to_vect :: \<open>bool list \<Rightarrow> vect\<close> where
fun list_to_vect :: \<open>bool list \<Rightarrow> bseq\<close> where
\<open>list_to_vect [] i = True\<close> |
\<open>list_to_vect (x # xs) 0 = x\<close> |
\<open>list_to_vect (x # xs) (Suc i) = list_to_vect xs i\<close>
@@ -269,18 +269,18 @@ qed
definition is_unsorted_vt :: \<open>nat \<Rightarrow> vect_trie \<Rightarrow> bool\<close> where
\<open>is_unsorted_vt n A = (length_vt A > Suc n)\<close>

lemma fixed_width_vect_list_to_vect:
\<open>length xs = n \<Longrightarrow> fixed_width_vect n (list_to_vect xs)\<close>
unfolding fixed_width_vect_def list_to_vect_as_nth
lemma fixed_len_bseq_list_to_vect:
\<open>length xs = n \<Longrightarrow> fixed_len_bseq n (list_to_vect xs)\<close>
unfolding fixed_len_bseq_def list_to_vect_as_nth
by simp

lemma is_unsorted_vt_bound:
assumes \<open>set_vt A \<subseteq> {xs. length xs = n}\<close> \<open>is_unsorted_vt n A\<close>
shows \<open>pls_bound (list_to_vect ` set_vt A) 1\<close>
proof (rule unsorted_by_card_bound)
fix v assume \<open>v \<in> list_to_vect ` set_vt A\<close>
thus \<open>fixed_width_vect n v\<close>
using assms fixed_width_vect_list_to_vect
thus \<open>fixed_len_bseq n v\<close>
using assms fixed_len_bseq_list_to_vect
by blast
next
show \<open>n + 1 < card (list_to_vect ` set_vt A)\<close>
@@ -404,8 +404,8 @@ definition invert_vt :: \<open>bool \<Rightarrow> vect_trie \<Rightarrow> vect_t

lemma list_to_vect_set_vt_fixed_width:
assumes \<open>set_vt A \<subseteq> {xs. length xs = n}\<close>
shows \<open>list_to_vect ` set_vt A \<subseteq> {v. fixed_width_vect n v}\<close>
by (metis (mono_tags, lifting) Ball_Collect assms fixed_width_vect_list_to_vect image_subsetI
shows \<open>list_to_vect ` set_vt A \<subseteq> {v. fixed_len_bseq n v}\<close>
by (metis (mono_tags, lifting) Ball_Collect assms fixed_len_bseq_list_to_vect image_subsetI
mem_Collect_eq)

lemma invert_vt_bound:
@@ -731,7 +731,7 @@ proof -
show \<open>\<not>inj_on weight (list_to_vect ` set_vt A)\<close>
using is_unsorted bound_unsorted by blast
next
show \<open>\<And>v. v \<in> list_to_vect ` set_vt A \<Longrightarrow> fixed_width_vect width v\<close>
show \<open>\<And>v. v \<in> list_to_vect ` set_vt A \<Longrightarrow> fixed_len_bseq width v\<close>
by (metis (full_types) A_lengths Ball_Collect list_to_vect_set_vt_fixed_width)
next
show \<open>\<And>c. fst c < snd c \<and> snd c < width \<Longrightarrow>
@@ -787,7 +787,7 @@ lemma remove_nth_as_take_drop:
\<open>remove_nth i xs = take i xs @ drop (Suc i) xs\<close>
by (induction i xs rule: remove_nth.induct; simp)

definition prune_nth :: \<open>nat \<Rightarrow> vect \<Rightarrow> vect\<close> where
definition prune_nth :: \<open>nat \<Rightarrow> bseq \<Rightarrow> bseq\<close> where
\<open>prune_nth n v i = (if i \<ge> n then v (Suc i) else v i)\<close>

lemma list_to_vect_remove_nth:
@@ -999,10 +999,10 @@ lemma shift_channels_permutes:
unshift_shift_inverse)

lemma prune_nth_as_perm:
assumes \<open>fixed_width_vect n v\<close> \<open>v i\<close> \<open>i < n\<close>
assumes \<open>fixed_len_bseq n v\<close> \<open>v i\<close> \<open>i < n\<close>
shows \<open>prune_nth i v = apply_perm (shift_channels n i) v\<close>
unfolding prune_nth_def shift_channels_def apply_perm_def
using assms fixed_width_vect_def by auto
using assms fixed_len_bseq_def by auto

lemma inverted_prune_nth:
assumes \<open>i < Suc n\<close>
@@ -1011,11 +1011,11 @@ lemma inverted_prune_nth:
using assms by auto

lemma prune_nth_as_perm_inverted:
assumes \<open>fixed_width_vect n v\<close> \<open>\<not>v i\<close> \<open>i < n\<close>
assumes \<open>fixed_len_bseq n v\<close> \<open>\<not>v i\<close> \<open>i < n\<close>
shows
\<open>prune_nth i v = invert_vect (nat.pred n) (apply_perm (shift_channels n i) (invert_vect n v))\<close>
proof -
have \<open>fixed_width_vect n (invert_vect n v)\<close>
have \<open>fixed_len_bseq n (invert_vect n v)\<close>
by (simp add: assms(1) invert_vect_fixed_width)
moreover have \<open>(invert_vect n v) i\<close>
by (simp add: assms(2) assms(3) invert_vect_def)
@@ -1030,7 +1030,7 @@ proof -
qed

lemma prune_nth_as_perm_pol_image:
assumes \<open>\<And>v. v \<in> V \<Longrightarrow> fixed_width_vect n v\<close> \<open>\<And>v. v \<in> V \<Longrightarrow> v i = pol\<close> \<open>i < n\<close>
assumes \<open>\<And>v. v \<in> V \<Longrightarrow> fixed_len_bseq n v\<close> \<open>\<And>v. v \<in> V \<Longrightarrow> v i = pol\<close> \<open>i < n\<close>
shows
\<open>prune_nth i ` V = apply_pol (nat.pred n) pol `
apply_perm (shift_channels n i) ` apply_pol n pol ` V\<close>
@@ -1047,19 +1047,19 @@ proof -
obtain n' where n': \<open>n = Suc n'\<close>
using assms less_imp_Suc_add by blast

have f1: \<open>\<And>v. v \<in> list_to_vect ` {xs \<in> set_vt A. xs ! i \<noteq> pol} \<Longrightarrow> fixed_width_vect n v\<close>
have f1: \<open>\<And>v. v \<in> list_to_vect ` {xs \<in> set_vt A. xs ! i \<noteq> pol} \<Longrightarrow> fixed_len_bseq n v\<close>
by (metis (mono_tags) Collect_subset assms(3) image_mono in_mono
list_to_vect_set_vt_fixed_width mem_Collect_eq)

hence \<open>\<And>v.
v \<in> apply_pol n (\<not> pol) ` list_to_vect ` {xs \<in> set_vt A. xs ! i \<noteq> pol}
\<Longrightarrow> fixed_width_vect n v\<close>
\<Longrightarrow> fixed_len_bseq n v\<close>
using invert_vect_fixed_width by auto

hence \<open>\<And>v.
v \<in> apply_perm (shift_channels n i) ` apply_pol n (\<not> pol) `
list_to_vect ` {xs \<in> set_vt A. xs ! i \<noteq> pol}
\<Longrightarrow> fixed_width_vect n v\<close>
\<Longrightarrow> fixed_len_bseq n v\<close>
by (meson apply_perm_fixed_width_image assms(2) shift_channels_permutes)

moreover have \<open>\<And>v. v \<in> set_vt A \<and> v ! i \<noteq> pol \<Longrightarrow>
@@ -1077,8 +1077,8 @@ proof -
ultimately have f2: \<open>\<And>v.
v \<in> apply_perm (shift_channels n i) ` apply_pol n (\<not> pol) `
list_to_vect ` {xs \<in> set_vt A. xs ! i \<noteq> pol}
\<Longrightarrow> fixed_width_vect n' v\<close>
unfolding n' fixed_width_vect_def
\<Longrightarrow> fixed_len_bseq n' v\<close>
unfolding n' fixed_len_bseq_def
by (metis (no_types, lifting) Suc_leI le_imp_less_or_eq)


@@ -1095,7 +1095,7 @@ proof -
apply_pol n (\<not>pol) `
list_to_vect ` {xs \<in> set_vt A. xs ! i \<noteq> pol}) b\<close>
by (subst (asm) prune_nth_as_perm_pol_image[where n=n and pol=\<open>\<not>pol\<close>];
insert assms(2, 3) fixed_width_vect_list_to_vect list_to_vect_as_nth; auto simp add: n')
insert assms(2, 3) fixed_len_bseq_list_to_vect list_to_vect_as_nth; auto simp add: n')
hence
\<open>pls_bound (
apply_perm (shift_channels n i) `
@@ -1223,7 +1223,7 @@ proof -
have \<open>pls_bound (list_to_vect ` set_vt A) (sucmax.value_bound_mset (mset_ran D))\<close>
proof (rule pls_bound_from_pruned_bounds_pol[where n=width and pol=pol and B=D])
fix v assume v: \<open>v \<in> list_to_vect ` set_vt A\<close>
thus \<open>fixed_width_vect width v\<close>
thus \<open>fixed_len_bseq width v\<close>
by (metis A_lengths Ball_Collect v list_to_vect_set_vt_fixed_width)
next
show \<open>finite (dom D)\<close>
@@ -1449,24 +1449,24 @@ definition check_proof_get_bound :: \<open>proof_cert \<Rightarrow> (int \<times

lemma step_checked_bound:
assumes \<open>step_checked step\<close>
shows \<open>lower_size_bound {v. fixed_width_vect (nat (step_width step)) v} (nat (step_bound step))\<close>
shows \<open>partial_lower_size_bound {v. fixed_len_bseq (nat (step_width step)) v} (nat (step_bound step))\<close>
proof -
define A where \<open>A = list_to_vect ` set_vt (vt_list (step_vect_list step))\<close>
hence \<open>pls_bound A (nat (step_bound step))\<close>
using assms step_checked_def by auto
moreover have \<open>A \<subseteq> {v. fixed_width_vect (nat (step_width step)) v}\<close>
moreover have \<open>A \<subseteq> {v. fixed_len_bseq (nat (step_width step)) v}\<close>
by (metis (no_types, lifting) A_def Ball_Collect assms list.pred_set
list_to_vect_set_vt_fixed_width set_vt_list step_checked_def)
ultimately have
\<open>pls_bound {v. fixed_width_vect (nat (step_width step)) v} (nat (step_bound step))\<close>
\<open>pls_bound {v. fixed_len_bseq (nat (step_width step)) v} (nat (step_bound step))\<close>
using bound_mono_subset by blast
thus ?thesis
by (metis (full_types) mem_Collect_eq pls_bound_implies_lower_size_bound)
qed

lemma check_proof_get_bound_spec:
assumes \<open>check_proof_get_bound cert = Some (width, bound)\<close>
shows \<open>lower_size_bound_for_width (nat width) (nat bound)\<close>
shows \<open>lower_size_bound (nat width) (nat bound)\<close>
proof -
have checked: \<open>check_proof cert \<and> cert_length cert > 0\<close>
using assms unfolding check_proof_get_bound_def
@@ -1479,7 +1479,7 @@ proof -

thus ?thesis
by (metis Pair_inject assms check_proof_get_bound_def checked last_step_def
option.inject step_checked_bound lower_size_bound_for_width_def)
option.inject step_checked_bound lower_size_bound_def)
qed

end
2 changes: 1 addition & 1 deletion checker/verified/Checker_Codegen.thy
Original file line number Diff line number Diff line change
@@ -4,7 +4,7 @@ begin

lemma check_proof_get_bound_spec:
assumes \<open>check_proof_get_bound cert = Some (width, bound)\<close>
shows \<open>lower_size_bound_for_width (nat width) (nat bound)\<close>
shows \<open>lower_size_bound (nat width) (nat bound)\<close>
using assms by (rule Checker.check_proof_get_bound_spec)

definition nat_pred_code :: \<open>nat \<Rightarrow> nat\<close> where
Loading