1 2open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_equal"; 3val _ = ParseExtras.temp_loose_equality() 4open lisp_sexpTheory lisp_invTheory; 5 6(* --- *) 7 8open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 9open combinTheory finite_mapTheory addressTheory helperLib; 10open set_sepTheory bitTheory fcpTheory stringTheory; 11 12open codegenLib decompilerLib prog_x64Lib; 13open lisp_consTheory stop_and_copyTheory; 14 15infix \\ 16val op \\ = op THEN; 17val RW = REWRITE_RULE; 18val RW1 = ONCE_REWRITE_RULE; 19fun SUBGOAL q = REVERSE (sg q) 20 21 22 23(* equality test - main loop 24 25 r8 - sexp1 26 r9 - sexp2 27 r15 - base pointer for "other" heap half 28 r0 - index pointer for "other" heap half 29 30*) 31 32val (thm,mc_equal_def) = basic_decompile_strings x64_tools "mc_equal" 33 (SOME (``(r8:word64,r9:word64,r0:word64,r15:word64,r6:word64,df:word64 set,f:word64->word32)``, 34 ``(r0:word64,r6:word64,df:word64 set,f:word64->word32)``)) 35 (assemble "x64" ` 36START: cmp r8,r9 37 je NEXT 38 test r8,1 39 jne FALSE 40 test r9,1 41 jne FALSE 42 mov r8,[r6+4*r8] 43 mov r9,[r6+4*r9] 44 mov [r15+8*r0],r8d 45 mov [r15+8*r0+4],r9d 46 shr r8,32 47 shr r9,32 48 inc r0 49 jmp START 50NEXT: cmp r0,0 51 je TRUE 52 dec r0 53 mov r8d,[r15+8*r0] 54 mov r9d,[r15+8*r0+4] 55 jmp START 56TRUE: mov r0d,11 57 jmp EXIT 58FALSE: mov r0d,3 59EXIT:`) 60 61(* equality test *) 62 63val (thm,mc_full_equal_def) = decompile_io_strings x64_tools "mc_full_equal" 64 (SOME (``(r6:word64,r7:word64,r8:word64,r9:word64,df:word64 set,f:word64->word32)``, 65 ``(r0:word64,r6:word64,r7:word64,r8:word64,r9:word64,r15:word64,df:word64 set,f:word64->word32)``)) 66 (assemble "x64" ` 67 mov r15,[r7-232] 68 xor r0,r0 69 insert mc_equal 70 mov r15,[r7-240] 71 mov r8,r0 72 mov r0d,3 73 mov r9,r0 74 add r15,r15 75 `); 76 77val mc_full_equal_spec = thm; 78val _ = save_thm("mc_full_equal_spec",thm); 79 80val LISP = lisp_inv_def |> SPEC_ALL |> concl |> dest_eq |> fst; 81val REST = LISP |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 82val STAT = LISP |> car |> car |> cdr; 83val VAR_REST = LISP |> car |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 84 85val lisp_equal_stack_def = Define ` 86 (lisp_equal_stack [] xx yy zz = T) /\ 87 (lisp_equal_stack ((w0,x0,w1,x1)::ys) ^STAT (x2,x3,x4,x5,^VAR_REST) (w2,w3,w4,w5,df,f,^REST) = 88 LDEPTH x0 + LENGTH ys <= e /\ LDEPTH x1 + LENGTH ys <= e /\ 89 lisp_inv ^STAT (x0,x1,x2,x3,x4,x5,^VAR_REST) (w0,w1,w2,w3,w4,w5,df,f,^REST) /\ 90 lisp_equal_stack ys ^STAT (x2,x3,x4,x5,^VAR_REST) (w2,w3,w4,w5,df,f,^REST))`; 91 92val one_eq_stack_def = Define ` 93 (one_eq_stack bp [] = emp) /\ 94 (one_eq_stack bp ((w0,x0,w1,x1)::ys) = 95 one (bp + n2w (8 * LENGTH ys), w0) * 96 one (bp + n2w (8 * LENGTH ys + 4), w1) * 97 one_eq_stack bp ys)`; 98 99val lisp_eq_measure_def = Define ` 100 (lisp_eq_measure [] = 0) /\ 101 (lisp_eq_measure ((w0:word32,x0,w1:word32,x1)::ys) = 3*LSIZE x0 + 3*LSIZE x1 + lisp_eq_measure ys)`; 102 103val w2w_lemma = prove( 104 ``!w v. ((w2w w = (w2w v):word64) = (w = v:word32)) /\ 105 ((w2w w && 1w = 0w:word64) = (w && 1w = 0w)) /\ 106 ((31 -- 0) (w2w w) = (w2w w):word64) /\ 107 ((w2w w << 32 !! w2w v) >>> 32 = (w2w w):word64) /\ 108 (w2w (w2w w << 32 !! (w2w v):word64) = v)``, 109 blastLib.BBLAST_TAC); 110 111val RANGE_TAC = FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC 112 113val ref_mem_REFL = prove( 114 ``ref_mem a m n n = emp``, 115 Cases_on `n` \\ ASM_SIMP_TAC std_ss [ref_mem_def]); 116 117val lisp_equal_stack_ignore1 = prove( 118 ``!ys. 119 lisp_equal_stack ys ^STAT (x2,x3,x4,x5,^VAR_REST) 120 (w2,w3,w4,w5,df,f,^REST) /\ RANGE (0,e) j ==> 121 lisp_equal_stack ys ^STAT (x2,x3,x4,x5,^VAR_REST) 122 (w2,w3,w4,w5,df,(n2w (8 * j) + bp2 =+ w) f,^REST)``, 123 Induct \\ SIMP_TAC std_ss [lisp_equal_stack_def] 124 \\ Cases \\ Cases_on `r` \\ Cases_on `r'` 125 \\ ASM_SIMP_TAC std_ss [lisp_equal_stack_def] \\ REPEAT STRIP_TAC 126 \\ IMP_RES_TAC (SIMP_RULE std_ss [LET_DEF] lisp_inv_ignore_write1) 127 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]); 128 129val lisp_equal_stack_ignore2 = prove( 130 ``!ys. 131 lisp_equal_stack ys ^STAT (x2,x3,x4,x5,^VAR_REST) 132 (w2,w3,w4,w5,df,f,^REST) /\ RANGE (0,e) j ==> 133 lisp_equal_stack ys ^STAT (x2,x3,x4,x5,^VAR_REST) 134 (w2,w3,w4,w5,df,(n2w (8 * j) + bp2 + 4w =+ w) f,^REST)``, 135 Induct \\ SIMP_TAC std_ss [lisp_equal_stack_def] 136 \\ Cases \\ Cases_on `r` \\ Cases_on `r'` 137 \\ ASM_SIMP_TAC std_ss [lisp_equal_stack_def] \\ REPEAT STRIP_TAC 138 \\ IMP_RES_TAC (SIMP_RULE std_ss [LET_DEF] lisp_inv_ignore_write2) 139 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]); 140 141val addr_lemma = prove( 142 ``((w2w (w && 3w) = 0w:word32) = (w && 3w = 0w:word64)) /\ 143 (((w + 4w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 144 (((w - 0x34w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 145 (((w - 0x38w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 146 (((w - 0x3Cw) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 147 (((w - 0x40w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 148 (((w - 0xE8w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 149 (((w - 0xE4w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 150 (((w - 0xECw) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 151 (((w - 0xF0w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 152 (((w + 8w * x) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 153 (((4w * x + w) && 3w = 0w) = (w && 3w = 0w:word64)) /\ 154 (((8w * x + w) && 3w = 0w) = (w && 3w = 0w:word64))``, 155 blastLib.BBLAST_TAC); 156 157val lisp_inv_Sym_NIL = 158 lisp_inv_Sym |> CONJUNCTS |> hd |> UNDISCH |> CONJUNCT1 |> DISCH_ALL 159 160val lisp_inv_Sym_T = 161 lisp_inv_Sym |> CONJUNCTS |> el 2 |> UNDISCH |> CONJUNCT1 |> DISCH_ALL 162 163val mc_equal_lemma = prove( 164 ``!ys w0 x0 w1 x1 f. 165 lisp_equal_stack ((w0,x0,w1,x1)::ys) ^STAT 166 (x2,x3,x4,x5,^VAR_REST) (w2,w3,w4,w5,df,f,^REST) /\ 167 LENGTH ys <= e /\ 168 (one_eq_stack bp2 ys * ref_mem bp2 (\x. H_EMP) (LENGTH ys) e * p) (fun2set (f,df)) ==> 169 ?fi. mc_equal_pre(w2w w0,w2w w1,n2w (LENGTH ys),bp2,bp,df,f) /\ 170 (mc_equal(w2w w0,w2w w1,n2w (LENGTH ys),bp2,bp,df,f) = 171 (if (x0 = x1) /\ EVERY (\(w0,x0,w1,x1). x0 = x1) ys then 11w else 3w,bp,df,fi)) /\ 172 lisp_inv ^STAT (Sym "NIL",Sym "NIL",x2,x3,x4,x5,^VAR_REST) 173 (3w,3w,w2,w3,w4,w5,df,fi,^REST)``, 174 NTAC 5 STRIP_TAC 175 \\ completeInduct_on `lisp_eq_measure ((w0,x0,w1,x1)::ys) + LENGTH ys` 176 \\ REPEAT STRIP_TAC \\ ONCE_REWRITE_TAC [mc_equal_def] 177 \\ ASM_SIMP_TAC std_ss [w2w_lemma] 178 \\ Cases_on `w0 = w1` \\ ASM_SIMP_TAC std_ss [w2w_lemma] THEN1 179 (`LENGTH ys < 18446744073709551616` by 180 (FULL_SIMP_TAC std_ss [lisp_equal_stack_def,lisp_inv_def] \\ DECIDE_TAC) 181 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LENGTH_NIL] 182 \\ Cases_on `ys = []` \\ ASM_SIMP_TAC std_ss [] THEN1 183 (FULL_SIMP_TAC std_ss [LET_DEF,EVERY_DEF] 184 \\ FULL_SIMP_TAC std_ss [lisp_equal_stack_def] 185 \\ IMP_RES_TAC (SIMP_RULE std_ss [] lisp_inv_eq_lucky) 186 \\ ASM_SIMP_TAC std_ss [] 187 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_Sym_NIL) 188 \\ Q.LIST_EXISTS_TAC [`x1`,`w1`] 189 \\ MATCH_MP_TAC lisp_inv_swap1 190 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_Sym_NIL) 191 \\ Q.LIST_EXISTS_TAC [`x0`,`w0`] 192 \\ FULL_SIMP_TAC std_ss []) 193 \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [] 194 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 195 \\ FULL_SIMP_TAC std_ss [lisp_equal_stack_def] 196 \\ `?w0n x0n w1n x1n. h = (w0n,x0n,w1n,x1n)` by METIS_TAC [PAIR] 197 \\ FULL_SIMP_TAC std_ss [] 198 \\ Q.PAT_X_ASSUM `!m.bbb` (MP_TAC o Q.SPEC `lisp_eq_measure ((w0n,x0n,w1n,x1n)::t) + (LENGTH t)`) 199 \\ MATCH_MP_TAC (METIS_PROVE [] ``b1 /\ (b2 ==> b3) ==> ((b1 ==> b2) ==> b3)``) 200 \\ STRIP_TAC THEN1 (SIMP_TAC std_ss [lisp_eq_measure_def,ADD_ASSOC] \\ DECIDE_TAC) 201 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPECL [`w0n`,`x0n`,`w1n`,`x1n`,`t`]) 202 \\ ASM_SIMP_TAC std_ss [] \\ `LENGTH t <= e` by DECIDE_TAC 203 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPECL [`f`]) 204 \\ FULL_SIMP_TAC std_ss [lisp_equal_stack_def] 205 \\ MATCH_MP_TAC (METIS_PROVE [] ``b1 /\ (b2 ==> b3) ==> ((b1 ==> b2) ==> b3)``) 206 \\ STRIP_TAC THEN1 207 (FULL_SIMP_TAC std_ss [one_eq_stack_def] 208 \\ `RANGE(LENGTH t,e)(LENGTH t)` by RANGE_TAC 209 \\ IMP_RES_TAC ref_mem_RANGE 210 \\ FULL_SIMP_TAC std_ss [ref_aux_def,SEP_CLAUSES,SEP_EXISTS_THM,STAR_ASSOC,ref_mem_REFL] 211 \\ Q.LIST_EXISTS_TAC [`w0n`,`w1n`] 212 \\ FULL_SIMP_TAC (std_ss++star_ss) [ADD1,word_arith_lemma1]) 213 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [LET_DEF] 214 \\ FULL_SIMP_TAC std_ss [one_eq_stack_def,word_mul_n2w,AC ADD_COMM ADD_ASSOC, 215 AC WORD_ADD_COMM WORD_ADD_ASSOC,word_add_n2w,EVERY_DEF] 216 \\ SEP_R_TAC \\ IMP_RES_TAC lisp_inv_eq_lucky 217 \\ FULL_SIMP_TAC std_ss [] 218 \\ FULL_SIMP_TAC std_ss [addr_lemma,GSYM word_add_n2w,GSYM word_mul_n2w,WORD_ADD_ASSOC] 219 \\ FULL_SIMP_TAC std_ss [lisp_inv_def]) 220 \\ REVERSE (Cases_on `isDot x0`) THEN1 221 (FULL_SIMP_TAC std_ss [lisp_equal_stack_def] 222 \\ `~(w0 && 0x1w = 0x0w)` by METIS_TAC [lisp_inv_type] 223 \\ `~(x0 = x1)` by METIS_TAC [lisp_inv_eq] 224 \\ ASM_SIMP_TAC std_ss [LET_DEF] 225 \\ METIS_TAC [lisp_inv_Sym_T,lisp_inv_Sym_NIL,lisp_inv_swap1]) 226 \\ REVERSE (Cases_on `isDot x1`) THEN1 227 (FULL_SIMP_TAC std_ss [lisp_equal_stack_def] 228 \\ `~(w1 && 0x1w = 0x0w)` by METIS_TAC [lisp_inv_type,lisp_inv_swap1] 229 \\ `~(x0 = x1)` by METIS_TAC [lisp_inv_eq] 230 \\ ASM_SIMP_TAC std_ss [LET_DEF] 231 \\ METIS_TAC [lisp_inv_Sym_T,lisp_inv_Sym_NIL,lisp_inv_swap1]) 232 \\ `(w0 && 0x1w = 0x0w) /\ (w1 && 0x1w = 0x0w)` by 233 (FULL_SIMP_TAC std_ss [lisp_equal_stack_def] 234 \\ METIS_TAC [lisp_inv_type,lisp_inv_swap1]) 235 \\ ASM_SIMP_TAC std_ss [] 236 \\ FULL_SIMP_TAC std_ss [lisp_equal_stack_def] 237 \\ Q.ABBREV_TAC `w04 = f (0x4w * w2w w0 + bp + 0x4w)` 238 \\ Q.ABBREV_TAC `w00 = f (0x4w * w2w w0 + bp)` 239 \\ Q.ABBREV_TAC `w14 = f (0x4w * w2w w1 + bp + 0x4w)` 240 \\ Q.ABBREV_TAC `w10 = f (0x4w * w2w w1 + bp)` 241 \\ `f (bp + 0x4w * w2w w1 + 0x4w) = w14` by FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 242 \\ `f (bp + 0x4w * w2w w0 + 0x4w) = w04` by FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 243 \\ `f (bp + 0x4w * w2w w1) = w10` by FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 244 \\ `f (bp + 0x4w * w2w w0) = w00` by FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 245 \\ FULL_SIMP_TAC std_ss [LET_DEF,word_mul_n2w,w2w_lemma] 246 \\ `lisp_equal_stack ((w00,CAR x0,w10,CAR x1)::ys) ^STAT (x2,x3,x4,x5,^VAR_REST) 247 (w2,w3,w4,w5,df,f,^REST)` by 248 (FULL_SIMP_TAC std_ss [lisp_equal_stack_def,CONJ_ASSOC] 249 \\ STRIP_TAC THEN1 250 (FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,LDEPTH_def,MAX_DEF] 251 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,LDEPTH_def,MAX_DEF] 252 \\ DECIDE_TAC) 253 \\ IMP_RES_TAC lisp_inv_car \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 254 \\ IMP_RES_TAC lisp_inv_swap1 255 \\ IMP_RES_TAC lisp_inv_car \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 256 \\ IMP_RES_TAC lisp_inv_swap1 \\ METIS_TAC []) 257 \\ `lisp_equal_stack ((w04,CDR x0,w14,CDR x1)::(w00,CAR x0,w10,CAR x1)::ys) ^STAT (x2,x3,x4,x5,^VAR_REST) 258 (w2,w3,w4,w5,df,f,^REST)` by 259 (ONCE_REWRITE_TAC [lisp_equal_stack_def] \\ ASM_SIMP_TAC std_ss [] 260 \\ FULL_SIMP_TAC std_ss [lisp_equal_stack_def,CONJ_ASSOC] 261 \\ STRIP_TAC THEN1 262 (FULL_SIMP_TAC std_ss [isDot_thm,CDR_def,LDEPTH_def,MAX_DEF,LENGTH] 263 \\ FULL_SIMP_TAC std_ss [isDot_thm,CDR_def,LDEPTH_def,MAX_DEF] 264 \\ DECIDE_TAC) 265 \\ IMP_RES_TAC lisp_inv_cdr \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 266 \\ IMP_RES_TAC lisp_inv_swap1 267 \\ IMP_RES_TAC lisp_inv_cdr \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 268 \\ IMP_RES_TAC lisp_inv_swap1 \\ METIS_TAC []) 269 \\ Q.ABBREV_TAC `fj = (n2w (8 * LENGTH ys) + bp2 + 0x4w =+ w10) 270 ((n2w (8 * LENGTH ys) + bp2 =+ w00) f)` 271 \\ FULL_SIMP_TAC std_ss [GSYM lisp_equal_stack_def] 272 \\ Q.PAT_X_ASSUM `!m.bbb` (MP_TAC o Q.SPEC `lisp_eq_measure ((w04,CDR x0,w14,CDR x1)::(w00,CAR x0,w10,CAR x1)::ys) + LENGTH ((w00,CAR x0,w10,CAR x1)::ys)`) 273 \\ MATCH_MP_TAC (METIS_PROVE [] ``b1 /\ (b2 ==> b3) ==> ((b1 ==> b2) ==> b3)``) 274 \\ STRIP_TAC THEN1 275 (FULL_SIMP_TAC std_ss [isDot_thm] 276 \\ SIMP_TAC std_ss [lisp_eq_measure_def,LENGTH,CAR_def,CDR_def,LSIZE_def] 277 \\ DECIDE_TAC) 278 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPECL [`w04`,`CDR x0`,`w14`,`CDR x1`,`(w00,CAR x0,w10,CAR x1)::ys`]) 279 \\ ASM_SIMP_TAC std_ss [] 280 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPEC `fj`) 281 \\ MATCH_MP_TAC (METIS_PROVE [] ``b1 /\ (b2 ==> b3) ==> ((b1 ==> b2) ==> b3)``) 282 \\ STRIP_TAC THEN1 283 (SIMP_TAC std_ss [LENGTH,one_eq_stack_def] 284 \\ `SUC (LENGTH ys) <= e` by 285 (FULL_SIMP_TAC std_ss [isDot_thm] \\ FULL_SIMP_TAC std_ss [LDEPTH_def,MAX_DEF] 286 \\ DECIDE_TAC) \\ ASM_SIMP_TAC std_ss [] 287 \\ REVERSE (REPEAT STRIP_TAC) THEN1 288 (`RANGE(LENGTH ys,e)(LENGTH ys)` by RANGE_TAC 289 \\ IMP_RES_TAC ref_mem_RANGE 290 \\ FULL_SIMP_TAC std_ss [ref_mem_REFL,SEP_CLAUSES,STAR_ASSOC,ref_aux_def,SEP_EXISTS_THM] 291 \\ Q.UNABBREV_TAC `fj` 292 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,GSYM word_add_n2w] 293 \\ SEP_WRITE_TAC) 294 \\ Q.UNABBREV_TAC `fj` \\ `RANGE(0,e)(LENGTH ys)` by RANGE_TAC 295 \\ MATCH_MP_TAC lisp_equal_stack_ignore2 \\ ASM_SIMP_TAC std_ss [] 296 \\ MATCH_MP_TAC lisp_equal_stack_ignore1 \\ ASM_SIMP_TAC std_ss []) 297 \\ SIMP_TAC std_ss [LENGTH,word_add_n2w,EVERY_DEF,ADD1] 298 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 299 \\ FULL_SIMP_TAC std_ss [isDot_thm,CDR_def,CAR_def,SExp_11,AC CONJ_ASSOC CONJ_COMM] 300 \\ FULL_SIMP_TAC std_ss [addr_lemma,INSERT_SUBSET,EMPTY_SUBSET,GSYM word_mul_n2w] 301 \\ `(bp && 0x3w = 0x0w) /\ (bp2 && 0x3w = 0x0w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 302 \\ ASM_SIMP_TAC std_ss [] 303 \\ `RANGE(0,e)(LENGTH ys)` by 304 (SIMP_TAC std_ss [LENGTH,one_eq_stack_def] 305 \\ FULL_SIMP_TAC std_ss [isDot_thm] \\ FULL_SIMP_TAC std_ss [LDEPTH_def,MAX_DEF] 306 \\ RANGE_TAC) 307 \\ IMP_RES_TAC lisp_inv_ignore_write1 308 \\ IMP_RES_TAC lisp_inv_ignore_write2 309 \\ REPEAT (Q.PAT_X_ASSUM `!x.bbb` (K ALL_TAC)) 310 \\ IMP_RES_TAC (RW [isDot_def] (Q.INST [`x0`|->`Dot a b`] lisp_inv_car)) 311 \\ IMP_RES_TAC (RW [isDot_def] (Q.INST [`x0`|->`Dot a b`] lisp_inv_cdr)) 312 \\ IMP_RES_TAC lisp_inv_swap1 313 \\ IMP_RES_TAC (RW [isDot_def] (Q.INST [`x0`|->`Dot a b`] lisp_inv_car)) 314 \\ IMP_RES_TAC (RW [isDot_def] (Q.INST [`x0`|->`Dot a b`] lisp_inv_cdr)) 315 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,word_mul_n2w]); 316 317val mc_equal_thm = mc_equal_lemma 318 |> Q.SPECL [`[]`,`w0`,`x0`,`w1`,`x1`,`f`] 319 |> SIMP_RULE std_ss [EVERY_DEF,LENGTH,lisp_equal_stack_def,one_eq_stack_def,SEP_CLAUSES] 320 321val mc_full_equal_thm = store_thm("mc_full_equal_thm", 322 ``lisp_inv ^STAT (x0,x1,x2,x3,x4,x5,^VAR_REST) 323 (w0,w1,w2,w3,w4,w5,df,f,^REST) ==> 324 ?fi w0i w1i. 325 mc_full_equal_pre (bp,sp,w2w w0,w2w w1,df,f) /\ 326 (mc_full_equal (bp,sp,w2w w0,w2w w1,df,f) = (tw0,bp,sp,w2w w0i,w2w w1i,we,df,fi)) /\ 327 lisp_inv ^STAT (LISP_TEST (x0 = x1),Sym "NIL",x2,x3,x4,x5,^VAR_REST) 328 (w0i,w1i,w2,w3,w4,w5,df,fi,^REST)``, 329 SIMP_TAC std_ss [mc_full_equal_def] \\ STRIP_TAC 330 \\ `?p. (ref_mem bp2 (\x. H_EMP) 0 e * p) (fun2set (f,df))` by 331 (FULL_SIMP_TAC std_ss [lisp_inv_def] \\ METIS_TAC [STAR_ASSOC,STAR_COMM]) 332 \\ MP_TAC mc_equal_thm \\ ASM_SIMP_TAC std_ss [] 333 \\ `LDEPTH x0 <= e /\ LDEPTH x1 <= e` by METIS_TAC [lisp_inv_LDEPTH,lisp_inv_swap1] 334 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 335 \\ ASM_SIMP_TAC std_ss [LET_DEF] 336 \\ `w2w (f (sp - 0xE4w)) << 32 !! w2w (f (sp - 0xE8w)) = bp2` by 337 (FULL_SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,ref_static_def,APPEND] 338 \\ FULL_SIMP_TAC std_ss [LET_DEF,word64_3232_def,word_arith_lemma3,STAR_ASSOC,SEP_CLAUSES] 339 \\ SEP_R_TAC \\ blastLib.BBLAST_TAC) 340 \\ ASM_SIMP_TAC std_ss [] 341 \\ Q.LIST_EXISTS_TAC [`if x0 = x1 then 0xBw else 0x3w`,`3w`] 342 \\ `(w2w (fi (sp - 0xECw)) << 32 !! w2w (fi (sp - 0xF0w)) = (n2w e):word64)` by 343 (FULL_SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,ref_static_def,APPEND] 344 \\ FULL_SIMP_TAC std_ss [LET_DEF,word64_3232_def,word_arith_lemma3,STAR_ASSOC] 345 \\ SEP_R_TAC \\ Q.SPEC_TAC (`(n2w e):word64`,`ww`) \\ blastLib.BBLAST_TAC) 346 \\ ASM_SIMP_TAC std_ss [] 347 \\ `n2w e + n2w e = we` by 348 FULL_SIMP_TAC std_ss [lisp_inv_def,word_add_n2w,DECIDE ``2*e=e+e:num``] 349 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 350 \\ FULL_SIMP_TAC std_ss [addr_lemma] 351 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 352 \\ ASM_SIMP_TAC std_ss [] 353 \\ `(sp - 0xE4w IN df /\ sp - 0xE8w IN df) /\ 354 (sp - 0xECw IN df /\ sp - 0xF0w IN df)` by 355 (FULL_SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,ref_static_def, 356 LET_DEF,word64_3232_def,word_arith_lemma3,STAR_ASSOC,APPEND] \\ SEP_R_TAC 357 \\ ASM_SIMP_TAC std_ss []) \\ ASM_SIMP_TAC std_ss [] 358 \\ `tw0 = 3w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 359 \\ Cases_on `x0 = x1` \\ ASM_SIMP_TAC std_ss [LISP_TEST_def] 360 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 361 \\ IMP_RES_TAC lisp_inv_Sym_T); 362 363 364val _ = export_theory(); 365