From d3adae072c6e49dd0c5b855ba34c57d0be0d2beb Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Mon, 4 Feb 2019 02:30:43 +0900 Subject: [PATCH] Reduce the size of proof --- src/bitvector.lean | 3 ++ src/freevar.lean | 3 +- src/smtexpr.lean | 7 ++++ src/spec/closed.lean | 35 +++++----------- src/spec/customlemmas.lean | 53 ++++++++----------------- src/spec/freevar.lean | 81 ++++++++++---------------------------- src/spec/lemmas.lean | 2 +- src/spec/openprog.lean | 2 +- 8 files changed, 60 insertions(+), 126 deletions(-) diff --git a/src/bitvector.lean b/src/bitvector.lean index cfa9feb..778fa67 100644 --- a/src/bitvector.lean +++ b/src/bitvector.lean @@ -43,10 +43,13 @@ def of_int (sz:size) : ℤ → bitvector sz | x@(int.neg_succ_of_nat p) := ⟨(((2 ^ sz.val) - p - 1) % (2^sz.val)), ♯⟩ +@[simp] def all_one (sz:size) : bitvector sz := of_int sz (all_one_nat sz) +@[simp] def int_min (sz:size) : bitvector sz := of_int sz (int_min_nat sz) +@[simp] def zero (sz:size) : bitvector sz := of_int sz 0 def of_bool (b:bool) : bitvector (size.one) := of_int size.one (cond b 1 0) diff --git a/src/freevar.lean b/src/freevar.lean index 6d0cb51..86c07f6 100644 --- a/src/freevar.lean +++ b/src/freevar.lean @@ -108,6 +108,7 @@ namespace env def add_b (e:env) (name:string) (b:bool):env := {bv := e.bv, b := (λ n, if n = name then some b else e.b n)} + @[simp] mutual def replace_sbv, replace_sb with replace_sbv: Π (η:env) {sz:size}, sbitvec sz → sbitvec sz | η sz x@(sbitvec.var _ name) := @@ -201,8 +202,8 @@ namespace env have 0 < sbitvec.sizeof sz x, by apply sbitvec.decr_sbitvec, sbool.ult (replace_sbv η x) (replace_sbv η y) | η x := x - + @[simp, reducible] def replace_valty (η:env) (v:irsem.valty irsem_smt) := match v with | irsem.valty.ival sz i p := diff --git a/src/smtexpr.lean b/src/smtexpr.lean index 362c569..2fc2670 100644 --- a/src/smtexpr.lean +++ b/src/smtexpr.lean @@ -90,14 +90,19 @@ def of_int (sz:size) : ℤ → sbitvec sz | x@(int.neg_succ_of_nat p) := sbitvec.const sz (((2 ^ sz.val) - p - 1) % (2^sz.val)) +@[simp] def one (sz:size) : sbitvec sz := of_int sz 1 +@[simp] def zero (sz:size) : sbitvec sz := of_int sz 0 +@[simp] def intmin (sz:size) : sbitvec sz := of_int sz (int_min_nat sz) +@[simp] def intmax (sz:size) : sbitvec sz := of_int sz (int.of_nat ((2^(sz.val-1))-1)) +@[simp] def uintmax (sz:size) : sbitvec sz := of_int sz (all_one_nat sz) def of_bool (b:sbool) : sbitvec (size.one) := @@ -127,9 +132,11 @@ end variable {sz:size} +@[simp] def mk_zext (m:size) (a:sbitvec sz): sbitvec (sz.add m) := sbitvec.zext (sz.add m) a +@[simp] def mk_sext (m:size) (a:sbitvec sz): sbitvec (sz.add m) := sbitvec.sext (sz.add m) a diff --git a/src/spec/closed.lean b/src/spec/closed.lean index c97aac9..34f93d7 100644 --- a/src/spec/closed.lean +++ b/src/spec/closed.lean @@ -63,7 +63,6 @@ lemma closed_b_never_var: ∀ s, ¬ closed_b (sbool.var s) unfold env.add_b at H', unfold freevar.env.replace_sb at H', simp at H', - unfold env.replace_sb._match_1 at H', cases H' end @@ -76,7 +75,6 @@ lemma closed_bv_never_var: ∀ sz s, ¬ closed_bv (sbitvec.var sz s) unfold env.add_bv at H', unfold freevar.env.replace_sbv at H', simp at H', - unfold env.replace_sbv._match_1 at H', cases H' end @@ -169,7 +167,6 @@ lemma closed_b_var_add2: ∀ (η:freevar.env) (v:bool) (s:string), simp, intros, generalize Hb': (η.b s) = b', - unfold env.replace_sb._match_1 at *, unfold closed_b, intros, cases v, refl, refl end @@ -204,14 +201,13 @@ lemma closed_bv_var_add2: ∀ (η:freevar.env) sz v (s:string), closed_bv ((η.add_bv s v)⟦sbitvec.var sz s⟧) := begin unfold env.add_bv, - unfold freevar.env.replace_sbv, - simp, intros, generalize Hb': (η.b s) = b', - unfold env.replace_sbv._match_1 at *, unfold closed_bv, - intros, cases v; unfold sbitvec.of_int; - unfold freevar.env.replace_sbv + intros, cases v; + unfold freevar.env.replace_sbv; simp, + { unfold sbitvec.of_int, unfold env.replace_sbv }, + { unfold sbitvec.of_int, unfold env.replace_sbv }, end lemma ival_closed: ∀ sz vn pn (η:freevar.env) z b, @@ -224,18 +220,12 @@ lemma ival_closed: ∀ sz vn pn (η:freevar.env) z b, unfold env.add_b, unfold env.add_bv, simp, - unfold freevar.env.replace_valty, - unfold freevar.env.replace_sb, - unfold freevar.env.replace_sbv, - simp, split, { - unfold env.replace_sbv._match_1, cases z; unfold sbitvec.of_int; unfold freevar.env.replace_sbv }, { - unfold env.replace_sb._match_1, rw env.replace_sb_of_bool } end @@ -289,17 +279,8 @@ lemma closed_regfile_update_split: ∀ {rf:regfile irsem_smt} {n} {v}, unfold regfile.apply_to_values at *, simp at HC, split, - { - intros, - have HC := HC η, - injection HC - }, - { - intros, - have HC := HC η, - injection HC, - injection h_1 - } + { intros, have HC := HC η, injection HC }, + { intros, have HC := HC η, injection HC, injection h_1 } }, { intros HC η, @@ -307,11 +288,13 @@ lemma closed_regfile_update_split: ∀ {rf:regfile irsem_smt} {n} {v}, have HC1 := HC1 η, have HC2 := HC2 η, unfold regfile.apply_to_values at *, - simp, + simp at *, rw HC1, rw HC2 } end + + -- TODO 1: Merge closed_b_add_b and closed_bv_add_b into a single -- theorem (I tried merging them -- but it raised excessive memory consumption error.) diff --git a/src/spec/customlemmas.lean b/src/spec/customlemmas.lean index 27daaee..2b731fa 100644 --- a/src/spec/customlemmas.lean +++ b/src/spec/customlemmas.lean @@ -34,6 +34,9 @@ def is_poison: irsem.valty irsem_exec → Prop set_option eqn_compiler.zeta true set_option pp.proofs true +local attribute [simp] option.bind irsem.step irsem.step_bop + irsem.bop irsem.bop_ub irsem.irstate.updateub irsem.irstate.updatereg + lemma never_poison: ∀ isz name op1 op2 st st' val (HSTEP:step st (udiv isz name op1 op2) = some st') @@ -47,53 +50,31 @@ lemma never_poison: injection HNOUB, clear HNOUB, cases op2, simp at *, { - unfold irsem.step at HSTEP, cases (irsem.get_value irsem_exec (ub, regs) op1 (ty.int isz)) with val1; unfold has_bind.bind at *; unfold option.bind at *, injection HSTEP, - rw ← HVAL at HSTEP, unfold option.bind at HSTEP, - unfold irsem.step_bop at HSTEP, + rw ← HVAL at HSTEP, simp at HSTEP, cases val1 with isz1 ii1 ip1, cases val with isz2 ii2 ip2, + simp at HSTEP, have HISZDEC:decidable (isz1 = isz2), apply_instance, - cases HISZDEC; - unfold irsem.step_bop._match_1 at HSTEP; - unfold irsem.bop at HSTEP; - unfold irsem.step_bop._match_2 at HSTEP; - unfold irsem.bop_val at HSTEP, - { rw dif_neg at HSTEP, injection HSTEP - }, - { - rw (dif_pos HISZDEC) at HSTEP, + cases HISZDEC; unfold irsem.bop_val at HSTEP, + { rw dif_neg at HSTEP, injection HSTEP }, + { rw (dif_pos HISZDEC) at HSTEP, injection HSTEP with HSTEP', clear HSTEP, - generalize HH: - (irsem.bop_ub irsem_exec isz1 bopcode.udiv ii1 ip1 (cast (by rw HISZDEC) ii2) ip2) - = eub, - rw HH at HSTEP', - unfold irsem.irstate.updateub at HSTEP', - unfold irsem.irstate.updatereg at HSTEP', - simp at HSTEP', injection HSTEP' with HUB HREG, - cases eub, cases ub; injection HUB, - -- now let's unfold irsem.bop_ub. - unfold irsem.bop_ub at HH, - have HDIV: bop_isdiv bopcode.udiv = tt, by simp, - rw (if_pos HDIV) at HH, - simp at *, - cases ip2, - { -- if dividend was poison.. - unfold_coes at HH, unfold has_and.and at HH, - unfold bool_like.and at HH, simp at HH, exfalso, exact HH - }, - { - simp - } + cases ub; cases ip2, + any_goals { + -- if dividend was poison or previous state was ub.. + unfold_coes at HSTEP', unfold has_and.and at HSTEP', + unfold bool_like.and at HSTEP', simp at HSTEP', injection HSTEP' with HH _, + injection HH }, + { simp } } }, { - simp at HVAL, unfold irsem.get_value at HVAL, + simp at HVAL, cases op2, - dunfold irsem.get_value._match_1 at HVAL, - dunfold irsem.get_value._match_2 at HVAL, + unfold irsem.get_value at HVAL, have HSZDEC1: decidable (0 < isz), apply_instance, cases HSZDEC1, { rw (dif_neg HSZDEC1) at HVAL, injection HVAL }, diff --git a/src/spec/freevar.lean b/src/spec/freevar.lean index c2e293e..864a7b1 100644 --- a/src/spec/freevar.lean +++ b/src/spec/freevar.lean @@ -460,11 +460,10 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧ intros, unfold freevar.env.replace_sb, unfold freevar.env.empty, - simp, - unfold freevar.env.replace_sb._match_1 + simp, done }, any_goals { - intros b H, unfold freevar.env.replace_sb, rw H, done + intros b H, unfold freevar.env.replace_sb, rw H }, any_goals { intros b1 b2 H1 H2, unfold freevar.env.replace_sb, rw [H1, H2], done @@ -486,8 +485,7 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧ intros, unfold freevar.env.replace_sbv, unfold freevar.env.empty, - simp, - unfold freevar.env.replace_sbv._match_1 + simp, done }, any_goals { intros sz v' sz' H, @@ -505,6 +503,7 @@ lemma env.empty_replace: (∀ (b:sbool), freevar.env.empty⟦b⟧ = b) ∧ } end + lemma env.empty_replace_sb: ∀ (b:sbool), freevar.env.empty⟦b⟧ = b := begin apply (and.elim_left env.empty_replace) @@ -530,18 +529,7 @@ lemma env.replace_sb_overflowchk_add: ∀ sbitvec.overflow_chk @sbitvec.add sz2 nsw (η⟦v1⟧) (η⟦v2⟧) := begin intros, unfold sbitvec.overflow_chk, - cases nsw; simp; unfold freevar.env.replace_sb, - { - rw env.replace_sbv_extract, - rw env.replace_sbv_add, - repeat { rw env.replace_sbv_mk_zext }, - unfold sbitvec.zero, rw env.replace_sbv_of_int - }, - { - rw env.replace_sbv_add, - repeat { rw env.replace_sbv_mk_sext }, - rw env.replace_sbv_add - } + cases nsw; simp, rw env.replace_sbv_of_int end lemma env.replace_sb_overflowchk_sub: ∀ @@ -550,18 +538,7 @@ lemma env.replace_sb_overflowchk_sub: ∀ sbitvec.overflow_chk @sbitvec.sub sz2 nsw (η⟦v1⟧) (η⟦v2⟧) := begin intros, unfold sbitvec.overflow_chk, - cases nsw; simp; unfold freevar.env.replace_sb, - { - rw env.replace_sbv_extract, - rw env.replace_sbv_sub, - repeat { rw env.replace_sbv_mk_zext }, - unfold sbitvec.zero, rw env.replace_sbv_of_int - }, - { - rw env.replace_sbv_sub, - repeat { rw env.replace_sbv_mk_sext }, - rw env.replace_sbv_sub - } + cases nsw; simp, rw env.replace_sbv_of_int end lemma env.replace_sb_overflowchk_mul: ∀ @@ -570,18 +547,7 @@ lemma env.replace_sb_overflowchk_mul: ∀ sbitvec.overflow_chk @sbitvec.mul sz2 nsw (η⟦v1⟧) (η⟦v2⟧) := begin intros, unfold sbitvec.overflow_chk, - cases nsw; simp; unfold freevar.env.replace_sb, - { - rw env.replace_sbv_extract, - rw env.replace_sbv_mul, - repeat { rw env.replace_sbv_mk_zext }, - unfold sbitvec.zero, rw env.replace_sbv_of_int - }, - { - rw env.replace_sbv_mul, - repeat { rw env.replace_sbv_mk_sext }, - rw env.replace_sbv_mul - } + cases nsw; simp, rw env.replace_sbv_of_int end lemma env.replace_sb_overflowchk_shl: ∀ @@ -591,20 +557,9 @@ lemma env.replace_sb_overflowchk_shl: ∀ := begin intros, unfold sbitvec.shl_overflow_chk, unfold sbitvec.overflow_chk, - cases nsw; simp; unfold freevar.env.replace_sb, - { - rw env.replace_sbv_extract, - rw env.replace_sbv_shl, - repeat { rw env.replace_sbv_mk_zext }, - unfold sbitvec.zero, rw env.replace_sbv_of_int, - rw env.replace_sbv_urem, rw env.replace_sbv_of_int - }, - { - rw env.replace_sbv_shl, - repeat { rw env.replace_sbv_mk_sext }, - rw env.replace_sbv_shl, - rw env.replace_sbv_urem, rw env.replace_sbv_of_int - } + cases nsw; simp, + { repeat { rw env.replace_sbv_of_int }, tauto }, + { rw env.replace_sbv_of_int, tauto } end -- irstate @@ -925,7 +880,7 @@ lemma env.add_b_replace_match: ∀ (η:freevar.env) n b, intros, unfold freevar.env.replace_sb, unfold freevar.env.add_b, - simp, unfold freevar.env.replace_sb._match_1 + simp end lemma env.add_bv_replace_match: ∀ (η:freevar.env) n z sz, @@ -934,7 +889,7 @@ lemma env.add_bv_replace_match: ∀ (η:freevar.env) n z sz, intros, unfold freevar.env.replace_sbv, unfold freevar.env.add_bv, - simp, unfold freevar.env.replace_sbv._match_1 + simp end lemma env.add_bv_replace_sb: ∀ (η:freevar.env) n n' z, @@ -1297,8 +1252,10 @@ lemma env.not_in_add_bv_irstate_comm: ∀ (η:freevar.env) (ss:irstate irsem_smt rw ss_snd_ih, cases ss_snd_hd with rn v, cases v with sz iv pv, - rw env.not_in_add_bv_valty_comm, - assumption + simp, + rw env.not_in_add_bv_bv_comm, + rw env.not_in_add_bv_b_comm, + assumption, assumption } } end @@ -1332,8 +1289,10 @@ lemma env.not_in_add_b_irstate_comm: ∀ (η:freevar.env) (ss:irstate irsem_smt) rw ss_snd_ih, cases ss_snd_hd with rn v, cases v with sz iv pv, - rw env.not_in_add_b_valty_comm, - assumption + simp, + rw env.not_in_add_b_bv_comm, + rw env.not_in_add_b_b_comm, + assumption, assumption } } end diff --git a/src/spec/lemmas.lean b/src/spec/lemmas.lean index e6637fb..3d8beec 100644 --- a/src/spec/lemmas.lean +++ b/src/spec/lemmas.lean @@ -185,7 +185,7 @@ lemma bvequiv_urem: ∀ (sz:size) (sb:sbitvec sz) eb intros, apply bv_equiv.urem, assumption, apply bvequiv_from_z, { cases sz, unfold_coes, simp, unfold uint_like.from_z, unfold bitvector.ne, - unfold bitvector.zero, unfold bitvector.of_int, simp, + unfold bitvector.of_int, simp, intros H, injection H, simp at h_1, rw nat.mod_pow2 at h_1, rw h_1 at sz_property, cases sz_property }, diff --git a/src/spec/openprog.lean b/src/spec/openprog.lean index 01232d1..a9cd90e 100644 --- a/src/spec/openprog.lean +++ b/src/spec/openprog.lean @@ -561,8 +561,8 @@ lemma step_replace: ∀ (ss:irstate_smt) (i:instruction) have HOPCOND' := apply_some HOPCOND, cases HOPCOND' with vopcond' HOPCOND', rw HOPCOND', - rw get_value_replace, unfold option.bind, + rw get_value_replace, cases vop1, { rw apply_none at HOP1, rw HOP1, unfold option.bind },