1open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_inv"; 2val _ = ParseExtras.temp_loose_equality() 3 4 5open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 6open combinTheory finite_mapTheory addressTheory helperLib; 7open set_sepTheory bitTheory fcpTheory; 8 9open lisp_sexpTheory lisp_consTheory stop_and_copyTheory lisp_bytecodeTheory; 10 11 12infix \\ 13val op \\ = op THEN; 14val RW = REWRITE_RULE; 15val RW1 = ONCE_REWRITE_RULE; 16fun SUBGOAL q = REVERSE (sg q) 17val wstd_ss = std_ss ++ SIZES_ss ++ rewrites [DECIDE ``n<256 ==> (n:num)<18446744073709551616``,stringTheory.ORD_BOUND]; 18 19 20(* I/O definition *) 21 22val _ = Hol_datatype ` 23 io_streams = IO_STREAMS of string (* input *) => string (* output *)`; 24 25val io_streams_11 = fetch "-" "io_streams_11" 26 27(* symbol table definition *) 28 29val one_byte_list_def = Define ` 30 (one_byte_list a [] = emp) /\ 31 (one_byte_list a (x::xs) = one (a:word64,x:word8) * one_byte_list (a + 1w) xs)`; 32 33val one_byte_list_APPEND = store_thm("one_byte_list_APPEND", 34 ``!a xs ys. 35 one_byte_list a (xs++ys) = one_byte_list a xs * one_byte_list (a + n2w (LENGTH xs)) ys``, 36 Induct_on `xs` \\ ASM_SIMP_TAC std_ss [one_byte_list_def,APPEND,SEP_CLAUSES, 37 LENGTH,WORD_ADD_0,word_arith_lemma1,ADD1,AC ADD_COMM ADD_ASSOC] 38 \\ SIMP_TAC (std_ss++star_ss) []); 39 40val string_data_def = Define ` 41 string_data str = n2w (LENGTH str + 1) :: MAP ((n2w:num->word8) o ORD) str`; 42 43val symbol_list_def = Define ` 44 (symbol_list [] = [0w]) /\ 45 (symbol_list (str::xs) = string_data str ++ symbol_list xs)`; 46 47val one_symbol_list_def = Define ` 48 one_symbol_list a xs k = 49 SEP_EXISTS ys. 50 one_byte_list a (symbol_list xs ++ ys) * 51 cond (EVERY (\x. LENGTH x < 255) xs /\ (LENGTH (symbol_list xs ++ ys) = k) /\ 52 ALL_DISTINCT xs /\ 520 <= LENGTH ys /\ 53 LENGTH xs < 536870912)`; 54 55val symtable_inv_def = Define ` 56 symtable_inv (sa1:word64,sa2:word64,sa3:word64,dg,g) xs = 57 (one_symbol_list sa1 xs (w2n sa3 - w2n sa1)) (fun2set (g,dg)) /\ 58 (sa2 = sa1 + n2w (LENGTH (symbol_list xs)))`; 59 60 61(* top-level stack declaration *) 62 63val ref_stack_space_above_def = Define ` 64 (ref_stack_space_above sp 0 = emp) /\ 65 (ref_stack_space_above sp (SUC n) = 66 ref_stack_space_above (sp + 4w) n * SEP_EXISTS w. one (sp + 4w:word64,w:word32))`; 67 68val ref_full_stack_def = Define ` 69 ref_full_stack sp wsp xs xs_rest ys n_rest = 70 ref_stack (sp + 4w * wsp) (xs ++ xs_rest) * 71 ref_stack_space (sp + 4w * wsp) (w2n wsp + 6) * 72 ref_static (sp - 256w) ys * 73 ref_stack_space_above (sp + 4w * wsp + n2w (4 * LENGTH (xs ++ xs_rest))) n_rest`; 74 75(* definition of code heap *) 76 77val IMMEDIATE32_def = Define ` 78 IMMEDIATE32 (w:word32) = 79 [w2w w; w2w (w >>> 8); w2w (w >>> 16); w2w (w >>> 24)]:word8 list`; 80 81val bc_ref_def = Define ` 82 (bc_ref (i,sym) iPOP = 83 [0x44w; 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 0xC3w]) /\ 84 (bc_ref (i,sym) (iCONST_NUM n) = 85 [0x48w; 0x85w; 0xDBw; 0x3Ew; 0x48w; 0x75w; 0x9w; 0x8Bw; 0xD1w; 0x48w; 86 0xFFw; 0xA7w; 0x38w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xCBw; 0x44w; 87 0x89w; 0x4w; 0x9Fw; 0x41w; 0xB8w] ++ 88 IMMEDIATE32 (n2w (4 * n + 1))) /\ 89 (bc_ref (i,sym) (iCONST_SYM s) = 90 [0x48w; 0x85w; 0xDBw; 0x3Ew; 0x48w; 0x75w; 0x9w; 0x8Bw; 0xD1w; 0x48w; 91 0xFFw; 0xA7w; 0x38w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xCBw; 0x44w; 92 0x89w; 0x4w; 0x9Fw; 0x41w; 0xB8w] ++ 93 IMMEDIATE32 (n2w (8 * THE (LIST_FIND 0 s sym) + 3))) /\ 94 (bc_ref (i,sym) iRETURN = 95 [0x48w; 0xC3w]) /\ 96 (bc_ref (i,sym) (iPOPS n) = 97 [0x48w; 0x81w; 0xC3w] ++ IMMEDIATE32 (n2w n)) /\ 98 (bc_ref (i,sym) (iLOAD pos) = 99 [0x48w; 0x85w; 0xDBw; 0x3Ew; 0x48w; 0x75w; 0x9w; 0x8Bw; 0xD1w; 0x48w; 100 0xFFw; 0xA7w; 0x38w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xCBw; 0x44w; 101 0x89w; 0x4w; 0x9Fw; 0x44w; 0x8Bw; 0x84w; 0x9Fw] ++ IMMEDIATE32 (n2w (4 * pos))) /\ 102 (bc_ref (i,sym) (iSTORE pos) = 103 [0x44w; 0x89w; 0x84w; 0x9Fw] ++ IMMEDIATE32 (n2w (4 * pos)) ++ 104 [0x44w; 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 0xC3w]) /\ 105 (bc_ref (i,sym) iCOMPILE = 106 [0x48w; 0x8Bw; 0x57w; 0x88w; 0x48w; 0xFFw; 0xD2w]) /\ 107 (bc_ref (i,sym) iFAIL = 108 [0xBAw; 0x4w; 0x0w; 0x0w; 0x0w; 0x48w; 0xFFw; 0xA7w; 0x38w; 0xFFw; 109 0xFFw; 0xFFw]) /\ 110 (bc_ref (i,sym) iPRINT = 111 [0x48w; 0x8Bw; 0x97w; 0x78w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 112 0xD2w; 0x48w; 0x8Bw; 0x8Fw; 0x40w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 113 0x8Bw; 0x87w; 0x28w; 0xFFw; 0xFFw; 0xFFw; 0xC6w; 0x0w; 0xAw; 114 0xC6w; 0x40w; 0x1w; 0x0w; 0x48w; 0xFFw; 0xD1w; 0xB8w; 0x3w; 115 0x0w; 0x0w; 0x0w; 0xB9w; 0x1w; 0x0w; 0x0w; 0x0w]) /\ 116 (bc_ref (i,sym) (iJUMP pos) = 117 [0x48w; 0xE9w] ++ IMMEDIATE32 (n2w pos - n2w i - 6w)) /\ 118 (bc_ref (i,sym) (iCALL pos) = 119 [0x48w; 0xE8w] ++ IMMEDIATE32 (n2w pos - n2w i - 6w)) /\ 120 (bc_ref (i,sym) (iJNIL pos) = 121 [0x4Dw; 0x8Bw; 0xC8w; 0x44w; 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 0xC3w; 122 0x49w; 0x83w; 0xF9w; 0x3w; 0x48w; 0x0Fw; 0x84w] ++ IMMEDIATE32 (n2w pos - n2w i - 21w)) /\ 123 (bc_ref (i,sym) (iDATA opCAR) = 124 [0x49w; 0xF7w; 0xC0w; 0x1w; 0x0w; 0x0w; 0x0w; 0x4Cw; 0xFw; 0x45w; 125 0xC0w; 0x48w; 0x75w; 0x4w; 0x46w; 0x8Bw; 0x4w; 0x86w]) /\ 126 (bc_ref (i,sym) (iDATA opCDR) = 127 [0x49w; 0xF7w; 0xC0w; 0x1w; 0x0w; 0x0w; 0x0w; 0x4Cw; 0xFw; 0x45w; 128 0xC0w; 0x48w; 0x75w; 0x5w; 0x46w; 0x8Bw; 0x44w; 0x86w; 0x4w]) /\ 129 (bc_ref (i,sym) (iDATA opCONSP) = 130 [0x49w; 0xF7w; 0xC0w; 0x1w; 0x0w; 0x0w; 0x0w; 0xBAw; 0xBw; 0x0w; 131 0x0w; 0x0w; 0x4Cw; 0xFw; 0x44w; 0xC2w; 0x44w; 0xFw; 0x45w; 0xC0w]) /\ 132 (bc_ref (i,sym) (iDATA opNATP) = 133 [0x49w; 0x8Bw; 0xD0w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 0xD1w; 134 0xBAw; 0xBw; 0x0w; 0x0w; 0x0w; 0x4Cw; 0xFw; 0x44w; 0xC2w; 0x44w; 135 0xFw; 0x45w; 0xC0w]) /\ 136 (bc_ref (i,sym) (iDATA opSYMBOLP) = 137 [0x49w; 0x8Bw; 0xD0w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 0xD0w; 138 0xBAw; 0xBw; 0x0w; 0x0w; 0x0w; 0x4Cw; 0xFw; 0x44w; 0xC2w; 0x44w; 139 0xFw; 0x45w; 0xC0w]) /\ 140 (bc_ref (i,sym) (iDATA opADD) = 141 [0x44w; 0x8Bw; 0xCw; 0x9Fw; 0x48w; 0xFFw; 0xC3w; 0x49w; 0x8Bw; 142 0xD0w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 0xD1w; 0x44w; 0xFw; 143 0x45w; 0xC1w; 0x49w; 0x8Bw; 0xD1w; 0x48w; 0x21w; 0xC2w; 0x48w; 144 0x39w; 0xD1w; 0x44w; 0xFw; 0x45w; 0xC9w; 0x41w; 0xFFw; 0xC8w; 145 0x45w; 0x1w; 0xC8w; 0x48w; 0x73w; 0xFw; 0x4Cw; 0x8Bw; 0xC1w; 0xBAw; 146 0x2w; 0x0w; 0x0w; 0x0w; 0x48w; 0xFFw; 0xA7w; 0x38w; 0xFFw; 0xFFw; 147 0xFFw]) /\ 148 (bc_ref (i,sym) (iDATA opCONS) = 149 [0x4Dw; 0x87w; 0xC8w; 0x44w; 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 150 0xC3w; 0x4Dw; 0x39w; 0xFEw; 0x3Ew; 0x48w; 0x75w; 0xAw; 0x48w; 151 0x8Bw; 0x97w; 0x68w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xD2w; 152 0x46w; 0x89w; 0x4Cw; 0xB6w; 0x4w; 0x46w; 0x89w; 0x4w; 0xB6w; 153 0x45w; 0x8Bw; 0xC6w; 0x49w; 0x83w; 0xC6w; 0x2w]) /\ 154 (bc_ref (i,sym) (iDATA opLESS) = 155 [0x4Dw; 0x87w; 0xC8w; 0x44w; 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 156 0xC3w; 0x49w; 0x8Bw; 0xD0w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 157 0xD1w; 0x44w; 0xFw; 0x45w; 0xC1w; 0x49w; 0x8Bw; 0xD1w; 0x48w; 158 0x21w; 0xC2w; 0x48w; 0x39w; 0xD1w; 0x44w; 0xFw; 0x45w; 0xC9w; 159 0x4Dw; 0x39w; 0xC8w; 0xBAw; 0xBw; 0x0w; 0x0w; 0x0w; 0x4Cw; 0xFw; 160 0x42w; 0xC2w; 0x44w; 0xFw; 0x43w; 0xC0w]) /\ 161 (bc_ref (i,sym) (iDATA opSUB) = 162 [0x4Dw; 0x87w; 0xC8w; 0x44w; 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 163 0xC3w; 0x49w; 0x8Bw; 0xD0w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 164 0xD1w; 0x44w; 0xFw; 0x45w; 0xC1w; 0x49w; 0x8Bw; 0xD1w; 0x48w; 165 0x21w; 0xC2w; 0x48w; 0x39w; 0xD1w; 0x44w; 0xFw; 0x45w; 0xC9w; 166 0x41w; 0xFFw; 0xC0w; 0x45w; 0x29w; 0xC8w; 0x44w; 0xFw; 0x42w; 167 0xC1w]) /\ 168 (bc_ref (i,sym) (iDATA opSYMBOL_LESS) = 169 [0x4Dw; 0x87w; 0xC8w; 0x44w; 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 170 0xC3w; 0x49w; 0x8Bw; 0xD0w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 171 0xD0w; 0x44w; 0xFw; 0x45w; 0xC0w; 0x49w; 0x8Bw; 0xD1w; 0x48w; 172 0x21w; 0xC2w; 0x48w; 0x39w; 0xD0w; 0x44w; 0xFw; 0x45w; 0xC8w; 173 0x4Cw; 0x8Bw; 0x9Fw; 0x20w; 0xFFw; 0xFFw; 0xFFw; 0x49w; 0xC1w; 174 0xE8w; 0x3w; 0x4Dw; 0x8Bw; 0xD0w; 0x4Dw; 0x85w; 0xD2w; 0x48w; 175 0x74w; 0xDw; 0x49w; 0xFw; 0xB6w; 0x3w; 0x49w; 0x1w; 0xC3w; 0x49w; 176 0xFFw; 0xCAw; 0x48w; 0xEBw; 0xEDw; 0x4Dw; 0x8Bw; 0xC3w; 0x49w; 177 0xC1w; 0xE9w; 0x3w; 0x4Dw; 0x8Bw; 0xD1w; 0x4Cw; 0x8Bw; 0x9Fw; 178 0x20w; 0xFFw; 0xFFw; 0xFFw; 0x4Dw; 0x85w; 0xD2w; 0x48w; 0x74w; 179 0xDw; 0x49w; 0xFw; 0xB6w; 0x3w; 0x49w; 0x1w; 0xC3w; 0x49w; 0xFFw; 180 0xCAw; 0x48w; 0xEBw; 0xEDw; 0x4Dw; 0x8Bw; 0xCBw; 0x4Dw; 0xFw; 181 0xB6w; 0x10w; 0x4Dw; 0xFw; 0xB6w; 0x19w; 0x49w; 0xFFw; 0xCAw; 182 0x49w; 0xFFw; 0xCBw; 0x49w; 0xFFw; 0xC0w; 0x49w; 0xFFw; 0xC1w; 183 0x49w; 0x83w; 0xFBw; 0x0w; 0x48w; 0x74w; 0x23w; 0x49w; 0x83w; 184 0xFAw; 0x0w; 0x48w; 0x74w; 0x24w; 0x49w; 0xFw; 0xB6w; 0x0w; 0x41w; 185 0x3Aw; 0x1w; 0x48w; 0x72w; 0x1Aw; 0x48w; 0x77w; 0xFw; 0x49w; 0xFFw; 186 0xC0w; 0x49w; 0xFFw; 0xC1w; 0x49w; 0xFFw; 0xCAw; 0x49w; 0xFFw; 187 0xCBw; 0x48w; 0xEBw; 0xD6w; 0xB8w; 0x3w; 0x0w; 0x0w; 0x0w; 0x48w; 188 0xEBw; 0x5w; 0xB8w; 0xBw; 0x0w; 0x0w; 0x0w; 0x4Cw; 0x8Bw; 0xC0w; 189 0xB8w; 0x3w; 0x0w; 0x0w; 0x0w; 0x4Cw; 0x8Bw; 0xC8w; 0x4Cw; 0x8Bw; 190 0xD0w; 0x4Cw; 0x8Bw; 0xD8w]) /\ 191 (bc_ref (i,sym) (iDATA opEQUAL) = 192 [0x44w; 0x8Bw; 0xCw; 0x9Fw; 0x48w; 0xFFw; 0xC3w; 0x48w; 0x8Bw; 193 0x97w; 0x70w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xD2w]) /\ 194 (bc_ref (i,sym) (iCONST_LOOKUP) = 195 [0x48w; 0x8Bw; 0x57w; 0xC0w; 0x46w; 0x8Bw; 0x4w; 0x2w]) /\ 196 (bc_ref (i,sym) iJUMP_SYM = 197 [0x46w; 0x8Bw; 0x4Cw; 0xAEw; 0x4w; 0x4Dw; 0x8Bw; 0xD0w; 0x44w; 198 0x8Bw; 0x1Cw; 0x9Fw; 0x48w; 0xFFw; 0xC3w; 0x49w; 0xF7w; 0xC1w; 199 0x1w; 0x0w; 0x0w; 0x0w; 0x48w; 0x75w; 0x30w; 0x46w; 0x8Bw; 0x4w; 200 0x8Ew; 0x46w; 0x8Bw; 0x4Cw; 0x8Ew; 0x4w; 0x4Dw; 0x39w; 0xD0w; 201 0x48w; 0x74w; 0x8w; 0x46w; 0x8Bw; 0x4Cw; 0x8Ew; 0x4w; 0x48w; 202 0xEBw; 0xDFw; 0x46w; 0x8Bw; 0xCw; 0x8Ew; 0x46w; 0x8Bw; 0x44w; 203 0x8Ew; 0x4w; 0x46w; 0x8Bw; 0xCw; 0x8Ew; 0x4Dw; 0x39w; 0xD8w; 204 0x48w; 0x74w; 0x6w; 0x41w; 0xB9w; 0x3w; 0x0w; 0x0w; 0x0w; 0x44w; 205 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 0xC3w; 0x4Dw; 0x8Bw; 0xD1w; 206 0x49w; 0x8Bw; 0xD1w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 0xD1w; 207 0x48w; 0x74w; 0x3Bw; 0x4Dw; 0x8Bw; 0xC2w; 0x48w; 0x8Bw; 0x97w; 208 0x78w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xD2w; 0x48w; 0x8Bw; 209 0x8Fw; 0x40w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0x8Bw; 0x87w; 0x28w; 210 0xFFw; 0xFFw; 0xFFw; 0xC6w; 0x0w; 0xAw; 0xC6w; 0x40w; 0x1w; 211 0x0w; 0x48w; 0xFFw; 0xD1w; 0xB8w; 0x3w; 0x0w; 0x0w; 0x0w; 0xB9w; 212 0x1w; 0x0w; 0x0w; 0x0w; 0xBAw; 0xBw; 0x0w; 0x0w; 0x0w; 0x48w; 213 0xFFw; 0xA7w; 0x38w; 0xFFw; 0xFFw; 0xFFw; 0x49w; 0x8Bw; 0xD2w; 214 0x48w; 0xC1w; 0xEAw; 0x2w; 0x48w; 0x3w; 0x97w; 0x60w; 0xFFw; 215 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xE2w]) /\ 216 (bc_ref (i,sym) iCALL_SYM = 217 [0x46w; 0x8Bw; 0x4Cw; 0xAEw; 0x4w; 0x4Dw; 0x8Bw; 0xD0w; 0x44w; 218 0x8Bw; 0x1Cw; 0x9Fw; 0x48w; 0xFFw; 0xC3w; 0x49w; 0xF7w; 0xC1w; 219 0x1w; 0x0w; 0x0w; 0x0w; 0x48w; 0x75w; 0x30w; 0x46w; 0x8Bw; 0x4w; 220 0x8Ew; 0x46w; 0x8Bw; 0x4Cw; 0x8Ew; 0x4w; 0x4Dw; 0x39w; 0xD0w; 221 0x48w; 0x74w; 0x8w; 0x46w; 0x8Bw; 0x4Cw; 0x8Ew; 0x4w; 0x48w; 222 0xEBw; 0xDFw; 0x46w; 0x8Bw; 0xCw; 0x8Ew; 0x46w; 0x8Bw; 0x44w; 223 0x8Ew; 0x4w; 0x46w; 0x8Bw; 0xCw; 0x8Ew; 0x4Dw; 0x39w; 0xD8w; 224 0x48w; 0x74w; 0x6w; 0x41w; 0xB9w; 0x3w; 0x0w; 0x0w; 0x0w; 0x44w; 225 0x8Bw; 0x4w; 0x9Fw; 0x48w; 0xFFw; 0xC3w; 0x4Dw; 0x8Bw; 0xD1w; 226 0x49w; 0x8Bw; 0xD1w; 0x48w; 0x21w; 0xC2w; 0x48w; 0x39w; 0xD1w; 227 0x48w; 0x74w; 0x3Bw; 0x4Dw; 0x8Bw; 0xC2w; 0x48w; 0x8Bw; 0x97w; 228 0x78w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xD2w; 0x48w; 0x8Bw; 229 0x8Fw; 0x40w; 0xFFw; 0xFFw; 0xFFw; 0x48w; 0x8Bw; 0x87w; 0x28w; 230 0xFFw; 0xFFw; 0xFFw; 0xC6w; 0x0w; 0xAw; 0xC6w; 0x40w; 0x1w; 231 0x0w; 0x48w; 0xFFw; 0xD1w; 0xB8w; 0x3w; 0x0w; 0x0w; 0x0w; 0xB9w; 232 0x1w; 0x0w; 0x0w; 0x0w; 0xBAw; 0xBw; 0x0w; 0x0w; 0x0w; 0x48w; 233 0xFFw; 0xA7w; 0x38w; 0xFFw; 0xFFw; 0xFFw; 0x49w; 0x8Bw; 0xD2w; 234 0x48w; 0xC1w; 0xEAw; 0x2w; 0x48w; 0x3w; 0x97w; 0x60w; 0xFFw; 235 0xFFw; 0xFFw; 0x48w; 0xFFw; 0xD2w])`; 236 237val bc_length_def = Define ` 238 bc_length x = LENGTH (bc_ref (0,[]) x)`; 239 240val bs2bytes_def = Define ` 241 (bs2bytes (i,sym) [] = []) /\ 242 (bs2bytes (i,sym) (x::xs) = bc_ref (i,sym) x ++ bs2bytes (i+bc_length x,sym) xs)`; 243 244val _ = Hol_datatype ` 245 code_type = BC_CODE of (num -> bc_inst_type option) # num`; 246 247val WRITE_CODE_def = Define ` 248 (WRITE_CODE (BC_CODE (code,ptr)) [] = BC_CODE (code,ptr)) /\ 249 (WRITE_CODE (BC_CODE (code,ptr)) (c::cs) = 250 WRITE_CODE (BC_CODE ((ptr =+ SOME c) code,ptr+bc_length c)) cs)`; 251 252val bc_symbols_ok_def = Define ` 253 (bc_symbols_ok sym [] = T) /\ 254 (bc_symbols_ok sym (iCONST_NUM i::xs) = i < 2**30 /\ bc_symbols_ok sym xs) /\ 255 (bc_symbols_ok sym (iCONST_SYM s::xs) = MEM s sym /\ bc_symbols_ok sym xs) /\ 256 (bc_symbols_ok sym (iJUMP i::xs) = i < 2**30 /\ bc_symbols_ok sym xs) /\ 257 (bc_symbols_ok sym (iJNIL i::xs) = i < 2**30 /\ bc_symbols_ok sym xs) /\ 258 (bc_symbols_ok sym (iCALL i::xs) = i < 2**30 /\ bc_symbols_ok sym xs) /\ 259 (bc_symbols_ok sym (iSTORE i::xs) = i < 2**29 /\ bc_symbols_ok sym xs) /\ 260 (bc_symbols_ok sym (iLOAD i::xs) = i < 2**29 /\ bc_symbols_ok sym xs) /\ 261 (bc_symbols_ok sym (iPOPS i::xs) = i < 2**30 /\ bc_symbols_ok sym xs) /\ 262 (bc_symbols_ok sym (_::xs) = bc_symbols_ok sym xs)`; 263 264val code_ptr_def = Define `code_ptr (BC_CODE (_,p)) = p`; 265val code_mem_def = Define `code_mem (BC_CODE (m,_)) = m`; 266 267val code_heap_def = Define ` 268 code_heap code (sym,base_ptr,curr_ptr,space_left,dh,h) = 269 ?bs hs. 270 (WRITE_CODE (BC_CODE ((\x. NONE),0)) bs = code) /\ 271 (curr_ptr = base_ptr + n2w (code_ptr code)) /\ 272 (one_byte_list base_ptr (bs2bytes (0,sym) bs ++ hs)) (fun2set (h,dh)) /\ 273 code_ptr code + w2n space_left < 2**30 /\ (LENGTH hs = w2n (space_left:word64)) /\ 274 bc_symbols_ok sym bs`; 275 276 277(* definition of main invariant *) 278 279val INIT_SYMBOLS_def = Define ` 280 INIT_SYMBOLS = ["NIL";"T";"QUOTE";"CONS";"CAR";"CDR";"EQUAL";"<";"SYMBOL-<"; 281 "+";"-";"ATOMP";"CONSP";"NATP";"SYMBOLP";"DEFINE";"IF"; 282 "LAMBDA";"FUNCALL";"ERROR";"PRINT";"LET";"LET*";"COND";"OR"; 283 "AND";"FIRST";"SECOND";"THIRD";"FOURTH";"FIFTH";"LIST";"DEFUN"]`; 284 285val IS_TRUE_def = Define `IS_TRUE ok = (ok = T)`; 286 287val lisp_inv_def = Define ` 288 lisp_inv (* pointers and bounds that are constant throughout execution *) 289 (a1,a2,sl,sl1,e,ex,cs,ok) 290 (* high-level data that is held in the heap *) 291 (x0,x1,x2,x3,x4,x5,xs,xs1,io:io_streams,xbp:num,qs:word64 list,code,amnt) 292 (* implementation level equivalents *) 293 (w0,w1,w2,w3,w4,w5,df,f,dg,g,bp,bp2,wsp,wi:word64,we:word64,tw0:word64,tw1:word64,tw2:word64,sp,ds,sa1,sa2,sa3,dd,d) = 294 ?s0 s1 s2 s3 s4 s5 m i ss ss1 sym b. 295 (LENGTH xs = LENGTH ss) /\ (LENGTH xs1 = LENGTH ss1) /\ 296 (LENGTH ss + w2n wsp = sl) /\ IS_TRUE ok /\ 297 (wi = n2w (2 * i)) /\ (we = n2w (2 * e)) /\ (tw0 = 3w) /\ (tw1 = 1w) /\ 298 ok_split_heap ([s0;s1;s2;s3;s4;s5]++ss++ss1,m,i,e) /\ i <= e /\ e < 2147483648 /\ 299 EVERY (lisp_x (m,INIT_SYMBOLS++sym)) 300 ((s0,x0)::(s1,x1)::(s2,x2)::(s3,x3)::(s4,x4)::(s5,x5)::ZIP(ss++ss1,xs++xs1)) /\ 301 (MAP ref_heap_addr [s0;s1;s2;s3;s4;s5] = [w0;w1;w2;w3;w4;w5]) /\ 302 ((bp,bp2) = if b then (a1,a2) else (a2,a1)) /\ sl < 2**64 /\ sl1 < 2**30 /\ 303 (LENGTH cs = 10) /\ (LENGTH ds = 10) /\ (amnt < 2**30) /\ 304 (bp && 0x3w = 0x0w) /\ (bp2 && 0x3w = 0x0w) /\ (sp && 0x3w = 0x0w) /\ 305 (EL 1 ds = sp + n2w (4 * sl) - n2w (4 * xbp) - 1w) /\ xbp <= sl /\ 306 (EL 6 ds = sp + n2w (4 * sl) - 1w) /\ 307 (EL 7 ds = n2w (sl1 - LENGTH ss1)) /\ LENGTH ss1 <= sl1 /\ 308 (EL 8 ds = n2w (LENGTH ss1)) /\ (w2n (EL 5 ds) <= e) /\ 309 (n2w amnt = EL 9 ds) /\ 310 (ref_mem bp m 0 e * ref_mem bp2 (\x.H_EMP) 0 e * 311 ref_full_stack sp wsp ss ss1 312 ([a1;a2;n2w e;bp2;sa1;sa2;sa3;ex] ++ cs ++ ds) (sl1 - LENGTH ss1)) (fun2set (f,df)) /\ 313 symtable_inv (sa1:word64,sa2:word64,sa3:word64,dg,g) (INIT_SYMBOLS++sym) /\ 314 code_heap code (INIT_SYMBOLS++sym,EL 4 cs,EL 2 ds,EL 3 ds,dd,d)`; 315 316val LISP = lisp_inv_def |> SPEC_ALL |> concl |> dest_eq |> fst 317 318(* swap *) 319 320val w2n_lt30 = SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a``|->``:30``] w2n_lt) 321val w2n_lt29 = SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a``|->``:29``] w2n_lt) 322 323val SWAP_TAC = 324 Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 325 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 326 \\ FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 327 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 328 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 329 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 330 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []; 331 332val lisp_inv_swap0 = METIS_PROVE [] ``^LISP ==> ^LISP``; 333 334val lisp_inv_swap1 = prove( 335 ``^LISP ==> 336 let (x0,x1) = (x1,x0) in 337 let (w0,w1) = (w1,w0) in ^LISP``, 338 SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 339 \\ Q.LIST_EXISTS_TAC [`s1`,`s0`,`s2`,`s3`,`s4`,`s5`] \\ SWAP_TAC) 340 |> SIMP_RULE std_ss [LET_DEF]; 341 342val lisp_inv_swap2 = prove( 343 ``^LISP ==> 344 let (x0,x2) = (x2,x0) in 345 let (w0,w2) = (w2,w0) in ^LISP``, 346 SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 347 \\ Q.LIST_EXISTS_TAC [`s2`,`s1`,`s0`,`s3`,`s4`,`s5`] \\ SWAP_TAC) 348 |> SIMP_RULE std_ss [LET_DEF]; 349 350val lisp_inv_swap3 = prove( 351 ``^LISP ==> 352 let (x0,x3) = (x3,x0) in 353 let (w0,w3) = (w3,w0) in ^LISP``, 354 SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 355 \\ Q.LIST_EXISTS_TAC [`s3`,`s1`,`s2`,`s0`,`s4`,`s5`] \\ SWAP_TAC) 356 |> SIMP_RULE std_ss [LET_DEF]; 357 358val lisp_inv_swap4 = prove( 359 ``^LISP ==> 360 let (x0,x4) = (x4,x0) in 361 let (w0,w4) = (w4,w0) in ^LISP``, 362 SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 363 \\ Q.LIST_EXISTS_TAC [`s4`,`s1`,`s2`,`s3`,`s0`,`s5`] \\ SWAP_TAC) 364 |> SIMP_RULE std_ss [LET_DEF]; 365 366val lisp_inv_swap5 = prove( 367 ``^LISP ==> 368 let (x0,x5) = (x5,x0) in 369 let (w0,w5) = (w5,w0) in ^LISP``, 370 SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 371 \\ Q.LIST_EXISTS_TAC [`s5`,`s1`,`s2`,`s3`,`s4`,`s0`] \\ SWAP_TAC) 372 |> SIMP_RULE std_ss [LET_DEF]; 373 374val _ = save_thm("lisp_inv_swap0",lisp_inv_swap0); 375val _ = save_thm("lisp_inv_swap1",lisp_inv_swap1); 376val _ = save_thm("lisp_inv_swap2",lisp_inv_swap2); 377val _ = save_thm("lisp_inv_swap3",lisp_inv_swap3); 378val _ = save_thm("lisp_inv_swap4",lisp_inv_swap4); 379val _ = save_thm("lisp_inv_swap5",lisp_inv_swap5); 380 381 382(* copy *) 383 384val lisp_inv_copy = prove( 385 ``^LISP ==> let (x1,w1) = (x0,w0) in ^LISP``, 386 SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 387 \\ Q.LIST_EXISTS_TAC [`s0`,`s0`,`s2`,`s3`,`s4`,`s5`] \\ SWAP_TAC) 388 |> SIMP_RULE std_ss [LET_DEF]; 389 390val _ = save_thm("lisp_inv_copy",lisp_inv_copy); 391 392 393(* assign const *) 394 395val lisp_inv_Val = prove( 396 ``!w. ^LISP ==> let (x0,w0) = (Val (w2n w), w2w (w:word30) << 2 !! 1w) in ^LISP``, 397 SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 398 \\ Q.EXISTS_TAC `H_DATA (INL w)` 399 \\ Q.LIST_EXISTS_TAC [`s1`,`s2`,`s3`,`s4`,`s5`] \\ SWAP_TAC) 400 |> SIMP_RULE std_ss [LET_DEF]; 401 402val _ = save_thm("lisp_inv_Val",lisp_inv_Val); 403 404val BLAST_LEMMA = prove(``w << 2 !! 1w = w << 2 + 1w:word32``,blastLib.BBLAST_TAC); 405val lisp_inv_Val_n2w = Q.SPEC `n2w n` lisp_inv_Val 406 |> DISCH ``n < dimword (:30)`` |> SIMP_RULE std_ss [w2n_n2w,AND_IMP_INTRO,BLAST_LEMMA] 407 |> SIMP_RULE (std_ss++SIZES_ss) [w2w_def,WORD_MUL_LSL,word_mul_n2w,word_add_n2w,w2n_n2w] 408 |> Q.GEN `n` 409 410val _ = save_thm("lisp_inv_Val_n2w",lisp_inv_Val_n2w); 411 412val LIST_FIND_APPEND = prove( 413 ``!xs x k d. (LIST_FIND k x xs = SOME d) ==> (LIST_FIND k (x:'a) (xs++ys) = SOME d)``, 414 Induct \\ SIMP_TAC std_ss [LIST_FIND_def,APPEND] \\ REPEAT STRIP_TAC 415 \\ Cases_on `x = h` \\ FULL_SIMP_TAC std_ss []); 416 417val LIST_FIND_NEQ = prove( 418 ``!xs k d. (LIST_FIND k x xs = SOME d) /\ ~(x = y) ==> 419 ~(LIST_FIND k (y:'a) (xs++ys) = SOME d)``, 420 Induct \\ SIMP_TAC std_ss [LIST_FIND_def,APPEND] \\ REPEAT STRIP_TAC 421 \\ Cases_on `x = h` \\ FULL_SIMP_TAC std_ss [] THEN1 422 (`~(y = h)` by ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [] 423 \\ IMP_RES_TAC LIST_FIND_LESS_EQ \\ DECIDE_TAC) 424 \\ Cases_on `y = h` \\ FULL_SIMP_TAC std_ss [] 425 \\ RES_TAC \\ IMP_RES_TAC LIST_FIND_LESS_EQ \\ DECIDE_TAC); 426 427val EXISTS_OVER_CONJ = METIS_PROVE [] ``(?x. P x) /\ Q = ?x. P x /\ Q``; 428 429val lisp_inv_Sym_w2w_lemma = prove( 430 ``!w v. (w2w (w:29 word) << 3 !! 3w = w2w v << 3 !! 3w:word32) = (w = v)``, 431 blastLib.BBLAST_TAC) 432 433val lisp_inv_Sym_blast = prove( 434 ``(w:word32 << 3 !! 0x3w = 8w * w + 3w) /\ 435 (v:word64 << 3 !! 0x3w = 8w * v + 3w)``, 436 blastLib.BBLAST_TAC) 437 438val lisp_inv_Sym_lemma = prove( 439 ``!w s. (LIST_FIND 0 s INIT_SYMBOLS = SOME (w2n w)) ==> ^LISP ==> 440 (let (x0,w0) = (Sym s, w2w (w:29 word) << 3 !! 3w) in ^LISP) /\ 441 (((w2w w0):word64 = w2w (w:29 word) << 3 !! 3w) = (x0 = Sym s))``, 442 SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 443 \\ Q.EXISTS_TAC `H_DATA (INR w)` 444 \\ Q.LIST_EXISTS_TAC [`s1`,`s2`,`s3`,`s4`,`s5`] 445 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 446 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 447 \\ FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 448 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 449 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] 450 \\ REVERSE (REPEAT STRIP_TAC) THEN1 451 (Cases_on `x0` \\ FULL_SIMP_TAC (srw_ss()) [lisp_x_def] 452 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (MP_TAC o GSYM) 453 \\ ASM_SIMP_TAC std_ss [ref_heap_addr_def] \\ REPEAT STRIP_TAC 454 \\ POP_ASSUM MP_TAC THEN1 blastLib.BBLAST_TAC THEN1 blastLib.BBLAST_TAC 455 \\ REPEAT STRIP_TAC \\ Cases_on `s = s'` THEN1 456 (`SOME (w2n w) = SOME k` by METIS_TAC [LIST_FIND_APPEND] 457 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,lisp_inv_Sym_blast] 458 \\ `(8 * k + 3) < 4294967296` by DECIDE_TAC 459 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w]) 460 \\ `~(w2n w = k)` by METIS_TAC [LIST_FIND_NEQ] 461 \\ ASM_SIMP_TAC std_ss [lisp_inv_Sym_w2w_lemma] 462 \\ Cases_on `w` \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,w2n_n2w] 463 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,lisp_inv_Sym_blast] 464 \\ `(8 * k + 3) < 4294967296` by DECIDE_TAC 465 \\ `(8 * n + 3) < 4294967296` by DECIDE_TAC 466 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w] 467 \\ IMP_RES_TAC (DECIDE ``n<4294967296 ==> n<18446744073709551616:num``) 468 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC) 469 THEN1 470 (Q.EXISTS_TAC `w2n w` 471 \\ ASM_SIMP_TAC std_ss [n2w_w2n,w2n_lt29,LIST_FIND_APPEND]) 472 \\ REPEAT STRIP_TAC 473 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 474 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 475 |> SIMP_RULE std_ss [LET_DEF] |> Q.SPEC `n2w n` |> GEN ``n:num``; 476 477val lisp_inv_Sym = let 478 fun zip_index i [] = [] 479 | zip_index i (x::xs) = (numSyntax.term_of_int i,x) :: zip_index (i+1) xs 480 in INIT_SYMBOLS_def 481 |> concl |> dest_eq |> snd |> listSyntax.dest_list |> fst |> zip_index 0 482 |> map (fn (x,y) => SPECL [x,y] lisp_inv_Sym_lemma) 483 |> map (CONV_RULE ((RATOR_CONV o RAND_CONV) EVAL)) 484 |> map (SIMP_RULE (srw_ss()) [w2w_n2w,bitTheory.BITS_THM, 485 WORD_MUL_LSL,word_mul_n2w,word_or_n2w]) 486 |> LIST_CONJ 487 end ; 488 489val _ = save_thm("lisp_inv_Sym",lisp_inv_Sym); 490 491val lisp_inv_nil = prove( 492 ``^LISP ==> let (x0,w0) = (Sym "NIL",w2w tw0) in ^LISP``, 493 SIMP_TAC std_ss [LET_DEF] 494 \\ STRIP_TAC \\ `tw0 = 3w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 495 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_n2w,BITS_THM] 496 \\ IMP_RES_TAC (hd (CONJUNCTS lisp_inv_Sym))) |> SIMP_RULE std_ss [LET_DEF]; 497 498val lisp_inv_zero = prove( 499 ``^LISP ==> let (x0,w0) = (Val 0,w2w tw1) in ^LISP``, 500 SIMP_TAC std_ss [LET_DEF] 501 \\ STRIP_TAC \\ `tw1 = 1w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 502 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_n2w,BITS_THM] 503 \\ MATCH_MP_TAC (SIMP_RULE std_ss [] (Q.SPEC `0` lisp_inv_Val_n2w)) 504 \\ ASM_SIMP_TAC std_ss []) |> SIMP_RULE std_ss [LET_DEF]; 505 506val _ = save_thm("lisp_inv_nil",lisp_inv_nil); 507val _ = save_thm("lisp_inv_zero",lisp_inv_zero); 508 509 510(* car and cdr *) 511 512val RANGE_TAC = FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC 513 514val ADDR_SET = SIMP_RULE std_ss [EXTENSION,GSPECIFICATION] ADDR_SET_def |> 515 SIMP_RULE std_ss [IN_DEF, SimpLHS]; 516 517val lisp_inv_car = prove( 518 ``isDot x0 ==> ^LISP ==> 519 (let (x0,w0) = (CAR x0,f (bp + 4w * w2w w0)) in ^LISP) /\ 520 (bp + 4w * w2w w0) IN df /\ (w0 && 1w = 0w) /\ ((bp + 4w * w2w w0) && 3w = 0w)``, 521 SIMP_TAC std_ss [isDot_thm] \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [LET_DEF,CAR_def] 522 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 523 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,lisp_x_def] 524 \\ Q.LIST_EXISTS_TAC [`ax`,`s1`,`s2`,`s3`,`s4`,`s5`] 525 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b'`] 526 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11] 527 \\ Q.PAT_X_ASSUM `xx = w0` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 528 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,CONJ_ASSOC] 529 \\ REVERSE STRIP_TAC 530 THEN1 (Q.PAT_X_ASSUM `bp && 3w = 0w` MP_TAC \\ blastLib.BBLAST_TAC) 531 \\ REVERSE STRIP_TAC 532 THEN1 (Q.PAT_X_ASSUM `bp && 3w = 0w` MP_TAC \\ blastLib.BBLAST_TAC) 533 \\ `k < i` by 534 (FULL_SIMP_TAC std_ss [ok_split_heap_def,RANGE_def] \\ CCONTR_TAC 535 \\ FULL_SIMP_TAC std_ss [NOT_LESS] \\ RES_TAC 536 \\ FULL_SIMP_TAC (srw_ss()) []) 537 \\ `RANGE(0,e)k /\ k < 2147483648` by RANGE_TAC 538 \\ IMP_RES_TAC ref_mem_RANGE 539 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`m`,`bp`]) 540 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [ref_aux_def] \\ STRIP_TAC 541 \\ `2 * k < 4294967296` by DECIDE_TAC 542 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_MUL_LSL,word_mul_n2w,w2w_def,w2n_n2w] 543 \\ FULL_SIMP_TAC std_ss [MULT_ASSOC,HD,TL,STAR_ASSOC] 544 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 545 \\ FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET] 546 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 547 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] 548 \\ REPEAT STRIP_TAC THEN1 549 (Q.PAT_X_ASSUM `!x. x IN D1 m ==> x IN D0 m` MATCH_MP_TAC 550 \\ SIMP_TAC std_ss [D1_def,IN_DEF] \\ Q.EXISTS_TAC `k` 551 \\ ASM_SIMP_TAC (srw_ss()) [ADDR_SET]) 552 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 553 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 554 |> SIMP_RULE std_ss [LET_DEF]; 555 556val lisp_inv_cdr = prove( 557 ``isDot x0 ==> ^LISP ==> 558 (let (x0,w0) = (CDR x0,f (bp + 4w * w2w w0 + 4w)) in ^LISP) /\ 559 (bp + 4w * w2w w0 + 4w) IN df /\ (w0 && 1w = 0w) /\ ((bp + 4w * w2w w0 + 4w) && 3w = 0w)``, 560 SIMP_TAC std_ss [isDot_thm] \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [LET_DEF,CDR_def] 561 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 562 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,lisp_x_def] 563 \\ Q.LIST_EXISTS_TAC [`ay`,`s1`,`s2`,`s3`,`s4`,`s5`] 564 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b'`] 565 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11] 566 \\ Q.PAT_X_ASSUM `xx = w0` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 567 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,CONJ_ASSOC] 568 \\ REVERSE STRIP_TAC 569 THEN1 (Q.PAT_X_ASSUM `bp && 3w = 0w` MP_TAC \\ blastLib.BBLAST_TAC) 570 \\ REVERSE STRIP_TAC 571 THEN1 (Q.PAT_X_ASSUM `bp && 3w = 0w` MP_TAC \\ blastLib.BBLAST_TAC) 572 \\ `k < i` by 573 (FULL_SIMP_TAC std_ss [ok_split_heap_def,RANGE_def] \\ CCONTR_TAC 574 \\ FULL_SIMP_TAC std_ss [NOT_LESS] \\ RES_TAC 575 \\ FULL_SIMP_TAC (srw_ss()) []) 576 \\ `RANGE(0,e)k /\ k < 2147483648` by RANGE_TAC 577 \\ IMP_RES_TAC ref_mem_RANGE 578 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`m`,`bp`]) 579 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [ref_aux_def] \\ STRIP_TAC 580 \\ `2 * k < 4294967296` by DECIDE_TAC 581 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_MUL_LSL,word_mul_n2w,w2w_def,w2n_n2w] 582 \\ FULL_SIMP_TAC std_ss [MULT_ASSOC,HD,TL] 583 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 584 \\ FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET] 585 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 586 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] 587 \\ REPEAT STRIP_TAC THEN1 588 (Q.PAT_X_ASSUM `!x. x IN D1 m ==> x IN D0 m` MATCH_MP_TAC 589 \\ SIMP_TAC std_ss [D1_def,IN_DEF] \\ Q.EXISTS_TAC `k` 590 \\ ASM_SIMP_TAC (srw_ss()) [ADDR_SET]) 591 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 592 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 593 |> SIMP_RULE std_ss [LET_DEF]; 594 595val _ = save_thm("lisp_inv_car",lisp_inv_car); 596val _ = save_thm("lisp_inv_cdr",lisp_inv_cdr); 597 598 599(* cons *) 600 601 602 603val lisp_x_UPDATE = prove( 604 ``!m s i x. 605 (m i = H_EMP) ==> 606 !y p. lisp_x (m,s) (p,y) ==> lisp_x ((i =+ x) m,s) (p,y)``, 607 NTAC 5 STRIP_TAC \\ Induct \\ FULL_SIMP_TAC std_ss [lisp_x_def] 608 \\ REPEAT STRIP_TAC \\ RES_TAC \\ ASM_SIMP_TAC (srw_ss()) [] 609 \\ Cases_on `i = k` \\ FULL_SIMP_TAC (srw_ss()) [APPLY_UPDATE_THM]); 610 611val lisp_inv_cons_blast = blastLib.BBLAST_PROVE 612 ``(bp && 3w = 0w:word64) ==> 613 (bp + 4w * wi && 3w = 0w) /\ (bp + 4w * wi + 4w && 3w = 0w)``; 614 615val IN_D0 = SIMP_CONV bool_ss [IN_DEF, D0_def] ``x IN D0 m`` 616val IN_D1 = (REWRITE_CONV [IN_DEF] THENC SIMP_CONV bool_ss [D1_def]) 617 ``x IN D1 m`` 618 619 620val lisp_inv_cons = prove( 621 ``~(wi = we) ==> ^LISP ==> 622 (let (x0,w0,wi,f) = (Dot x0 x1,w2w wi,wi+2w, 623 (bp + 4w * wi =+ w0) ((bp + 4w * wi + 4w =+ w1) f)) in ^LISP) /\ 624 (bp + 4w * wi) IN df /\ (bp + 4w * wi + 4w) IN df /\ 625 (bp + 4w * wi && 3w = 0w) /\ (bp + 4w * wi + 4w && 3w = 0w)``, 626 SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 627 \\ ASM_SIMP_TAC std_ss [lisp_inv_cons_blast] 628 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 629 \\ Q.LIST_EXISTS_TAC [`H_ADDR i`,`s1`,`s2`,`s3`,`s4`,`s5`] 630 \\ Q.LIST_EXISTS_TAC [`(i =+ H_BLOCK ([s0;s1],0,())) m`,`i+1`,`ss`,`ss1`,`sym`,`b`] 631 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,word_add_n2w,ref_heap_addr_def, 632 LEFT_ADD_DISTRIB,WORD_MUL_LSL,word_mul_n2w] 633 \\ `2 * i < 18446744073709551616 /\ 2 * e < 18446744073709551616` by DECIDE_TAC 634 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,n2w_11] 635 \\ `i+1<=e` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 636 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 637 \\ Q.ABBREV_TAC `ss2 = ss ++ ss1` 638 \\ Q.ABBREV_TAC `xs2 = xs ++ xs1` 639 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 640 (FULL_SIMP_TAC std_ss [ok_split_heap_def] \\ REVERSE (REPEAT STRIP_TAC) 641 THEN1 (`~(i = k) /\ i <= k` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM]) 642 THEN1 (FULL_SIMP_TAC std_ss [FUN_EQ_THM,EMPTY_DEF,R0_def,APPLY_UPDATE_THM] 643 \\ SRW_TAC [] []) 644 THEN1 (FULL_SIMP_TAC std_ss [memory_ok_def,APPLY_UPDATE_THM] \\ STRIP_TAC 645 \\ Cases_on `i = i'` \\ ASM_SIMP_TAC (srw_ss()) [] \\ METIS_TAC []) 646 \\ `D0 ((i =+ H_BLOCK ([s0; s1],0,())) m) = i INSERT D0 m` by 647 (SIMP_TAC std_ss [EXTENSION,IN_INSERT] 648 \\ SIMP_TAC std_ss [IN_DEF,D0_def,APPLY_UPDATE_THM] \\ STRIP_TAC 649 \\ Cases_on `i = x` \\ ASM_SIMP_TAC (srw_ss()) []) 650 \\ `D1 ((i =+ H_BLOCK ([s0; s1],0,())) m) = 651 ADDR_SET [s0;s1] UNION D1 m` by 652 (SIMP_TAC std_ss [EXTENSION,IN_UNION,ADDR_SET_def,GSPECIFICATION] 653 \\ SIMP_TAC std_ss [IN_D1,IN_D0,APPLY_UPDATE_THM] \\ STRIP_TAC 654 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 655 (Cases_on `i = k` \\ FULL_SIMP_TAC (srw_ss()) [] THEN1 656 (Q.PAT_X_ASSUM `[s0; s1] = x'` (ASSUME_TAC o GSYM) 657 \\ FULL_SIMP_TAC std_ss [ADDR_SET_def,MEM,GSPECIFICATION]) 658 \\ METIS_TAC []) 659 THEN1 (SIMP_TAC bool_ss [IN_DEF] \\ METIS_TAC [ADDR_SET]) 660 \\ Q.EXISTS_TAC `k` \\ Cases_on `i = k` \\ ASM_SIMP_TAC (srw_ss()) [] 661 \\ `m k = H_EMP` by METIS_TAC [LESS_EQ_REFL] 662 \\ FULL_SIMP_TAC (srw_ss()) []) 663 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_UNION,IN_INSERT] 664 \\ FULL_SIMP_TAC (srw_ss()) [ADDR_SET_def] 665 \\ METIS_TAC []) 666 \\ STRIP_TAC THEN1 667 (FULL_SIMP_TAC (srw_ss()) [EVERY_DEF,CONS_11,lisp_x_def,APPLY_UPDATE_THM] 668 \\ `m i = H_EMP` by FULL_SIMP_TAC std_ss [ok_split_heap_def] 669 \\ ASM_SIMP_TAC std_ss [lisp_x_UPDATE] 670 \\ Q.PAT_X_ASSUM `EVERY (lisp_x (m,INIT_SYMBOLS ++ sym)) (ZIP (ss2,xs2))` MP_TAC 671 \\ Q.SPEC_TAC (`ZIP (ss2,xs2)`,`ys`) 672 \\ Induct \\ ASM_SIMP_TAC std_ss [EVERY_DEF] 673 \\ Cases \\ ASM_SIMP_TAC std_ss [lisp_x_UPDATE]) 674 \\ `RANGE(0,e)i` by RANGE_TAC 675 \\ IMP_RES_TAC ref_mem_UPDATE \\ ASM_SIMP_TAC std_ss [ref_aux_def,STAR_ASSOC,HD,TL] 676 \\ IMP_RES_TAC ref_mem_RANGE 677 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`m`,`bp`]) 678 \\ `m i = H_EMP` by METIS_TAC [LESS_EQ_REFL,ok_split_heap_def] 679 \\ FULL_SIMP_TAC std_ss [ref_aux_def,SEP_CLAUSES,SEP_EXISTS_THM] 680 \\ FULL_SIMP_TAC std_ss [MULT_ASSOC] \\ SEP_R_TAC \\ SEP_W_TAC 681 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 682 |> SIMP_RULE std_ss [LET_DEF]; 683 684val _ = save_thm("lisp_inv_cons",lisp_inv_cons); 685 686 687(* top, pop and push *) 688 689val lisp_inv_top = prove( 690 ``~(xs = []) ==> ^LISP ==> 691 (let (x0,w0) = (HD xs,f (sp + 4w * wsp)) in ^LISP) /\ 692 (sp + 4w * wsp) IN df /\ (sp + 4w * wsp && 3w = 0w)``, 693 Cases_on `xs` \\ SIMP_TAC std_ss [NOT_CONS_NIL,LET_DEF,TL,HD] 694 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 695 \\ REPEAT STRIP_TAC 696 \\ Cases_on `ss` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF] 697 \\ Q.LIST_EXISTS_TAC [`h'`,`s1`,`s2`,`s3`,`s4`,`s5`] 698 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`h'::t'`,`ss1`,`sym`,`b`] 699 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF,LENGTH,ADD1,ZIP,EVERY_DEF,APPEND] 700 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 701 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 702 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 703 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 704 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 705 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 706 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,ref_stack_def,APPEND] \\ SEP_R_TAC 707 \\ SIMP_TAC std_ss [] 708 \\ Q.PAT_X_ASSUM `sp && 3w = 0w` MP_TAC \\ blastLib.BBLAST_TAC) 709 |> SIMP_RULE std_ss [LET_DEF]; 710 711val SPLIT_LIST_LESS_EQ = store_thm("SPLIT_LIST_LESS_EQ", 712 ``!xs j. j <= LENGTH xs ==> 713 ?xs1 xs2. (xs = xs1 ++ xs2) /\ 714 (LENGTH xs1 = j)``, 715 Induct \\ SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC 716 THEN1 (Q.LIST_EXISTS_TAC [`[]`,`[]`] \\ ASM_SIMP_TAC std_ss [LENGTH,APPEND]) 717 \\ Cases_on `j` \\ FULL_SIMP_TAC std_ss [ADD1,LENGTH_NIL,APPEND,CONS_11] 718 \\ RES_TAC \\ Q.EXISTS_TAC `h::xs1` 719 \\ ASM_SIMP_TAC std_ss [LENGTH,APPEND_11,APPEND,CONS_11] 720 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND_11,APPEND,CONS_11,ADD1]); 721 722val ZIP_APPEND = store_thm("ZIP_APPEND", 723 ``!xs1 ys1 xs2 ys2. 724 (LENGTH ys1 = LENGTH xs1) ==> 725 (ZIP (xs1 ++ xs2, ys1 ++ ys2) = ZIP (xs1,ys1) ++ ZIP (xs2,ys2))``, 726 Induct \\ SIMP_TAC std_ss [LENGTH,LENGTH_NIL,ZIP,APPEND] 727 \\ Cases_on `ys1` \\ FULL_SIMP_TAC std_ss [ADD1,LENGTH,ZIP,APPEND]); 728 729val ref_stack_APPEND = store_thm("ref_stack_APPEND", 730 ``!xs ys a. 731 ref_stack a (xs ++ ys) = 732 SEP_ARRAY (\a x. one (a,ref_heap_addr x)) 4w a xs * 733 ref_stack (a + n2w (4 * LENGTH xs)) ys``, 734 Induct \\ ASM_SIMP_TAC std_ss [APPEND,ref_stack_def,LENGTH,SEP_ARRAY_def, 735 SEP_CLAUSES,WORD_ADD_0,STAR_ASSOC,MULT_CLAUSES,GSYM word_add_n2w,WORD_ADD_ASSOC]); 736 737val ref_stack_space_LEMMA = prove( 738 ``!k n p. 739 p * ref_stack_space (sp + n2w (4 * n + 4 * k)) (n + k + 6) = 740 SEP_EXISTS zs. SEP_ARRAY (\a x. one(a,x)) 4w (sp + n2w (4 * n)) zs * 741 p * ref_stack_space (sp + n2w (4 * n)) (n + 6) * 742 cond (LENGTH zs = k)``, 743 Induct THEN1 SIMP_TAC std_ss [FUN_EQ_THM,cond_STAR,SEP_EXISTS_THM,LENGTH_NIL, 744 SEP_ARRAY_def,SEP_CLAUSES] 745 \\ FULL_SIMP_TAC std_ss [GSYM LEFT_ADD_DISTRIB,DECIDE ``n + SUC k = SUC n + k``] 746 \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [ADD_CLAUSES,ref_stack_space_def, 747 SEP_CLAUSES,STAR_ASSOC,FUN_EQ_THM,SEP_EXISTS_THM,cond_STAR] 748 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 749 (Q.EXISTS_TAC `w::zs` \\ FULL_SIMP_TAC std_ss [LENGTH,SEP_ARRAY_def,ADD1, 750 LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_ADD_SUB] 751 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 752 \\ Cases_on `zs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 753 \\ Q.EXISTS_TAC `t` \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `h` 754 \\ FULL_SIMP_TAC std_ss [SEP_ARRAY_def,LEFT_ADD_DISTRIB] 755 \\ FULL_SIMP_TAC std_ss [LENGTH,SEP_ARRAY_def,ADD1, 756 LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_ADD_SUB] 757 \\ FULL_SIMP_TAC (std_ss++star_ss) []); 758 759val lisp_inv_pops_lemma = prove( 760 ``n <= LENGTH xs ==> ^LISP ==> let (xs,wsp) = (DROP n xs,wsp + n2w n) in ^LISP``, 761 STRIP_TAC \\ IMP_RES_TAC SPLIT_LIST_LESS_EQ \\ ASM_SIMP_TAC std_ss [] 762 \\ POP_ASSUM (MP_TAC o GSYM) 763 \\ FULL_SIMP_TAC std_ss [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,LET_DEF] 764 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def] \\ REPEAT STRIP_TAC 765 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 766 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`DROP n ss`,`ss1`,`sym`,`b`] 767 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF,LENGTH_APPEND] 768 \\ `LENGTH xs1' <= LENGTH ss` by DECIDE_TAC 769 \\ IMP_RES_TAC SPLIT_LIST_LESS_EQ 770 \\ FULL_SIMP_TAC std_ss [] 771 \\ POP_ASSUM (MP_TAC o GSYM) 772 \\ FULL_SIMP_TAC std_ss [rich_listTheory.BUTFIRSTN_LENGTH_APPEND] 773 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND] 774 \\ STRIP_TAC THEN1 775 (Q.PAT_X_ASSUM `xx = sl` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 776 \\ Cases_on `wsp` \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_add_n2w,w2n_n2w] 777 \\ `(n' + LENGTH xs1'') < 18446744073709551616` by DECIDE_TAC 778 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC) 779 \\ FULL_SIMP_TAC std_ss [ZIP_APPEND,EVERY_APPEND,GSYM APPEND_ASSOC] 780 \\ REPEAT STRIP_TAC 781 THEN1 782 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 783 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 784 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 785 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 786 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 787 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,ref_stack_def,word_mul_n2w] 788 \\ Cases_on `wsp` \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_add_n2w,w2n_n2w] 789 \\ `(n' + LENGTH xs1'') < 18446744073709551616` by DECIDE_TAC 790 \\ FULL_SIMP_TAC std_ss [ref_stack_APPEND,word_mul_n2w,word_arith_lemma1,LEFT_ADD_DISTRIB] 791 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` MP_TAC 792 \\ ONCE_REWRITE_TAC [STAR_COMM] 793 \\ ASM_SIMP_TAC std_ss [ref_stack_space_LEMMA] 794 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,SEP_EXISTS_THM,cond_STAR] 795 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `MAP ref_heap_addr xs1''` 796 \\ ASM_SIMP_TAC std_ss [LENGTH_MAP] 797 \\ `SEP_ARRAY (\a x. one (a,x)) 0x4w (sp + n2w (4 * n')) 798 (MAP ref_heap_addr xs1'') = 799 SEP_ARRAY (\a x. one (a,ref_heap_addr x)) 0x4w 800 (sp + n2w (4 * n')) xs1''` by 801 (Q.SPEC_TAC (`(sp + n2w (4 * n'))`,`w`) \\ Q.SPEC_TAC (`xs1''`,`ws`) 802 \\ Induct \\ ASM_SIMP_TAC std_ss [MAP,SEP_ARRAY_def,SEP_CLAUSES]) 803 \\ FULL_SIMP_TAC std_ss [SEP_ARRAY_APPEND,LENGTH_APPEND,LEFT_ADD_DISTRIB, 804 ADD_ASSOC,word_arith_lemma1,word_mul_n2w] 805 \\ FULL_SIMP_TAC std_ss [AC MULT_COMM MULT_ASSOC,AC ADD_COMM ADD_ASSOC]) 806 |> SIMP_RULE std_ss [LET_DEF]; 807 808val lisp_inv_pops = prove( 809 ``w2n (j:word30) <= LENGTH xs ==> ^LISP ==> let (xs,wsp) = (DROP (w2n j) xs,wsp + w2w j) in ^LISP``, 810 Cases_on `j` \\ ASM_SIMP_TAC std_ss [w2n_n2w,w2w_def,LET_DEF] \\ STRIP_TAC 811 \\ METIS_TAC [lisp_inv_pops_lemma]); 812 813val lisp_inv_pop = prove( 814 ``~(xs = []) ==> ^LISP ==> let (xs,wsp) = (TL xs,wsp+1w) in ^LISP``, 815 Cases_on `xs` \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL,TL] \\ STRIP_TAC 816 \\ `w2n (1w:word30) <= LENGTH (h::t)` by 817 SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,LENGTH,ADD1] 818 \\ IMP_RES_TAC (Q.INST [`j`|->`1w`] lisp_inv_pops) 819 \\ FULL_SIMP_TAC std_ss [EVAL ``w2n (1w:word30)``,DROP_def,DROP_0] 820 \\ FULL_SIMP_TAC std_ss [LET_DEF,EVAL ``(w2w (1w:word30)):word64``]) 821 |> SIMP_RULE std_ss [LET_DEF]; 822 823val lisp_inv_push = prove( 824 ``~(wsp = 0w) ==> ^LISP ==> 825 (let (xs,wsp,f) = (x0::xs,wsp-1w,(sp + 4w * (wsp-1w) =+ w0) f) in ^LISP) /\ 826 (sp + 4w * (wsp-1w)) IN df /\ (sp + 4w * (wsp-1w) && 3w = 0w)``, 827 STRIP_TAC \\ STRIP_TAC 828 \\ `(sp + 4w * (wsp-1w) && 3w = 0w)` by (FULL_SIMP_TAC std_ss [lisp_inv_def,lisp_inv_cons_blast]) 829 \\ ASM_SIMP_TAC std_ss [LET_DEF] 830 \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 831 \\ Cases_on `wsp` \\ ASM_SIMP_TAC std_ss [n2w_11,LET_DEF,ZERO_LT_dimword] 832 \\ Cases_on `n` \\ ASM_SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 833 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 834 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 835 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`s0::ss`,`ss1`,`sym`,`b`] 836 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 837 \\ `n' < dimword (:64)` by DECIDE_TAC 838 \\ Q.PAT_X_ASSUM `xxx = sl` MP_TAC 839 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,w2n_n2w,word_add_n2w,APPEND] 840 \\ REPEAT STRIP_TAC THEN1 DECIDE_TAC 841 THEN1 842 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 843 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 844 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 845 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 846 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 847 \\ Q.PAT_X_ASSUM `n' + 1 < dimword (:64)` ASSUME_TAC 848 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,ref_stack_def,word_mul_n2w,w2n_n2w,APPEND] 849 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,word_mul_n2w,LENGTH,LEFT_ADD_DISTRIB,ADD1] 850 \\ `n' + 1 + 6 = SUC (n' + 6)` by DECIDE_TAC 851 \\ FULL_SIMP_TAC std_ss [ref_stack_space_def,SEP_CLAUSES,STAR_ASSOC,SEP_EXISTS_THM] 852 \\ FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_ADD_SUB] 853 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 854 \\ SEP_W_TAC \\ SEP_R_TAC 855 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 856 |> SIMP_RULE std_ss [LET_DEF]; 857 858val _ = save_thm("lisp_inv_top",lisp_inv_top); 859val _ = save_thm("lisp_inv_pop",lisp_inv_pop); 860val _ = save_thm("lisp_inv_push",lisp_inv_push); 861val _ = save_thm("lisp_inv_pops",lisp_inv_pops); 862val _ = save_thm("lisp_inv_pops_lemma",lisp_inv_pops_lemma); 863 864 865(* store and load from stack *) 866 867val SPLIT_LIST = store_thm("SPLIT_LIST", 868 ``!xs j. j < LENGTH xs ==> 869 ?xs1 x xs2. (xs = xs1 ++ x::xs2) /\ 870 (LENGTH xs1 = j)``, 871 Induct \\ SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC 872 \\ Cases_on `j` \\ FULL_SIMP_TAC std_ss [ADD1,LENGTH_NIL,APPEND,CONS_11] 873 \\ RES_TAC \\ Q.EXISTS_TAC `h::xs1` 874 \\ ASM_SIMP_TAC std_ss [LENGTH,APPEND_11,APPEND,CONS_11] 875 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND_11,APPEND,CONS_11,ADD1]); 876 877val lisp_inv_load_blast = prove( 878 ``(w + 4w * x && 3w = 0w) = (w && 3w = 0w:word64)``, 879 blastLib.BBLAST_TAC); 880 881val lisp_inv_load_lemma = prove( 882 ``n < LENGTH xs ==> ^LISP ==> 883 (let (x0,w0) = (EL n xs,f (sp + 4w * wsp + 4w * n2w n)) in ^LISP) /\ 884 (sp + 4w * wsp + 4w * n2w n) IN df /\ (sp + 4w * wsp + 4w * n2w n && 3w = 0w)``, 885 SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 886 \\ REPEAT STRIP_TAC 887 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF] 888 \\ Q.LIST_EXISTS_TAC [`EL n ss`,`s1`,`s2`,`s3`,`s4`,`s5`] 889 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 890 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF,LENGTH,ADD1,ZIP,EVERY_DEF] 891 \\ `?ss1 s ss2. (ss = ss1 ++ s::ss2) /\ (LENGTH ss1 = n)` by METIS_TAC [SPLIT_LIST,APPEND_ASSOC,APPEND] 892 \\ `?xs1 x xs2. (xs = xs1 ++ x::xs2) /\ (LENGTH xs1 = n)` by METIS_TAC [SPLIT_LIST,APPEND_ASSOC,APPEND] 893 \\ FULL_SIMP_TAC std_ss [ZIP_APPEND,ZIP,EVERY_DEF,EVERY_APPEND,GSYM APPEND_ASSOC] 894 \\ FULL_SIMP_TAC std_ss [ZIP,APPEND,EVERY_DEF] 895 \\ FULL_SIMP_TAC std_ss [rich_listTheory.EL_APPEND2,LENGTH_APPEND,LENGTH,EL,HD] 896 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 897 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 898 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 899 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 900 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 901 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 902 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,GSYM APPEND_ASSOC] 903 \\ FULL_SIMP_TAC std_ss [ref_stack_def,Once ref_stack_APPEND,APPEND] 904 \\ FULL_SIMP_TAC std_ss [word_mul_n2w] 905 \\ SEP_R_TAC \\ SIMP_TAC std_ss [] 906 \\ FULL_SIMP_TAC std_ss [GSYM word_mul_n2w] 907 \\ FULL_SIMP_TAC std_ss [lisp_inv_load_blast]) 908 |> SIMP_RULE std_ss [LET_DEF]; 909 910val lisp_inv_load = prove( 911 ``w2n (j:29 word) < LENGTH xs ==> ^LISP ==> 912 (let (x0,w0) = (EL (w2n j) xs,f (sp + 4w * wsp + 4w * w2w j)) in ^LISP) /\ 913 (sp + 4w * wsp + 4w * w2w j) IN df /\ (sp + 4w * wsp + 4w * w2w j && 3w = 0w)``, 914 Cases_on `j` \\ FULL_SIMP_TAC std_ss [w2n_n2w,w2w_def,LET_DEF] 915 \\ METIS_TAC [lisp_inv_load_lemma]) |> SIMP_RULE std_ss [LET_DEF]; 916 917val LENGTH_UPDATE_NTH = store_thm("LENGTH_UPDATE_NTH", 918 ``!xs n x. (LENGTH (UPDATE_NTH n x xs) = LENGTH xs)``, 919 Induct \\ Cases_on `n` \\ ASM_SIMP_TAC std_ss [UPDATE_NTH_def,LENGTH]); 920 921val UPDATE_NTH_APPEND = prove( 922 ``!xs ys zs y x n. 923 (LENGTH xs = n) ==> 924 (UPDATE_NTH n x (xs ++ y::ys) ++ zs = xs ++ x::ys ++ zs)``, 925 Induct \\ FULL_SIMP_TAC std_ss [LENGTH,APPEND,UPDATE_NTH_def,CONS_11]); 926 927val lisp_inv_store_lemma = prove( 928 ``n < LENGTH xs ==> ^LISP ==> 929 (let (xs,f) = (UPDATE_NTH n x0 xs,((sp + 4w * wsp + 4w * n2w n) =+ w0) f) in ^LISP) /\ 930 (sp + 4w * wsp + 4w * n2w n) IN df /\ (sp + 4w * wsp + 4w * n2w n && 3w = 0w)``, 931 SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 932 \\ REPEAT STRIP_TAC 933 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF] 934 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 935 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`UPDATE_NTH n s0 ss`,`ss1`,`sym`,`b`] 936 \\ FULL_SIMP_TAC std_ss [LENGTH_UPDATE_NTH] 937 \\ `?ss1 s ss2. (ss = ss1 ++ s::ss2) /\ (LENGTH ss1 = n)` by METIS_TAC [SPLIT_LIST,APPEND_ASSOC,APPEND] 938 \\ `?xs1 x xs2. (xs = xs1 ++ x::xs2) /\ (LENGTH xs1 = n)` by METIS_TAC [SPLIT_LIST,APPEND_ASSOC,APPEND] 939 \\ FULL_SIMP_TAC std_ss [ZIP_APPEND,ZIP,EVERY_DEF,EVERY_APPEND,GSYM APPEND_ASSOC] 940 \\ FULL_SIMP_TAC std_ss [ZIP,APPEND,EVERY_DEF] 941 \\ FULL_SIMP_TAC std_ss [UPDATE_NTH_APPEND] 942 \\ FULL_SIMP_TAC std_ss [ZIP_APPEND,ZIP,EVERY_DEF,EVERY_APPEND,GSYM APPEND_ASSOC] 943 \\ FULL_SIMP_TAC std_ss [APPEND,ZIP,EVERY_DEF] 944 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 945 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 946 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 947 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 948 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 949 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 950 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,UPDATE_NTH_APPEND] 951 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 952 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,ref_stack_def,ref_stack_APPEND] 953 \\ FULL_SIMP_TAC std_ss [lisp_inv_load_blast] 954 \\ FULL_SIMP_TAC std_ss [word_mul_n2w] 955 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] \\ SEP_W_TAC 956 \\ FULL_SIMP_TAC (std_ss++star_ss) [MAP,CONS_11] 957 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,LENGTH_APPEND,LENGTH] \\ METIS_TAC []) 958 |> SIMP_RULE std_ss [LET_DEF]; 959 960val lisp_inv_store = prove( 961 ``w2n (j:29 word) < LENGTH xs ==> ^LISP ==> 962 (let (xs,f) = (UPDATE_NTH (w2n j) x0 xs,((sp + 4w * wsp + 4w * w2w j) =+ w0) f) in ^LISP) /\ 963 (sp + 4w * wsp + 4w * w2w j) IN df /\ (sp + 4w * wsp + 4w * w2w j && 3w = 0w)``, 964 Cases_on `j` \\ FULL_SIMP_TAC std_ss [w2n_n2w,w2w_def,LET_DEF] 965 \\ METIS_TAC [lisp_inv_store_lemma]) |> SIMP_RULE std_ss [LET_DEF]; 966 967val _ = save_thm("lisp_inv_load",lisp_inv_load); 968val _ = save_thm("lisp_inv_load_lemma",lisp_inv_load_lemma); 969val _ = save_thm("lisp_inv_store",lisp_inv_store); 970val _ = save_thm("lisp_inv_store_lemma",lisp_inv_store_lemma); 971 972 973(* test for Dot and Sym and pointer equality *) 974 975val lisp_inv_type = prove( 976 ``^LISP ==> 977 ((w0 && 1w = 0w) = isDot x0) /\ 978 ((w0 && 3w = 1w) = isVal x0) /\ 979 ((w0 && 3w = 3w) = isSym x0)``, 980 SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 981 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,CONS_11] 982 \\ Q.PAT_X_ASSUM `xxx = w0` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 983 \\ Cases_on `x0` \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def, 984 isDot_def,isSym_def,isVal_def] \\ blastLib.BBLAST_TAC); 985 986val _ = save_thm("lisp_inv_type",lisp_inv_type); 987 988val lisp_inv_ignore_tw2 = prove( 989 ``^LISP ==> let tw2 = temp in ^LISP``, 990 SIMP_TAC std_ss [LET_DEF,lisp_inv_def]) |> SIMP_RULE std_ss [LET_DEF]; 991 992val _ = save_thm("lisp_inv_ignore_tw2",lisp_inv_ignore_tw2); 993 994val lisp_inv_ignore_ret_stack = prove( 995 ``^LISP ==> let qs = temp in ^LISP``, 996 SIMP_TAC std_ss [LET_DEF,lisp_inv_def]) |> SIMP_RULE std_ss [LET_DEF]; 997 998val _ = save_thm("lisp_inv_ignore_ret_stack",lisp_inv_ignore_ret_stack); 999 1000val lisp_inv_isSym = prove( 1001 ``^LISP ==> 1002 ((w2w w0 && tw0 = tw0) = isSym x0) /\ 1003 let tw2 = w2w w0 && tw0 in ^LISP``, 1004 REVERSE (REPEAT STRIP_TAC) \\ IMP_RES_TAC (GSYM lisp_inv_type) 1005 THEN1 (ASM_SIMP_TAC std_ss [LET_DEF] \\ METIS_TAC [lisp_inv_ignore_tw2]) 1006 \\ ASM_SIMP_TAC std_ss [] 1007 \\ `tw0 = 3w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1008 \\ `tw1 = 1w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1009 \\ ASM_SIMP_TAC std_ss [] THEN1 blastLib.BBLAST_TAC) |> SIMP_RULE std_ss [LET_DEF]; 1010 1011val lisp_inv_isVal = prove( 1012 ``^LISP ==> 1013 ((w2w w0 && tw0 = tw1) = isVal x0) /\ 1014 let tw2 = w2w w0 && tw0 in ^LISP``, 1015 REVERSE (REPEAT STRIP_TAC) \\ IMP_RES_TAC (GSYM lisp_inv_type) 1016 THEN1 (ASM_SIMP_TAC std_ss [LET_DEF] \\ METIS_TAC [lisp_inv_ignore_tw2]) 1017 \\ ASM_SIMP_TAC std_ss [] 1018 \\ `tw0 = 3w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1019 \\ `tw1 = 1w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1020 \\ ASM_SIMP_TAC std_ss [] THEN1 blastLib.BBLAST_TAC) |> SIMP_RULE std_ss [LET_DEF]; 1021 1022val _ = save_thm("lisp_inv_isVal",lisp_inv_isVal); 1023val _ = save_thm("lisp_inv_isSym",lisp_inv_isSym); 1024 1025val WORD_OR_EQ_WORD_ADD_LEMMA = prove( 1026 ``!w. (w << 2 !! 1w = w << 2 + 1w:word32) /\ 1027 (w << 3 !! 3w = w << 3 + 3w:word32)``, 1028 blastLib.BBLAST_TAC); 1029 1030val LIST_FIND_LEMMA = prove( 1031 ``!xs k. ~(s1 = s2) /\ 1032 (LIST_FIND k s1 xs = SOME n) ==> 1033 (LIST_FIND k s2 xs = SOME m) ==> ~(m = n)``, 1034 Induct \\ SIMP_TAC std_ss [LIST_FIND_def] \\ REPEAT STRIP_TAC 1035 \\ Cases_on `s1 = h` \\ FULL_SIMP_TAC std_ss [] 1036 \\ Cases_on `s2 = h` \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC 1037 \\ IMP_RES_TAC LIST_FIND_LESS_EQ \\ DECIDE_TAC); 1038 1039val lisp_inv_eq_lemma = prove( 1040 ``~isDot x0 ==> ^LISP ==> 1041 ((w0 = w1) = (x0 = x1))``, 1042 Cases_on `x0` \\ Cases_on `x1` \\ SIMP_TAC (srw_ss()) [isDot_def] 1043 \\ SIMP_TAC std_ss [lisp_inv_def,MAP,CONS_11] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 1044 \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC \\ ASM_SIMP_TAC std_ss [] 1045 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,lisp_x_def,ref_heap_addr_def] 1046 THEN1 blastLib.BBLAST_TAC 1047 THEN1 1048 (REPEAT STRIP_TAC 1049 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_OR_EQ_WORD_ADD_LEMMA,w2w_def,w2n_n2w] 1050 \\ `(4 * n' + 1) < 4294967296` by DECIDE_TAC 1051 \\ `(4 * n + 1) < 4294967296` by DECIDE_TAC 1052 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_MUL_LSL,word_mul_n2w,word_add_n2w,n2w_11] 1053 \\ DECIDE_TAC) 1054 THEN1 blastLib.BBLAST_TAC 1055 THEN1 blastLib.BBLAST_TAC 1056 THEN1 blastLib.BBLAST_TAC 1057 THEN1 1058 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [APPEND] 1059 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_OR_EQ_WORD_ADD_LEMMA,w2w_def,w2n_n2w] 1060 \\ `(8 * k' + 3) < 4294967296` by DECIDE_TAC 1061 \\ `(8 * k + 3) < 4294967296` by DECIDE_TAC 1062 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_MUL_LSL,word_mul_n2w,word_add_n2w,n2w_11] 1063 \\ Cases_on `s = s'` \\ FULL_SIMP_TAC std_ss [] 1064 \\ IMP_RES_TAC LIST_FIND_LEMMA \\ DECIDE_TAC)); 1065 1066val lisp_inv_eq = prove( 1067 ``~isDot x0 \/ ~isDot x1 ==> ^LISP ==> ((w0 = w1) = (x0 = x1))``, 1068 METIS_TAC [lisp_inv_eq_lemma,lisp_inv_swap1]); 1069 1070val lisp_inv_eq_zero = store_thm("lisp_inv_eq_zero", 1071 ``^LISP ==> ((tw1 = w2w w0) = (x0 = Val 0))``, 1072 REPEAT STRIP_TAC \\ IMP_RES_TAC lisp_inv_swap1 1073 \\ IMP_RES_TAC (Q.SPEC `0w` lisp_inv_Val) 1074 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w] 1075 \\ IMP_RES_TAC lisp_inv_swap1 1076 \\ IMP_RES_TAC (RW [isDot_def] (Q.INST [`x1`|->`Val 0`] lisp_inv_eq)) 1077 \\ FULL_SIMP_TAC std_ss [EVAL ``(w2w (0w:word30):word32) << 2 !! 1w``] 1078 \\ `tw1 = 1w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1079 \\ FULL_SIMP_TAC std_ss [] 1080 \\ Q.PAT_X_ASSUM `xxx = (x0 = Val 0)` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 1081 \\ blastLib.BBLAST_TAC); 1082 1083val lisp_inv_eq_lucky = prove( 1084 ``!x0 x1 w0 w1. (w0 = w1) /\ ^LISP ==> (x0 = x1)``, 1085 REVERSE Induct \\ SIMP_TAC std_ss [] 1086 THEN1 METIS_TAC [lisp_inv_eq,isDot_def] 1087 THEN1 METIS_TAC [lisp_inv_eq,isDot_def] 1088 \\ REVERSE Cases \\ FULL_SIMP_TAC (srw_ss()) [] 1089 THEN1 METIS_TAC [lisp_inv_eq,isDot_def] 1090 THEN1 METIS_TAC [lisp_inv_eq,isDot_def] 1091 \\ REPEAT STRIP_TAC THEN1 1092 (`isDot (Dot x0 x0')` by ASM_SIMP_TAC std_ss [isDot_def] 1093 \\ IMP_RES_TAC lisp_inv_car \\ FULL_SIMP_TAC std_ss [CAR_def] 1094 \\ IMP_RES_TAC lisp_inv_swap1 1095 \\ `isDot (Dot S' S0)` by ASM_SIMP_TAC std_ss [isDot_def] 1096 \\ IMP_RES_TAC lisp_inv_car \\ FULL_SIMP_TAC std_ss [CAR_def] 1097 \\ IMP_RES_TAC lisp_inv_swap1 \\ RES_TAC) 1098 THEN1 1099 (`isDot (Dot x0 x0')` by ASM_SIMP_TAC std_ss [isDot_def] 1100 \\ IMP_RES_TAC lisp_inv_cdr \\ FULL_SIMP_TAC std_ss [CDR_def] 1101 \\ IMP_RES_TAC lisp_inv_swap1 1102 \\ `isDot (Dot S' S0)` by ASM_SIMP_TAC std_ss [isDot_def] 1103 \\ IMP_RES_TAC lisp_inv_cdr \\ FULL_SIMP_TAC std_ss [CDR_def] 1104 \\ IMP_RES_TAC lisp_inv_swap1 \\ RES_TAC)); 1105 1106val _ = save_thm("lisp_inv_eq",lisp_inv_eq); 1107val _ = save_thm("lisp_inv_eq_lucky",lisp_inv_eq_lucky); 1108 1109 1110(* add, sub and < *) 1111 1112val lisp_inv_limit_blast = blastLib.BBLAST_PROVE 1113 ``w << 2 !! 1w = 4w * w + 1w:word32``; 1114 1115val lisp_inv_limit = prove( 1116 ``isVal x0 /\ isVal x1 ==> ^LISP ==> 1117 (getVal x0 + getVal x1 < 2**30 = w2n (w0 - 1w) + w2n w1 < 2**32)``, 1118 SIMP_TAC std_ss [isVal_thm] \\ ASM_SIMP_TAC std_ss [] 1119 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1120 \\ REPEAT STRIP_TAC 1121 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1122 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1123 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1124 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (ASSUME_TAC o GSYM) 1125 \\ FULL_SIMP_TAC std_ss [] 1126 \\ Q.PAT_X_ASSUM `x0 = xxx` (ASSUME_TAC) 1127 \\ Q.PAT_X_ASSUM `x1 = xxx` (ASSUME_TAC) 1128 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def,lisp_inv_limit_blast] 1129 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_n2w,BITS_THM,WORD_ADD_SUB] 1130 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w] 1131 \\ `(4 * a) < 4294967296` by DECIDE_TAC 1132 \\ `(4 * a' + 1) < 4294967296` by DECIDE_TAC 1133 \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 1134 1135val lisp_inv_add_lemma = prove( 1136 ``w2n (w0 - 1w) + w2n w1 < 2**32 ==> ^LISP ==> 1137 isVal x0 /\ isVal x1 ==> 1138 let (x0,w0) = (LISP_ADD x0 x1,w0-1w+w1) in ^LISP``, 1139 SIMP_TAC std_ss [isVal_thm,LISP_ADD_def] \\ ASM_SIMP_TAC std_ss [] 1140 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1141 \\ REPEAT STRIP_TAC 1142 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1143 \\ Q.LIST_EXISTS_TAC [`H_DATA (INL (n2w (a + a')))`,`s1`,`s2`,`s3`,`s4`,`s5`] 1144 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1145 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1146 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def] 1147 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 1148 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 1149 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 1150 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 1151 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1152 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 1153 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1154 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (ASSUME_TAC o GSYM) 1155 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,WORD_OR_EQ_WORD_ADD_LEMMA] 1156 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1157 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,WORD_MUL_LSL] 1158 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB] 1159 \\ FULL_SIMP_TAC std_ss [word_add_n2w,ADD_ASSOC] 1160 \\ `4 * a < 4294967296 /\ 4 * a' + 1 < 4294967296` by DECIDE_TAC 1161 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1162 \\ `(a+a') < 1073741824` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] 1163 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB,LEFT_ADD_DISTRIB]); 1164 1165val lisp_inv_add = prove( 1166 ``^LISP ==> 1167 isVal x0 /\ isVal x1 /\ getVal x0 + getVal x1 < 2**30 ==> 1168 (let (x0,w0) = (LISP_ADD x0 x1,w0-1w+w1) in ^LISP) /\ 1169 w2n (w0 - 1w) + w2n w1 < 2**32``, 1170 REPEAT STRIP_TAC \\ METIS_TAC [lisp_inv_add_lemma,lisp_inv_limit]) 1171 |> SIMP_RULE std_ss [LET_DEF]; 1172 1173val lisp_inv_add_nop = prove( 1174 ``^LISP ==> 1175 isVal x0 /\ isVal x1 /\ ~(getVal x0 + getVal x1 < 2**30) ==> 1176 (let (x0,w0,tw2) = (Val 0,w2w tw1,2w) in ^LISP) /\ 1177 2**32 <= w2n (w0 - 1w) + w2n w1 /\ 1178 ((31 -- 0) tw1 = tw1)``, 1179 REVERSE (REPEAT STRIP_TAC) \\ SIMP_TAC bool_ss [GSYM NOT_LESS] 1180 THEN1 (FULL_SIMP_TAC std_ss [lisp_inv_def] \\ EVAL_TAC) 1181 THEN1 METIS_TAC [lisp_inv_limit] \\ SIMP_TAC std_ss [LET_DEF] 1182 \\ MATCH_MP_TAC lisp_inv_zero 1183 \\ MATCH_MP_TAC lisp_inv_ignore_tw2 \\ ASM_SIMP_TAC std_ss []) 1184 |> SIMP_RULE std_ss [LET_DEF]; 1185 1186val lisp_inv_limit1 = prove( 1187 ``isVal x0 ==> ^LISP ==> 1188 (getVal x0 + 1 < 2**30 = w2n w0 + 4 < 2**32)``, 1189 SIMP_TAC std_ss [isVal_thm] \\ ASM_SIMP_TAC std_ss [] 1190 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1191 \\ REPEAT STRIP_TAC 1192 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1193 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1194 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1195 \\ FULL_SIMP_TAC std_ss [] 1196 \\ Q.PAT_X_ASSUM `x0 = xxx` (ASSUME_TAC) 1197 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def,lisp_inv_limit_blast] 1198 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_n2w,BITS_THM,WORD_ADD_SUB] 1199 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w] 1200 \\ `(4 * a + 1) < 4294967296` by DECIDE_TAC 1201 \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 1202 1203val lisp_inv_add1_lemma = prove( 1204 ``isVal x0 /\ w2n w0 + 4 < 2**32 ==> ^LISP ==> 1205 (let (x0,w0) = (Val (getVal x0 + 1),w0+4w) in ^LISP)``, 1206 SIMP_TAC std_ss [isVal_thm] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1207 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1208 \\ REPEAT STRIP_TAC 1209 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1210 \\ Q.LIST_EXISTS_TAC [`H_DATA (INL (n2w (a + 1)))`,`s1`,`s2`,`s3`,`s4`,`s5`] 1211 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1212 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1213 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def] 1214 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 1215 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 1216 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 1217 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 1218 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1219 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 1220 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1221 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,WORD_OR_EQ_WORD_ADD_LEMMA] 1222 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1223 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,WORD_MUL_LSL] 1224 \\ `4 * a + 1 < 4294967296` by DECIDE_TAC 1225 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1226 \\ `a+1 < 1073741824` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] 1227 \\ AP_TERM_TAC \\ DECIDE_TAC) 1228 |> SIMP_RULE std_ss [LET_DEF]; 1229val lisp_inv_sub = prove( 1230 ``isVal x0 /\ isVal x1 ==> ^LISP ==> 1231 let (x0,w0) = (Val (getVal x0 - getVal x1),if w1 <=+ w0 then (w0-w1)+1w else 1w) in ^LISP``, 1232 SIMP_TAC std_ss [isVal_thm] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1233 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1234 \\ REPEAT STRIP_TAC 1235 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1236 \\ Q.LIST_EXISTS_TAC [`H_DATA (INL (n2w (a - a')))`,`s1`,`s2`,`s3`,`s4`,`s5`] 1237 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1238 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1239 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def] 1240 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 1241 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 1242 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 1243 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 1244 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1245 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 1246 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1247 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (ASSUME_TAC o GSYM) 1248 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,WORD_OR_EQ_WORD_ADD_LEMMA] 1249 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1250 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,WORD_MUL_LSL] 1251 \\ `4 * a + 1 < 4294967296 /\ 4 * a' + 1 < 4294967296` by DECIDE_TAC 1252 \\ `(a-a') < 1073741824` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] 1253 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,word_ls_n2w] 1254 \\ REVERSE (Cases_on `a' <= a`) \\ ASM_SIMP_TAC std_ss [] 1255 THEN1 (`a - a' = 0` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []) 1256 \\ `~(a < a')` by DECIDE_TAC 1257 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2,word_add_n2w] 1258 \\ AP_TERM_TAC \\ DECIDE_TAC) 1259 |> SIMP_RULE std_ss [LET_DEF]; 1260val lisp_inv_sub = prove( 1261 ``isVal x0 /\ isVal x1 ==> ^LISP ==> 1262 let (x0,w0) = (Val (getVal x0 - getVal x1),if w1 <=+ w0 then (w0-w1)+1w else 1w) in ^LISP``, 1263 SIMP_TAC std_ss [isVal_thm] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1264 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1265 \\ REPEAT STRIP_TAC 1266 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1267 \\ Q.LIST_EXISTS_TAC [`H_DATA (INL (n2w (a - a')))`,`s1`,`s2`,`s3`,`s4`,`s5`] 1268 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1269 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1270 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def] 1271 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 1272 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 1273 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 1274 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 1275 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1276 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 1277 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1278 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (ASSUME_TAC o GSYM) 1279 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,WORD_OR_EQ_WORD_ADD_LEMMA] 1280 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1281 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,WORD_MUL_LSL] 1282 \\ `4 * a + 1 < 4294967296 /\ 4 * a' + 1 < 4294967296` by DECIDE_TAC 1283 \\ `(a-a') < 1073741824` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] 1284 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,word_ls_n2w] 1285 \\ REVERSE (Cases_on `a' <= a`) \\ ASM_SIMP_TAC std_ss [] 1286 THEN1 (`a - a' = 0` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []) 1287 \\ `~(a < a')` by DECIDE_TAC 1288 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2,word_add_n2w] 1289 \\ AP_TERM_TAC \\ DECIDE_TAC); 1290 1291val lisp_inv_add1 = prove( 1292 ``^LISP ==> 1293 isVal x0 /\ getVal x0 + 1 < 2**30 ==> 1294 (let (x0,w0) = (LISP_ADD x0 (Val 1),w0+4w) in ^LISP) /\ 1295 w2n w0 + 4 < 2**32``, 1296 SIMP_TAC std_ss [LET_DEF,LISP_ADD_def,getVal_def] 1297 \\ METIS_TAC [SIMP_RULE std_ss [LET_DEF] lisp_inv_add1_lemma, 1298 SIMP_RULE std_ss [LET_DEF] lisp_inv_limit1]) 1299 |> SIMP_RULE std_ss [LET_DEF]; 1300 1301val lisp_inv_add1_nop = prove( 1302 ``^LISP ==> 1303 isVal x0 /\ ~(getVal x0 + 1 < 2**30) ==> 1304 (let (x0,w0,tw2) = (Val 0,w2w tw1,2w) in ^LISP) /\ 1305 2**32 <= w2n w0 + 4 /\ 1306 ((31 -- 0) tw1 = tw1)``, 1307 REVERSE (REPEAT STRIP_TAC) \\ SIMP_TAC bool_ss [GSYM NOT_LESS] 1308 THEN1 (FULL_SIMP_TAC std_ss [lisp_inv_def] \\ EVAL_TAC) 1309 THEN1 METIS_TAC [lisp_inv_limit1] \\ SIMP_TAC std_ss [LET_DEF] 1310 \\ MATCH_MP_TAC lisp_inv_zero 1311 \\ MATCH_MP_TAC lisp_inv_ignore_tw2 \\ ASM_SIMP_TAC std_ss []) 1312 |> SIMP_RULE std_ss [LET_DEF]; 1313 1314val lisp_inv_sub = prove( 1315 ``isVal x0 /\ isVal x1 ==> ^LISP ==> 1316 let (x0,w0) = (LISP_SUB x0 x1,if w0 + 0x1w <+ w1 then w2w tw1 else w0 + 0x1w - w1) in ^LISP``, 1317 SIMP_TAC std_ss [isVal_thm,LISP_SUB_def] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1318 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1319 \\ REPEAT STRIP_TAC 1320 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1321 \\ Q.LIST_EXISTS_TAC [`H_DATA (INL (n2w (a - a')))`,`s1`,`s2`,`s3`,`s4`,`s5`] 1322 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1323 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1324 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def] 1325 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 1326 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 1327 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 1328 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 1329 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1330 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 1331 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1332 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (ASSUME_TAC o GSYM) 1333 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,WORD_OR_EQ_WORD_ADD_LEMMA] 1334 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1335 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,WORD_MUL_LSL] 1336 \\ `4 * a + 1 + 1 < 4294967296 /\ 4 * a' + 1 < 4294967296` by DECIDE_TAC 1337 \\ `(a-a') < 1073741824` by DECIDE_TAC 1338 \\ `4 * (a-a') < 4294967296` by DECIDE_TAC 1339 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w] 1340 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2,word_add_n2w] 1341 \\ STRIP_TAC THEN1 DECIDE_TAC 1342 \\ Cases_on `4 * a + 1 < 4 * a'` \\ ASM_SIMP_TAC std_ss [] 1343 \\ AP_TERM_TAC THEN1 DECIDE_TAC 1344 \\ `a' <= a` by DECIDE_TAC \\ DECIDE_TAC) 1345 |> SIMP_RULE std_ss [LET_DEF]; 1346 1347val lisp_inv_sub1 = prove( 1348 ``isVal x0 /\ ~(x0 = Val 0) ==> ^LISP ==> 1349 let (x0,w0) = (LISP_SUB x0 (Val 1),w0-4w) in ^LISP``, 1350 SIMP_TAC std_ss [isVal_thm,LISP_SUB_def,getVal_def] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1351 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1352 \\ REPEAT STRIP_TAC 1353 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1354 \\ Q.LIST_EXISTS_TAC [`H_DATA (INL (n2w (a - 1)))`,`s1`,`s2`,`s3`,`s4`,`s5`] 1355 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1356 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1357 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def] 1358 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 1359 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 1360 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 1361 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 1362 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1363 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 1364 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 1365 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,WORD_OR_EQ_WORD_ADD_LEMMA] 1366 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1367 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,WORD_MUL_LSL] 1368 \\ Q.PAT_X_ASSUM `x0 = Val a` (fn th => FULL_SIMP_TAC std_ss [th,SExp_11]) 1369 \\ `(a - 1) < 1073741824 /\ a < 1073741825 /\ ~(4 * a + 1 < 4)` by DECIDE_TAC 1370 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2] 1371 \\ AP_TERM_TAC \\ DECIDE_TAC) 1372 |> SIMP_RULE std_ss [LET_DEF]; 1373 1374val lisp_inv_less_lemma = prove( 1375 ``!w v:word32. ((w << 2 !! 1w) <+ (v << 2 !! 1w)) = ((w << 2) <+ (v << 2))``, 1376 REPEAT STRIP_TAC \\ blastLib.BBLAST_TAC); 1377 1378val lisp_inv_less = prove( 1379 ``isVal x0 /\ isVal x1 ==> ^LISP ==> (w0 <+ w1 = getVal x0 < getVal x1)``, 1380 SIMP_TAC std_ss [isVal_thm] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [getVal_def] 1381 \\ ASM_SIMP_TAC std_ss [lisp_inv_def,EVERY_DEF,lisp_x_def,MAP,CONS_11, 1382 ref_heap_addr_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 1383 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 1384 \\ ASM_SIMP_TAC std_ss [lisp_inv_less_lemma] 1385 \\ `(4 * a) < 4294967296 /\ (4 * a') < 4294967296` by DECIDE_TAC 1386 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_MUL_LSL,word_mul_n2w,word_lo_n2w]); 1387 1388val lisp_inv_even = prove( 1389 ``isVal x0 ==> ^LISP ==> ((w2w w0 && 4w = 0w:word64) = EVEN (getVal x0))``, 1390 SIMP_TAC std_ss [isVal_thm] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [getVal_def] 1391 \\ ASM_SIMP_TAC std_ss [lisp_inv_def,EVERY_DEF,lisp_x_def,MAP,CONS_11, 1392 ref_heap_addr_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 1393 \\ REPEAT STRIP_TAC 1394 \\ Q.PAT_X_ASSUM `w0 = dfgdf` (fn th => SIMP_TAC std_ss [th]) 1395 \\ `!w:word30. (w2w (w2w w << 2 !! 0x1w:word32) && 0x4w = 0x0w:word64) = (w && 1w = 0w)` by blastLib.BBLAST_TAC 1396 \\ POP_ASSUM (MP_TAC o Q.SPEC `n2w a`) \\ SIMP_TAC std_ss [] 1397 \\ SIMP_TAC std_ss [n2w_and_1] \\ SIMP_TAC wstd_ss [n2w_11] 1398 \\ `a MOD 2 < 2` by METIS_TAC [MOD_LESS,DECIDE ``0<2:num``] 1399 \\ `a MOD 2 < 1073741824` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [EVEN_MOD2]); 1400 1401val ref_heap_addr_alt = prove( 1402 ``(ref_heap_addr (H_ADDR a) = n2w a << 1) /\ 1403 (ref_heap_addr (H_DATA (INL w)) = w2w w << 2 + 0x1w) /\ 1404 (ref_heap_addr (H_DATA (INR v)) = w2w v << 3 + 0x3w)``, 1405 SIMP_TAC std_ss [ref_heap_addr_def] \\ blastLib.BBLAST_TAC); 1406 1407val lisp_inv_div2 = prove( 1408 ``isVal x0 ==> ^LISP ==> 1409 let (x0,w0) = (Val (getVal x0 DIV 2),(w0 >>> 3) << 2 + 1w) in ^LISP``, 1410 SIMP_TAC std_ss [isVal_thm,getVal_def] \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1411 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1412 \\ REPEAT STRIP_TAC 1413 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,TL,ZIP,EVERY_DEF,getVal_def] 1414 \\ Q.LIST_EXISTS_TAC [`H_DATA (INL (n2w (a DIV 2)))`,`s1`,`s2`,`s3`,`s4`,`s5`] 1415 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1416 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF] 1417 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_def] 1418 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 1419 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 1420 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 1421 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n,w2n_lt30] \\ REPEAT STRIP_TAC 1422 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 1423 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 1424 \\ SIMP_TAC wstd_ss [DIV_LT_X,w2n_n2w] 1425 \\ Q.PAT_X_ASSUM `xxx = w0` (ASSUME_TAC o GSYM) 1426 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def] 1427 \\ STRIP_TAC THEN1 DECIDE_TAC 1428 \\ SUBGOAL `n2w (a DIV 2) = (n2w a >>> 1):word30` 1429 \\ ASM_SIMP_TAC std_ss [] 1430 THEN1 (Q.SPEC_TAC (`(n2w a):word30`,`ww`) \\ blastLib.BBLAST_TAC) 1431 \\ ASM_SIMP_TAC std_ss [GSYM w2n_11,w2n_lsr] 1432 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,DIV_LT_X] \\ DECIDE_TAC) 1433 |> SIMP_RULE std_ss [LET_DEF]; 1434 1435val _ = save_thm("lisp_inv_add",lisp_inv_add); 1436val _ = save_thm("lisp_inv_add_nop",lisp_inv_add_nop); 1437val _ = save_thm("lisp_inv_sub",lisp_inv_sub); 1438val _ = save_thm("lisp_inv_add1",lisp_inv_add1); 1439val _ = save_thm("lisp_inv_add1_nop",lisp_inv_add1_nop); 1440val _ = save_thm("lisp_inv_sub1",lisp_inv_sub1); 1441val _ = save_thm("lisp_inv_less",lisp_inv_less); 1442val _ = save_thm("lisp_inv_even",lisp_inv_even); 1443val _ = save_thm("lisp_inv_div2",lisp_inv_div2); 1444 1445 1446(* depth limit *) 1447 1448val addr_path_def = Define ` 1449 (addr_path s [] sym m = ~isDot s) /\ 1450 (addr_path s (a::xs) sym m = 1451 lisp_x (m,sym) (H_ADDR a,s) /\ (LDEPTH s = SUC (LENGTH xs)) /\ 1452 (addr_path (CAR s) xs sym m \/ addr_path (CDR s) xs sym m))`; 1453 1454val lisp_x_IMP_addr_path = prove( 1455 ``!s a. lisp_x (m,sym) (a,s) ==> 1456 ?xs. addr_path s xs sym m /\ (LDEPTH s = LENGTH xs)``, 1457 REVERSE (Induct) \\ REPEAT STRIP_TAC 1458 THEN1 METIS_TAC [isDot_def,addr_path_def,LDEPTH_def,LENGTH] 1459 THEN1 METIS_TAC [isDot_def,addr_path_def,LDEPTH_def,LENGTH] 1460 \\ FULL_SIMP_TAC std_ss [lisp_x_def,LDEPTH_def,MAX_DEF] 1461 \\ RES_TAC \\ Q.EXISTS_TAC `k::if LDEPTH s < LDEPTH s' then xs else xs'` 1462 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ REVERSE STRIP_TAC THEN1 METIS_TAC [] 1463 \\ FULL_SIMP_TAC std_ss [addr_path_def,CAR_def,CDR_def,LDEPTH_def,MAX_DEF] 1464 \\ FULL_SIMP_TAC (srw_ss()) [lisp_x_def] \\ METIS_TAC []); 1465 1466val addr_path_APPEND = prove( 1467 ``!xs t. addr_path t (xs ++ y::ys) sym m ==> ?s2. addr_path s2 (y::ys) sym m``, 1468 Induct \\ SIMP_TAC std_ss [APPEND] THEN1 METIS_TAC [] 1469 \\ SIMP_TAC std_ss [Once addr_path_def] \\ REPEAT STRIP_TAC 1470 \\ RES_TAC \\ METIS_TAC []); 1471 1472val lisp_x11 = prove( 1473 ``!s1 s2 a. lisp_x (m,sym) (a,s1) /\ lisp_x (m,sym) (a,s2) ==> (s1 = s2)``, 1474 REVERSE Induct THEN1 1475 (SIMP_TAC std_ss [lisp_x_def] \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1476 \\ Cases_on `s2` \\ FULL_SIMP_TAC (srw_ss()) [lisp_x_def] \\ REPEAT STRIP_TAC 1477 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC [LIST_FIND_LEMMA]) 1478 THEN1 1479 (SIMP_TAC std_ss [lisp_x_def] \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1480 \\ Cases_on `s2` \\ FULL_SIMP_TAC (srw_ss()) [lisp_x_def]) 1481 \\ SIMP_TAC std_ss [lisp_x_def] \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1482 \\ Cases_on `s2` \\ FULL_SIMP_TAC (srw_ss()) [lisp_x_def] 1483 \\ STRIP_TAC \\ RES_TAC \\ ASM_SIMP_TAC std_ss []); 1484 1485val addr_path_ALL_DISTINCT = prove( 1486 ``!xs s sym m. addr_path s xs sym m ==> ALL_DISTINCT xs``, 1487 Induct \\ SIMP_TAC std_ss [ALL_DISTINCT] \\ REVERSE (REPEAT STRIP_TAC) 1488 THEN1 METIS_TAC [addr_path_def] 1489 \\ FULL_SIMP_TAC std_ss [MEM_SPLIT] 1490 \\ FULL_SIMP_TAC std_ss [] \\ Q.PAT_X_ASSUM `!s.bbb` (K ALL_TAC) 1491 \\ FULL_SIMP_TAC std_ss [addr_path_def] 1492 \\ IMP_RES_TAC addr_path_APPEND 1493 \\ FULL_SIMP_TAC std_ss [addr_path_def] 1494 \\ `s = s2` by METIS_TAC [lisp_x11] 1495 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH] \\ DECIDE_TAC); 1496 1497val addr_path_MEM = prove( 1498 ``!xs s. addr_path s xs sym m /\ MEM x xs ==> ~(m x = H_EMP)``, 1499 Induct \\ ASM_SIMP_TAC std_ss [MEM] \\ REPEAT STRIP_TAC THEN1 1500 (FULL_SIMP_TAC std_ss [addr_path_def] \\ POP_ASSUM MP_TAC 1501 \\ Cases_on `s` \\ FULL_SIMP_TAC (srw_ss()) [lisp_x_def]) 1502 \\ FULL_SIMP_TAC std_ss [addr_path_def] \\ METIS_TAC []); 1503 1504val ALL_DISTINCT_MAP_SUC = prove( 1505 ``!xs. ALL_DISTINCT xs ==> ALL_DISTINCT (MAP SUC xs)``, 1506 Induct \\ ASM_SIMP_TAC std_ss [ALL_DISTINCT,MAP,MEM_MAP]); 1507 1508val RANGE_LEMMA = prove( 1509 ``(RANGE (0,0) = {}) /\ 1510 (RANGE (0,SUC i) = i INSERT RANGE (0,i))``, 1511 SIMP_TAC std_ss [EXTENSION,IN_INSERT,NOT_IN_EMPTY] 1512 \\ SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC); 1513 1514val FINITE_RANGE = prove( 1515 ``!i. FINITE (RANGE(0,i))``, 1516 Induct \\ ASM_SIMP_TAC std_ss [RANGE_LEMMA,FINITE_EMPTY,FINITE_INSERT]); 1517 1518val CARD_RANGE = prove( 1519 ``!i. CARD (RANGE(0,i)) = i``, 1520 Induct \\ ASM_SIMP_TAC std_ss [RANGE_LEMMA,CARD_EMPTY,CARD_INSERT,FINITE_RANGE] 1521 \\ RANGE_TAC); 1522 1523val PIGEONHOLE_LEMMA = prove( 1524 ``!k xs. ALL_DISTINCT xs ==> k < LENGTH xs ==> ?i. MEM i xs /\ k <= i``, 1525 REPEAT STRIP_TAC \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] 1526 \\ `?f. INJ f (LIST_TO_SET xs) (RANGE(0,k))` by 1527 (Q.EXISTS_TAC `I` \\ SIMP_TAC std_ss [INJ_DEF] 1528 \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def,GSYM NOT_LESS] \\ METIS_TAC []) 1529 \\ `FINITE (RANGE (0,k))` by ASM_SIMP_TAC std_ss [FINITE_RANGE] 1530 \\ IMP_RES_TAC INJ_CARD 1531 \\ `CARD (LIST_TO_SET xs) = LENGTH xs` by ASM_SIMP_TAC std_ss [ALL_DISTINCT_CARD_LIST_TO_SET] 1532 \\ FULL_SIMP_TAC std_ss [CARD_RANGE] \\ DECIDE_TAC); 1533 1534val lisp_x_LDEPTH = prove( 1535 ``lisp_x (m,sym) (a,s) /\ (!i. k <= i ==> (m i = H_EMP)) ==> LDEPTH s <= k``, 1536 REPEAT STRIP_TAC 1537 \\ IMP_RES_TAC lisp_x_IMP_addr_path 1538 \\ IMP_RES_TAC addr_path_ALL_DISTINCT 1539 \\ ASM_SIMP_TAC std_ss [] 1540 \\ SIMP_TAC std_ss [GSYM NOT_LESS] 1541 \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] 1542 \\ SUBGOAL `?i. MEM i xs /\ k <= i` THEN1 METIS_TAC [addr_path_MEM] 1543 \\ METIS_TAC [PIGEONHOLE_LEMMA]); 1544 1545val lisp_inv_LDEPTH = prove( 1546 ``^LISP ==> LDEPTH x0 <= e``, 1547 STRIP_TAC \\ MATCH_MP_TAC (GEN_ALL lisp_x_LDEPTH) 1548 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,EVERY_DEF,lisp_x_def,MAP,CONS_11, 1549 ref_heap_addr_def] \\ Q.LIST_EXISTS_TAC [`INIT_SYMBOLS ++ sym`,`m`,`s0`] 1550 \\ FULL_SIMP_TAC std_ss [ok_split_heap_def] \\ REPEAT STRIP_TAC 1551 \\ Q.PAT_X_ASSUM `!k. bbb` MATCH_MP_TAC \\ DECIDE_TAC); 1552 1553val _ = save_thm("lisp_inv_LDEPTH",lisp_inv_LDEPTH); 1554 1555 1556(* ignore write to other heap half *) 1557 1558val lisp_inv_ignore_write1 = prove( 1559 ``RANGE(0,e)j ==> ^LISP ==> 1560 (let f = (bp2 + n2w (8 * j) =+ w) f in ^LISP) /\ (bp2 + n2w (8 * j)) IN df``, 1561 SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 1562 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1563 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 1564 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1565 \\ FULL_SIMP_TAC std_ss [] 1566 \\ IMP_RES_TAC ref_mem_RANGE 1567 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`(\x.H_EMP)`,`bp2`]) 1568 \\ FULL_SIMP_TAC std_ss [ref_aux_def,SEP_CLAUSES,SEP_EXISTS_THM,STAR_ASSOC] 1569 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 1570 \\ Q.LIST_EXISTS_TAC [`w`,`y`] 1571 \\ SEP_W_TAC); 1572 1573val lisp_inv_ignore_write2 = prove( 1574 ``RANGE(0,e)j ==> ^LISP ==> 1575 (let f = (bp2 + n2w (8 * j) + 4w =+ w) f in ^LISP) /\ (bp2 + n2w (8 * j) + 4w) IN df``, 1576 SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] \\ REPEAT STRIP_TAC 1577 \\ SIMP_TAC std_ss [LET_DEF,lisp_inv_def,EXISTS_OVER_CONJ] 1578 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 1579 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1580 \\ FULL_SIMP_TAC std_ss [] 1581 \\ IMP_RES_TAC ref_mem_RANGE 1582 \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`(\x.H_EMP)`,`bp2`]) 1583 \\ FULL_SIMP_TAC std_ss [ref_aux_def,SEP_CLAUSES,SEP_EXISTS_THM,STAR_ASSOC] 1584 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 1585 \\ Q.LIST_EXISTS_TAC [`x`,`w`] 1586 \\ SEP_W_TAC); 1587 1588val _ = save_thm("lisp_inv_ignore_write1",lisp_inv_ignore_write1); 1589val _ = save_thm("lisp_inv_ignore_write2",lisp_inv_ignore_write2); 1590 1591 1592(* error *) 1593 1594val gc_w2w_lemma = prove( 1595 ``!w. ((w2w:word64->word32) ((w2w:word32->word64) w) = w) /\ 1596 ((31 -- 0) ((w2w:word32->word64) w) = w2w w) /\ 1597 ((31 >< 0) bp = (w2w bp):word32) /\ 1598 ((63 >< 32) bp = (w2w (bp >>> 32)):word32) /\ 1599 (w2w ((w2w (bp >>> 32)):word32) << 32 !! w2w ((w2w bp):word32) = bp:word64)``, 1600 blastLib.BBLAST_TAC); 1601 1602val lisp_inv_error = store_thm("lisp_inv_error", 1603 ``^LISP ==> 1604 (w2w (f (sp - 0xC4w)) << 32 !! w2w (f (sp - 0xC8w)) = ex) /\ 1605 {sp - 0xC4w; sp - 0xC8w} SUBSET df /\ 1606 (sp - 0xC4w && 0x3w = 0x0w) /\ (sp - 0xC8w && 0x3w = 0x0w)``, 1607 SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,APPEND] 1608 \\ NTAC 8 (ONCE_REWRITE_TAC [ref_static_def]) \\ STRIP_TAC 1609 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,word64_3232_def,LET_DEF] 1610 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma1,SEP_CLAUSES] 1611 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3,INSERT_SUBSET,EMPTY_SUBSET] 1612 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [gc_w2w_lemma] 1613 \\ Q.PAT_X_ASSUM `sp && 0x3w = 0x0w` MP_TAC \\ blastLib.BBLAST_TAC); 1614 1615 1616(* I/O *) 1617 1618val lisp_inv_ignore_io = prove( 1619 ``!temp. ^LISP ==> let io = temp in ^LISP``, 1620 SIMP_TAC std_ss [LET_DEF,lisp_inv_def]) |> SIMP_RULE std_ss [LET_DEF]; 1621 1622val _ = save_thm("lisp_inv_ignore_io",lisp_inv_ignore_io); 1623 1624 1625(* read cs and ds, writing ds *) 1626 1627val expand_list = store_thm("expand_list", 1628 ``!cs. (LENGTH cs = 10) ==> 1629 ?c0 c1 c2 c3 c4 c5 c6 c7 c8 c9. cs = [c0;c1;c2;c3;c4;c5;c6;c7;c8;c9]``, 1630 Cases \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1631 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1632 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1633 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1634 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1635 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1636 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1637 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1638 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1639 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 1640 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11,NOT_CONS_NIL] 1641 \\ DECIDE_TAC); 1642 1643val EL_CONS = store_thm("EL_CONS", 1644 ``!n x xs. (EL n (x::xs)) = if n = 0 then x else EL (n-1) xs``, 1645 Cases \\ SIMP_TAC std_ss [EL,HD,TL,ADD1]); 1646 1647val lisp_inv_cs_read_blast = blastLib.BBLAST_PROVE 1648 ``(w2w (w1:word32) << 32 !! w2w (w2:word32) = w:word64) = 1649 (w1 = w2w (w >>> 32)) /\ (w2 = w2w w)``; 1650 1651val one_fun2set_IMP = prove( 1652 ``(one (a,x)) (fun2set (f,df)) ==> (f a = x) /\ a IN df``, 1653 REPEAT STRIP_TAC 1654 \\ IMP_RES_TAC (REWRITE_RULE [SEP_CLAUSES] (Q.SPECL [`a`,`x`,`emp`] one_fun2set))); 1655 1656val lisp_inv_cs_read = prove( 1657 ``^LISP ==> 1658 (w2w (f (sp - n2w (252 - 8 * 2))) << 32 !! w2w (f (sp - n2w (256 - 8 * 2))) = (n2w e):word64) /\ 1659 (sp - n2w (252 - 8 * 2)) IN df /\ (sp - n2w (256 - 8 * 2)) IN df /\ 1660 (w2w (f (sp - n2w (252 - 8 * 4))) << 32 !! w2w (f (sp - n2w (256 - 8 * 4))) = sa1) /\ 1661 (sp - n2w (252 - 8 * 4)) IN df /\ (sp - n2w (256 - 8 * 4)) IN df /\ 1662 (w2w (f (sp - n2w (252 - 8 * 5))) << 32 !! w2w (f (sp - n2w (256 - 8 * 5))) = sa2) /\ 1663 (sp - n2w (252 - 8 * 5)) IN df /\ (sp - n2w (256 - 8 * 5)) IN df /\ 1664 (w2w (f (sp - n2w (252 - 8 * 6))) << 32 !! w2w (f (sp - n2w (256 - 8 * 6))) = sa3) /\ 1665 (sp - n2w (252 - 8 * 6)) IN df /\ (sp - n2w (256 - 8 * 6)) IN df /\ 1666 (w2w (f (sp - n2w (188 - 8 * 0))) << 32 !! w2w (f (sp - n2w (192 - 8 * 0))) = EL 0 cs) /\ 1667 (sp - n2w (188 - 8 * 0)) IN df /\ (sp - n2w (192 - 8 * 0)) IN df /\ 1668 (w2w (f (sp - n2w (188 - 8 * 1))) << 32 !! w2w (f (sp - n2w (192 - 8 * 1))) = EL 1 cs) /\ 1669 (sp - n2w (188 - 8 * 1)) IN df /\ (sp - n2w (192 - 8 * 1)) IN df /\ 1670 (w2w (f (sp - n2w (188 - 8 * 2))) << 32 !! w2w (f (sp - n2w (192 - 8 * 2))) = EL 2 cs) /\ 1671 (sp - n2w (188 - 8 * 2)) IN df /\ (sp - n2w (192 - 8 * 2)) IN df /\ 1672 (w2w (f (sp - n2w (188 - 8 * 3))) << 32 !! w2w (f (sp - n2w (192 - 8 * 3))) = EL 3 cs) /\ 1673 (sp - n2w (188 - 8 * 3)) IN df /\ (sp - n2w (192 - 8 * 3)) IN df /\ 1674 (w2w (f (sp - n2w (188 - 8 * 4))) << 32 !! w2w (f (sp - n2w (192 - 8 * 4))) = EL 4 cs) /\ 1675 (sp - n2w (188 - 8 * 4)) IN df /\ (sp - n2w (192 - 8 * 4)) IN df /\ 1676 (w2w (f (sp - n2w (188 - 8 * 5))) << 32 !! w2w (f (sp - n2w (192 - 8 * 5))) = EL 5 cs) /\ 1677 (sp - n2w (188 - 8 * 5)) IN df /\ (sp - n2w (192 - 8 * 5)) IN df /\ 1678 (w2w (f (sp - n2w (188 - 8 * 6))) << 32 !! w2w (f (sp - n2w (192 - 8 * 6))) = EL 6 cs) /\ 1679 (sp - n2w (188 - 8 * 6)) IN df /\ (sp - n2w (192 - 8 * 6)) IN df /\ 1680 (w2w (f (sp - n2w (188 - 8 * 7))) << 32 !! w2w (f (sp - n2w (192 - 8 * 7))) = EL 7 cs) /\ 1681 (sp - n2w (188 - 8 * 7)) IN df /\ (sp - n2w (192 - 8 * 7)) IN df /\ 1682 (w2w (f (sp - n2w (188 - 8 * 8))) << 32 !! w2w (f (sp - n2w (192 - 8 * 8))) = EL 8 cs) /\ 1683 (sp - n2w (188 - 8 * 8)) IN df /\ (sp - n2w (192 - 8 * 8)) IN df /\ 1684 (w2w (f (sp - n2w (188 - 8 * 9))) << 32 !! w2w (f (sp - n2w (192 - 8 * 9))) = EL 9 cs) /\ 1685 (sp - n2w (188 - 8 * 9)) IN df /\ (sp - n2w (192 - 8 * 9)) IN df``, 1686 SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,APPEND] \\ STRIP_TAC 1687 \\ Q.PAT_X_ASSUM `LENGTH ds = 10` (K ALL_TAC) 1688 \\ IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [APPEND,EL,HD,TL,EL_CONS] 1689 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,word64_3232_def,LET_DEF,ref_static_def] 1690 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma1,SEP_CLAUSES] 1691 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3,INSERT_SUBSET,EMPTY_SUBSET] 1692 \\ FULL_SIMP_TAC std_ss [lisp_inv_cs_read_blast] 1693 \\ REPEAT (Q.PAT_X_ASSUM `(p_p * q_q) (fun2set (f_f,df_df))` 1694 (STRIP_ASSUME_TAC o MATCH_MP fun2set_STAR_IMP)) 1695 \\ IMP_RES_TAC one_fun2set_IMP \\ FULL_SIMP_TAC std_ss [DIFF_UNION] 1696 \\ FULL_SIMP_TAC std_ss [IN_DIFF]) |> SIMP_RULE std_ss []; 1697 1698val ref_static_APPEND = store_thm("ref_static_APPEND", 1699 ``!xs ys a. 1700 ref_static a (xs ++ ys) = 1701 ref_static a xs * ref_static (a + n2w (8 * LENGTH xs)) ys``, 1702 Induct \\ ASM_SIMP_TAC std_ss [APPEND,ref_static_def,SEP_CLAUSES,LENGTH, 1703 WORD_ADD_0,word64_3232_def,LET_DEF,word_arith_lemma1,MULT_CLAUSES,STAR_ASSOC]); 1704 1705val UPDATE_NTH_CONS = store_thm("UPDATE_NTH_CONS", 1706 ``UPDATE_NTH n x (y::ys) = if n = 0 then x::ys else y::UPDATE_NTH (n-1) x ys``, 1707 Cases_on `n` \\ SIMP_TAC std_ss [UPDATE_NTH_def,ADD1]); 1708 1709val lisp_inv_cs_write = prove( 1710 ``^LISP ==> 1711 (let f = ((sp - n2w (192 - 8 * 9)) =+ w2w (w:word64)) 1712 (((sp - n2w (188 - 8 * 9)) =+ w2w (w >>> 32)) f) in 1713 let cs = UPDATE_NTH 9 w cs in ^LISP) /\ 1714 (let f = ((sp - n2w (192 - 8 * 8)) =+ w2w (w:word64)) 1715 (((sp - n2w (188 - 8 * 8)) =+ w2w (w >>> 32)) f) in 1716 let cs = UPDATE_NTH 8 w cs in ^LISP) /\ 1717 (let f = ((sp - n2w (192 - 8 * 7)) =+ w2w (w:word64)) 1718 (((sp - n2w (188 - 8 * 7)) =+ w2w (w >>> 32)) f) in 1719 let cs = UPDATE_NTH 7 w cs in ^LISP) /\ 1720 (let f = ((sp - n2w (192 - 8 * 6)) =+ w2w (w:word64)) 1721 (((sp - n2w (188 - 8 * 6)) =+ w2w (w >>> 32)) f) in 1722 let cs = UPDATE_NTH 6 w cs in ^LISP) /\ 1723 (let f = ((sp - n2w (192 - 8 * 5)) =+ w2w (w:word64)) 1724 (((sp - n2w (188 - 8 * 5)) =+ w2w (w >>> 32)) f) in 1725 let cs = UPDATE_NTH 5 w cs in ^LISP) /\ 1726 (let f = ((sp - n2w (192 - 8 * 3)) =+ w2w (w:word64)) 1727 (((sp - n2w (188 - 8 * 3)) =+ w2w (w >>> 32)) f) in 1728 let cs = UPDATE_NTH 3 w cs in ^LISP)``, 1729 SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,APPEND] \\ STRIP_TAC 1730 \\ Q.PAT_X_ASSUM `LENGTH ds = 10` MP_TAC 1731 \\ IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [APPEND,EL,HD,TL,EL_CONS] 1732 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [UPDATE_NTH_CONS,LET_DEF] 1733 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,word64_3232_def,LET_DEF, 1734 ref_static_def,ref_static_APPEND] 1735 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 1736 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1737 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma1,SEP_CLAUSES] 1738 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3,INSERT_SUBSET,EMPTY_SUBSET] 1739 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,EL_CONS] 1740 \\ SEP_WRITE_TAC) 1741 |> SIMP_RULE std_ss [LET_DEF]; 1742 1743val lisp_inv_ds_read = prove( 1744 ``^LISP ==> 1745 (w2w (f (sp - n2w (108 - 8 * 0))) << 32 !! w2w (f (sp - n2w (112 - 8 * 0))) = EL 0 ds) /\ 1746 (sp - n2w (108 - 8 * 0)) IN df /\ (sp - n2w (112 - 8 * 0)) IN df /\ 1747 (w2w (f (sp - n2w (108 - 8 * 1))) << 32 !! w2w (f (sp - n2w (112 - 8 * 1))) = EL 1 ds) /\ 1748 (sp - n2w (108 - 8 * 1)) IN df /\ (sp - n2w (112 - 8 * 1)) IN df /\ 1749 (w2w (f (sp - n2w (108 - 8 * 2))) << 32 !! w2w (f (sp - n2w (112 - 8 * 2))) = EL 2 ds) /\ 1750 (sp - n2w (108 - 8 * 2)) IN df /\ (sp - n2w (112 - 8 * 2)) IN df /\ 1751 (w2w (f (sp - n2w (108 - 8 * 3))) << 32 !! w2w (f (sp - n2w (112 - 8 * 3))) = EL 3 ds) /\ 1752 (sp - n2w (108 - 8 * 3)) IN df /\ (sp - n2w (112 - 8 * 3)) IN df /\ 1753 (w2w (f (sp - n2w (108 - 8 * 4))) << 32 !! w2w (f (sp - n2w (112 - 8 * 4))) = EL 4 ds) /\ 1754 (sp - n2w (108 - 8 * 4)) IN df /\ (sp - n2w (112 - 8 * 4)) IN df /\ 1755 (w2w (f (sp - n2w (108 - 8 * 5))) << 32 !! w2w (f (sp - n2w (112 - 8 * 5))) = EL 5 ds) /\ 1756 (sp - n2w (108 - 8 * 5)) IN df /\ (sp - n2w (112 - 8 * 5)) IN df /\ 1757 (w2w (f (sp - n2w (108 - 8 * 6))) << 32 !! w2w (f (sp - n2w (112 - 8 * 6))) = EL 6 ds) /\ 1758 (sp - n2w (108 - 8 * 6)) IN df /\ (sp - n2w (112 - 8 * 6)) IN df /\ 1759 (w2w (f (sp - n2w (108 - 8 * 7))) << 32 !! w2w (f (sp - n2w (112 - 8 * 7))) = EL 7 ds) /\ 1760 (sp - n2w (108 - 8 * 7)) IN df /\ (sp - n2w (112 - 8 * 7)) IN df /\ 1761 (w2w (f (sp - n2w (108 - 8 * 8))) << 32 !! w2w (f (sp - n2w (112 - 8 * 8))) = EL 8 ds) /\ 1762 (sp - n2w (108 - 8 * 8)) IN df /\ (sp - n2w (112 - 8 * 8)) IN df /\ 1763 (w2w (f (sp - n2w (108 - 8 * 9))) << 32 !! w2w (f (sp - n2w (112 - 8 * 9))) = EL 9 ds) /\ 1764 (sp - n2w (108 - 8 * 9)) IN df /\ (sp - n2w (112 - 8 * 9)) IN df``, 1765 SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,APPEND] \\ STRIP_TAC 1766 \\ Q.PAT_X_ASSUM `LENGTH cs = 10` MP_TAC 1767 \\ IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [APPEND,EL,HD,TL,EL_CONS] 1768 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,word64_3232_def,LET_DEF, 1769 ref_static_def,ref_static_APPEND] \\ STRIP_TAC 1770 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma1,SEP_CLAUSES] 1771 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3,INSERT_SUBSET,EMPTY_SUBSET] 1772 \\ FULL_SIMP_TAC std_ss [lisp_inv_cs_read_blast] 1773 \\ Q.PAT_X_ASSUM `c1 = xxx` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [] 1774 \\ Q.PAT_X_ASSUM `n2w amnt = c9` (K ALL_TAC) 1775 \\ REPEAT (Q.PAT_X_ASSUM `(p_p * q_q) (fun2set (f_f,df_df))` 1776 (STRIP_ASSUME_TAC o MATCH_MP fun2set_STAR_IMP)) 1777 \\ IMP_RES_TAC one_fun2set_IMP \\ FULL_SIMP_TAC std_ss [DIFF_UNION] 1778 \\ FULL_SIMP_TAC std_ss [IN_DIFF]) |> SIMP_RULE std_ss []; 1779 1780val EL_LEMMA = prove( 1781 ``!x0 x1 x2 x3 x4 zs. 1782 (EL 1 (x0::x1::zs) = x1) /\ 1783 (EL 2 (x0::x1::x2::zs) = x2) /\ 1784 (EL 3 (x0::x1::x2::x3::zs) = x3) /\ 1785 (EL 4 (x0::x1::x2::x3::x4::zs) = x4)``, 1786 EVAL_TAC \\ SIMP_TAC std_ss []); 1787 1788val lisp_inv_ds_write = prove( 1789 ``^LISP ==> 1790 (let f = ((sp - n2w (112 - 8 * 0)) =+ w2w (w:word64)) 1791 (((sp - n2w (108 - 8 * 0)) =+ w2w (w >>> 32)) f) in 1792 let ds = UPDATE_NTH 0 w ds in ^LISP) /\ 1793 (let f = ((sp - n2w (108 - 8 * 0)) =+ w2w (w >>> 32)) 1794 (((sp - n2w (112 - 8 * 0)) =+ w2w (w:word64)) f) in 1795 let ds = UPDATE_NTH 0 w ds in ^LISP)``, 1796 SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,APPEND] \\ STRIP_TAC 1797 \\ Q.PAT_X_ASSUM `LENGTH cs = 10` MP_TAC 1798 \\ IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [APPEND,EL,HD,TL,EL_CONS] 1799 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [UPDATE_NTH_CONS,LET_DEF] 1800 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,word64_3232_def,LET_DEF, 1801 ref_static_def,ref_static_APPEND] 1802 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 1803 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1804 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma1,SEP_CLAUSES] 1805 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3,INSERT_SUBSET,EMPTY_SUBSET] 1806 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,EL_LEMMA,EL_CONS] 1807 \\ NTAC 7 (POP_ASSUM MP_TAC) \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1808 \\ SEP_WRITE_TAC) 1809 |> SIMP_RULE std_ss [LET_DEF]; 1810 1811val _ = save_thm("lisp_inv_cs_read",lisp_inv_cs_read); 1812val _ = save_thm("lisp_inv_ds_read",lisp_inv_ds_read); 1813val _ = save_thm("lisp_inv_cs_write",lisp_inv_cs_write); 1814val _ = save_thm("lisp_inv_ds_write",lisp_inv_ds_write); 1815 1816 1817 1818 1819(* gc is a no-op *) 1820 1821val memory_ok_EMP = prove( 1822 ``memory_ok (\x. H_EMP)``, 1823 SIMP_TAC (srw_ss()) [memory_ok_def]); 1824 1825val gc_addr_lemma1 = prove( 1826 ``!w. ((w2w ((w:word64) && 3w) = 0w:word32) = (w && 3w = 0w)) /\ 1827 ((w - 4w && 3w = 0w) = (w && 3w = 0w)) /\ 1828 ((w - 8w && 3w = 0w) = (w && 3w = 0w)) /\ 1829 ((w - 12w && 3w = 0w) = (w && 3w = 0w)) /\ 1830 ((w - 16w && 3w = 0w) = (w && 3w = 0w)) /\ 1831 ((w - 20w && 3w = 0w) = (w && 3w = 0w)) /\ 1832 ((w - 24w && 3w = 0w) = (w && 3w = 0w)) /\ 1833 ((w - 0x34w && 3w = 0w) = (w && 3w = 0w)) /\ 1834 ((w - 0x38w && 3w = 0w) = (w && 3w = 0w)) /\ 1835 ((w - 0x3Cw && 3w = 0w) = (w && 3w = 0w)) /\ 1836 ((w - 0x40w && 3w = 0w) = (w && 3w = 0w)) /\ 1837 ((w - 232w && 3w = 0w) = (w && 3w = 0w)) /\ 1838 ((w - 236w && 3w = 0w) = (w && 3w = 0w)) /\ 1839 ((w - 228w && 3w = 0w) = (w && 3w = 0w)) /\ 1840 ((w - 240w && 3w = 0w) = (w && 3w = 0w)) /\ 1841 (((v + 4w * w) && 3w = 0w) = (v && 3w = 0w))``, 1842 REPEAT STRIP_TAC \\ blastLib.BBLAST_TAC); 1843 1844val gc_addr_lemma = prove( 1845 ``((sp + 0x4w * wsp - 0x18w && 0x3w = 0x0w:word64)) = (sp && 3w = 0w)``, 1846 SIMP_TAC std_ss [gc_addr_lemma1]); 1847 1848val LENGTH_ADDR_MAP = prove( 1849 ``!xs. LENGTH (ADDR_MAP f xs) = LENGTH xs``, 1850 Induct \\ REPEAT Cases \\ ASM_SIMP_TAC std_ss [ADDR_MAP_def,LENGTH]); 1851 1852val EVERY_IMP_EVERY = prove( 1853 ``(LENGTH xs = LENGTH ys) /\ (LENGTH zs = LENGTH xs) /\ (LENGTH zs = LENGTH ys) /\ 1854 (!k. k < LENGTH xs ==> P (EL k xs,EL k zs) ==> Q (EL k ys,EL k zs)) ==> 1855 ((EVERY P (ZIP(xs,zs))) ==> (EVERY Q (ZIP(ys,zs))))``, 1856 FULL_SIMP_TAC std_ss [EVERY_EL,LENGTH_ZIP,EL_ZIP]); 1857 1858val lisp_inv_gc_blast = prove( 1859 ``!w v. (w2w w = (w2w v):word64) = (w = v:word32)``, 1860 blastLib.BBLAST_TAC); 1861 1862val STATIC = find_term (can (match_term ``ref_static x y``)) 1863 (concl (RW [ref_full_stack_def] lisp_inv_def)) 1864 1865val STATIC2 = subst [``bp2:word64``|->``bp:word64``] STATIC; 1866 1867val lisp_inv_gc = prove( 1868 ``^LISP ==> 1869 ?wsp' w0' w1' w2' w3' w4' w5' wi' we' f'. 1870 mc_full_gc_pre (wsp,bp,sp,w2w w0,w2w w1,w2w w2,w2w w3,w2w w4,w2w w5,wi,df,f) /\ 1871 (mc_full_gc (wsp,bp,sp,w2w w0,w2w w1,w2w w2,w2w w3,w2w w4,w2w w5,wi,df,f) = 1872 (wsp',bp2,sp,w2w w0',w2w w1',w2w w2',w2w w3',w2w w4',w2w w5',wi',we',df,f')) /\ 1873 let (wsp,bp,w0,w1,w2,w3,w4,w5,wi,we,f,bp2) = 1874 (wsp',bp2,w0',w1',w2',w3',w4',w5',wi',we',f',bp) in 1875 ^LISP``, 1876 STRIP_TAC 1877 \\ SIMP_TAC std_ss [mc_full_gc_def,mc_full_gc_pre_def,gc_w2w_lemma] 1878 \\ POP_ASSUM (MP_TAC o RW [lisp_inv_def,ref_full_stack_def]) \\ STRIP_TAC 1879 \\ `w2w (f (sp - 228w)) << 32 !! w2w (f (sp - 232w)) = bp2` by 1880 (NTAC 3 (POP_ASSUM MP_TAC) \\ SIMP_TAC std_ss [APPEND] 1881 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) \\ REPEAT STRIP_TAC 1882 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,word64_3232_def,LET_DEF] 1883 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma1,SEP_CLAUSES] 1884 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3] 1885 \\ REPEAT STRIP_TAC \\ SEP_R_TAC 1886 \\ FULL_SIMP_TAC std_ss [gc_w2w_lemma]) 1887 \\ ASM_SIMP_TAC std_ss [LET_DEF,word_arith_lemma3] 1888 \\ Q.ABBREV_TAC `f5 = (0x4w * wsp + sp - 0x4w =+ w5) 1889 ((0x4w * wsp + sp - 0x8w =+ w4) 1890 ((0x4w * wsp + sp - 0xCw =+ w3) 1891 ((0x4w * wsp + sp - 0x10w =+ w2) 1892 ((0x4w * wsp + sp - 0x14w =+ w1) 1893 ((0x4w * wsp + sp - 0x18w =+ w0) f)))))` 1894 \\ SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,GSYM CONJ_ASSOC] 1895 \\ `(ref_mem bp m 0 e * ref_mem bp2 (\x. H_EMP) 0 e * 1896 ref_stack (sp + 0x4w * wsp - 0x18w) (s0::s1::s2::s3::s4::s5::ss++ss1) * 1897 ref_stack_space (sp + 0x4w * wsp - 0x18w) (w2n wsp) * 1898 ref_stack_space_above (sp + 4w * wsp + n2w (4 * LENGTH (ss ++ ss1))) 1899 (sl1 - LENGTH ss1) * ^STATIC) (fun2set (f5,df)) /\ 1900 0x4w * wsp + sp - 0x18w IN df /\ 1901 0x4w * wsp + sp - 0x14w IN df /\ 1902 0x4w * wsp + sp - 0x10w IN df /\ 1903 0x4w * wsp + sp - 0xCw IN df /\ 1904 0x4w * wsp + sp - 0x8w IN df /\ 1905 0x4w * wsp + sp - 0x4w IN df` by 1906 (Q.PAT_X_ASSUM `MAP ref_heap_addr xxx = yyy` (ASSUME_TAC o GSYM) 1907 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,ref_stack_def,word_arith_lemma1,APPEND] 1908 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,STAR_ASSOC] 1909 \\ Q.UNABBREV_TAC `f5` 1910 \\ FULL_SIMP_TAC bool_ss [DECIDE ``n+6 = SUC (SUC (SUC (SUC (SUC (SUC n)))))``] 1911 \\ FULL_SIMP_TAC std_ss [ref_stack_space_def,word_arith_lemma1,STAR_ASSOC] 1912 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,SEP_EXISTS_THM,WORD_ADD_0] 1913 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1914 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 1915 \\ ASM_SIMP_TAC std_ss [] 1916 \\ ASSUME_TAC (GEN_ALL mc_gc_thm) 1917 \\ SEP_I_TAC "mc_gc" 1918 \\ FULL_SIMP_TAC std_ss [ok_split_heap] 1919 \\ IMP_RES_TAC split_gc_thm 1920 \\ FULL_SIMP_TAC std_ss [APPEND] 1921 \\ Q.PAT_X_ASSUM `split_gc xxx = yyy` MP_TAC 1922 \\ SEP_I_TAC "split_gc" 1923 \\ STRIP_TAC 1924 \\ Q.PAT_X_ASSUM `!xs2. bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] 1925 \\ Q.ABBREV_TAC `XX = ref_stack_space_above (sp + 4w * wsp + n2w (4 * LENGTH (ss ++ ss1))) (sl1 - LENGTH ss1)` 1926 \\ STRIP_TAC 1927 \\ POP_ASSUM (MP_TAC o Q.SPEC `^STATIC * ref_stack_space (sp + 0x4w * wsp - 0x18w) (w2n wsp) * XX`) 1928 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_ASSOC WORD_ADD_COMM,memory_ok_EMP,APPEND] 1929 \\ FULL_SIMP_TAC std_ss [gc_addr_lemma] \\ STRIP_TAC 1930 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 1931 \\ SIMP_TAC std_ss [gc_w2w_lemma] 1932 \\ Q.ABBREV_TAC `fj = (sp - 228w =+ w2w (bp >>> 32)) ((sp - 232w =+ w2w bp) fi)` 1933 \\ `(ref_mem bp2 m2 0 e * ref_mem bp (\x. H_EMP) 0 e * 1934 ref_stack (sp + 0x4w * wsp - 0x18w) roots2 * 1935 ref_stack_space (sp + 0x4w * wsp - 0x18w) (w2n wsp) * XX * 1936 ^STATIC2) (fun2set (fj,df))` by 1937 (FULL_SIMP_TAC std_ss [ref_static_def,word64_3232_def,LET_DEF,STAR_ASSOC,APPEND] 1938 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,SEP_CLAUSES] 1939 \\ Q.UNABBREV_TAC `fj` \\ FULL_SIMP_TAC std_ss [gc_w2w_lemma] 1940 \\ SEP_WRITE_TAC) 1941 \\ ASM_SIMP_TAC std_ss [lisp_inv_gc_blast] 1942 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 1943 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC) 1944 \\ Q.PAT_X_ASSUM `xxx (fun2set (fi,df))` (K ALL_TAC) 1945 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` (K ALL_TAC) 1946 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [APPEND] 1947 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) 1948 \\ FULL_SIMP_TAC std_ss [word64_3232_def,LET_DEF,STAR_ASSOC] 1949 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] \\ STRIP_TAC \\ SEP_R_TAC 1950 \\ ASM_SIMP_TAC std_ss [gc_addr_lemma1]) 1951 \\ `w2w (fj (sp - 236w)) << 32 !! w2w (fj (sp - 240w)) = (n2w e):word64` by 1952 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC) 1953 \\ Q.PAT_X_ASSUM `xxx (fun2set (fi,df))` (K ALL_TAC) 1954 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` (K ALL_TAC) 1955 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [APPEND] 1956 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) 1957 \\ FULL_SIMP_TAC std_ss [word64_3232_def,LET_DEF,STAR_ASSOC] 1958 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] \\ STRIP_TAC \\ SEP_R_TAC 1959 \\ FULL_SIMP_TAC std_ss [gc_w2w_lemma]) 1960 \\ ASM_SIMP_TAC std_ss [] 1961 \\ `LENGTH roots2 = LENGTH (s0::s1::s2::s3::s4::s5::(ss++ss1))` by 1962 (FULL_SIMP_TAC std_ss [gc_exec_def,gc_copy_def,gc_filter_def,LENGTH_ADDR_MAP]) 1963 \\ `?r0 r1 r2 r3 r4 r5 rs. roots2 = r0::r1::r2::r3::r4::r5::rs` by 1964 (Cases_on `roots2` THEN1 FULL_SIMP_TAC std_ss [LENGTH,ADD1] 1965 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 1966 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 1967 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 1968 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 1969 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 1970 \\ FULL_SIMP_TAC std_ss [CONS_11]) 1971 \\ FULL_SIMP_TAC std_ss [] 1972 \\ Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC) 1973 \\ Q.PAT_X_ASSUM `xxx (fun2set (fi,df))` (K ALL_TAC) 1974 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` (K ALL_TAC) 1975 \\ Q.PAT_X_ASSUM `Abbrev (xxx = (zz =+ yy) ff)` (K ALL_TAC) 1976 \\ Q.PAT_X_ASSUM `Abbrev (xxx = (zz =+ yy) ff)` (K ALL_TAC) 1977 \\ FULL_SIMP_TAC std_ss [ref_stack_def,word_arith_lemma3,STAR_ASSOC] 1978 \\ `fj (sp + 0x4w * wsp - 0x18w) = ref_heap_addr r0` by SEP_READ_TAC 1979 \\ `fj (sp + 0x4w * wsp - 0x14w) = ref_heap_addr r1` by SEP_READ_TAC 1980 \\ `fj (sp + 0x4w * wsp - 0x10w) = ref_heap_addr r2` by SEP_READ_TAC 1981 \\ `fj (sp + 0x4w * wsp - 0xCw) = ref_heap_addr r3` by SEP_READ_TAC 1982 \\ `fj (sp + 0x4w * wsp - 0x8w) = ref_heap_addr r4` by SEP_READ_TAC 1983 \\ `fj (sp + 0x4w * wsp - 0x4w) = ref_heap_addr r5` by SEP_READ_TAC 1984 \\ ASM_SIMP_TAC std_ss [] 1985 \\ `(ref_mem bp2 m2 0 e * ref_mem bp (\x. H_EMP) 0 e * 1986 ref_stack (sp + 0x4w * wsp) rs * 1987 ref_stack_space (sp + 0x4w * wsp) (w2n wsp + 6) * XX * 1988 ^STATIC2) (fun2set (fj,df))` by 1989 (FULL_SIMP_TAC bool_ss [DECIDE ``n+6 = SUC (SUC (SUC (SUC (SUC (SUC n)))))``] 1990 \\ FULL_SIMP_TAC std_ss [ref_stack_space_def,word_arith_lemma1,STAR_ASSOC] 1991 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,SEP_EXISTS_THM,WORD_ADD_0] 1992 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1993 \\ Q.LIST_EXISTS_TAC [`ref_heap_addr r5`,`ref_heap_addr r4`,`ref_heap_addr r3`, 1994 `ref_heap_addr r2`,`ref_heap_addr r1`,`ref_heap_addr r0`] 1995 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1996 \\ SIMP_TAC std_ss [lisp_inv_def] 1997 \\ Q.LIST_EXISTS_TAC [`r0`,`r1`,`r2`,`r3`,`r4`,`r5`] 1998 \\ Q.LIST_EXISTS_TAC [`m2`,`i2`,`TAKE (LENGTH ss) rs`,`DROP (LENGTH ss) rs`,`sym`,`~b`] 1999 \\ ASM_SIMP_TAC std_ss [MAP,APPEND,ref_full_stack_def,STAR_ASSOC] 2000 \\ FULL_SIMP_TAC std_ss [LENGTH,TAKE_DROP] 2001 \\ `ok_split_heap (r0::r1::r2::r3::r4::r5::rs,m2,i2,e)` by 2002 (FULL_SIMP_TAC std_ss [ok_split_heap] \\ METIS_TAC []) 2003 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [APPEND,LENGTH_APPEND] 2004 \\ `LENGTH ss <= LENGTH rs` by DECIDE_TAC 2005 \\ ASM_SIMP_TAC std_ss [LENGTH_TAKE,LENGTH_DROP] 2006 \\ Q.UNABBREV_TAC `XX` \\ FULL_SIMP_TAC (std_ss++star_ss) [WORD_ADD_ASSOC] 2007 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ REVERSE STRIP_TAC 2008 THEN1 (Cases_on `b` \\ FULL_SIMP_TAC std_ss []) 2009 \\ `i2 <= e` by (FULL_SIMP_TAC std_ss [ok_split_heap_def]) 2010 \\ ASM_SIMP_TAC std_ss [word_add_n2w,DECIDE ``2*n = n+n:num``] 2011 \\ Q.PAT_X_ASSUM `EVERY xxx yyy` MP_TAC 2012 \\ SIMP_TAC std_ss [GSYM ZIP] 2013 \\ MATCH_MP_TAC EVERY_IMP_EVERY 2014 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC 2015 THEN1 (FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND]) 2016 \\ NTAC 2 STRIP_TAC 2017 \\ MATCH_MP_TAC (Q.INST [`c2`|->`T`] lisp_x_gc_thm) 2018 \\ ASM_SIMP_TAC std_ss []) |> SIMP_RULE std_ss [LET_DEF]; 2019 2020(* -- generational version 2021 2022val align_blast = blastLib.BBLAST_PROVE 2023 ``(a && 3w = 0w) ==> ((a - w && 3w = 0w) = (w && 3w = 0w:word64)) /\ 2024 ((a + w && 3w = 0w) = (w && 3w = 0w:word64))`` 2025 2026val lisp_inv_gc = prove( 2027 ``^LISP ==> 2028 ?wsp' w0' w1' w2' w3' w4' w5' wi' we' f'. 2029 mc_full_gc_pre (tw0,wsp,bp,sp,w2w w0,w2w w1,w2w w2,w2w w3,w2w w4,w2w w5,wi,df,f) /\ 2030 (mc_full_gc (tw0,wsp,bp,sp,w2w w0,w2w w1,w2w w2,w2w w3,w2w w4,w2w w5,wi,df,f) = 2031 (tw0,wsp',bp,sp,w2w w0',w2w w1',w2w w2',w2w w3',w2w w4',w2w w5',wi',we',df,f')) /\ 2032 let (wsp,w0,w1,w2,w3,w4,w5,wi,we,f) = 2033 (wsp',w0',w1',w2',w3',w4',w5',wi',we',f') in 2034 ^LISP``, 2035 STRIP_TAC 2036 \\ STRIP_ASSUME_TAC (split_after (3*5) (CONJUNCTS (UNDISCH lisp_inv_ds_read)) |> snd |> 2037 split_after 3 |> fst |> LIST_CONJ) 2038 \\ SIMP_TAC std_ss [mc_full_gc_def,mc_full_gc_pre_def,gc_w2w_lemma] 2039 \\ NTAC 3 (POP_ASSUM MP_TAC) 2040 \\ POP_ASSUM (MP_TAC o RW [lisp_inv_def,ref_full_stack_def]) \\ STRIP_TAC 2041 \\ `w2w (f (sp - 228w)) << 32 !! w2w (f (sp - 232w)) = bp2` by 2042 (NTAC 3 (POP_ASSUM MP_TAC) \\ SIMP_TAC std_ss [APPEND] 2043 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) \\ REPEAT STRIP_TAC 2044 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,word64_3232_def,LET_DEF] 2045 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma1,SEP_CLAUSES] 2046 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3] 2047 \\ REPEAT STRIP_TAC \\ SEP_R_TAC 2048 \\ FULL_SIMP_TAC std_ss [gc_w2w_lemma]) 2049 \\ ASM_SIMP_TAC std_ss [LET_DEF,word_arith_lemma3] 2050 \\ Q.ABBREV_TAC `f5 = (0x4w * wsp + sp - 0x4w =+ w5) 2051 ((0x4w * wsp + sp - 0x8w =+ w4) 2052 ((0x4w * wsp + sp - 0xCw =+ w3) 2053 ((0x4w * wsp + sp - 0x10w =+ w2) 2054 ((0x4w * wsp + sp - 0x14w =+ w1) 2055 ((0x4w * wsp + sp - 0x18w =+ w0) f)))))` 2056 \\ SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,GSYM CONJ_ASSOC] 2057 \\ `(ref_mem bp m 0 e * ref_mem bp2 (\x. H_EMP) 0 e * 2058 ref_stack (sp + 0x4w * wsp - 0x18w) (s0::s1::s2::s3::s4::s5::ss++ss1) * 2059 ref_stack_space (sp + 0x4w * wsp - 0x18w) (w2n wsp) * 2060 ref_stack_space_above (sp + 4w * wsp + n2w (4 * LENGTH (ss ++ ss1))) 2061 (sl1 - LENGTH ss1) * ^STATIC) (fun2set (f5,df)) /\ 2062 0x4w * wsp + sp - 0x18w IN df /\ 2063 0x4w * wsp + sp - 0x14w IN df /\ 2064 0x4w * wsp + sp - 0x10w IN df /\ 2065 0x4w * wsp + sp - 0xCw IN df /\ 2066 0x4w * wsp + sp - 0x8w IN df /\ 2067 0x4w * wsp + sp - 0x4w IN df` by 2068 (Q.PAT_X_ASSUM `MAP ref_heap_addr xxx = yyy` (ASSUME_TAC o GSYM) 2069 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,ref_stack_def,word_arith_lemma1,APPEND] 2070 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,STAR_ASSOC] 2071 \\ Q.UNABBREV_TAC `f5` 2072 \\ FULL_SIMP_TAC bool_ss [DECIDE ``n+6 = SUC (SUC (SUC (SUC (SUC (SUC n)))))``] 2073 \\ FULL_SIMP_TAC std_ss [ref_stack_space_def,word_arith_lemma1,STAR_ASSOC] 2074 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,SEP_EXISTS_THM,WORD_ADD_0] 2075 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 2076 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 2077 \\ ASM_SIMP_TAC std_ss [] 2078 \\ ASSUME_TAC (GEN_ALL mc_gen_gc_thm) 2079 \\ `?l. (EL 5 ds = n2w l) /\ l <= e` by 2080 (Cases_on `EL 5 ds` \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] \\ METIS_TAC []) 2081 \\ FULL_SIMP_TAC std_ss [word_add_n2w,DECIDE ``l+l=2*l:num``] 2082 \\ SEP_I_TAC "mc_gen_gc" 2083 \\ FULL_SIMP_TAC std_ss [ok_split_heap] 2084 \\ IMP_RES_TAC gen_gc_thm 2085 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `l`) 2086 \\ FULL_SIMP_TAC std_ss [APPEND] 2087 \\ Q.PAT_X_ASSUM `gen_gc xxx = yyy` MP_TAC 2088 \\ SEP_I_TAC "gen_gc" 2089 \\ STRIP_TAC 2090 \\ Q.PAT_X_ASSUM `!xs2. bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [] 2091 \\ Q.ABBREV_TAC `XX = ref_stack_space_above (sp + 4w * wsp + n2w (4 * LENGTH (ss ++ ss1))) (sl1 - LENGTH ss1)` 2092 \\ STRIP_TAC 2093 \\ POP_ASSUM (MP_TAC o Q.SPEC `^STATIC * ref_stack_space (sp + 0x4w * wsp - 0x18w) (w2n wsp) * XX`) 2094 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_ASSOC WORD_ADD_COMM,memory_ok_EMP,APPEND] 2095 \\ FULL_SIMP_TAC std_ss [gc_addr_lemma] \\ STRIP_TAC 2096 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 2097 \\ SIMP_TAC std_ss [gc_w2w_lemma] 2098 \\ REPEAT STRIP_TAC 2099 \\ ASM_SIMP_TAC std_ss [lisp_inv_gc_blast] 2100 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 2101 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC) 2102 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` (K ALL_TAC) 2103 \\ NTAC 4 (POP_ASSUM MP_TAC) \\ FULL_SIMP_TAC std_ss [APPEND] 2104 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) 2105 \\ FULL_SIMP_TAC std_ss [word64_3232_def,LET_DEF,STAR_ASSOC] 2106 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] \\ NTAC 4 STRIP_TAC \\ SEP_R_TAC 2107 \\ ASM_SIMP_TAC std_ss [gc_addr_lemma1,align_blast] 2108 \\ ASM_SIMP_TAC std_ss [n2w_and_3]) 2109 \\ `w2w (fi (sp - 236w)) << 32 !! w2w (fi (sp - 240w)) = (n2w e):word64` by 2110 (Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC) 2111 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` (K ALL_TAC) 2112 \\ NTAC 4 (POP_ASSUM MP_TAC) \\ FULL_SIMP_TAC std_ss [APPEND] 2113 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) 2114 \\ FULL_SIMP_TAC std_ss [word64_3232_def,LET_DEF,STAR_ASSOC] 2115 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] \\ STRIP_TAC \\ SEP_R_TAC 2116 \\ FULL_SIMP_TAC std_ss [gc_w2w_lemma]) 2117 \\ ASM_SIMP_TAC std_ss [] 2118 \\ `LENGTH roots2 = LENGTH (s0::s1::s2::s3::s4::s5::(ss++ss1))` by 2119 (FULL_SIMP_TAC std_ss [weak_gc_exec_def] \\ Cases_on `z` 2120 \\ FULL_SIMP_TAC std_ss [weak_gc_copy_def,weak_gc_filter_def,LENGTH_ADDR_MAP]) 2121 \\ `?r0 r1 r2 r3 r4 r5 rs. roots2 = r0::r1::r2::r3::r4::r5::rs` by 2122 (Cases_on `roots2` THEN1 FULL_SIMP_TAC std_ss [LENGTH,ADD1] 2123 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 2124 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 2125 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 2126 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 2127 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 2128 \\ FULL_SIMP_TAC std_ss [CONS_11]) 2129 \\ FULL_SIMP_TAC std_ss [] 2130 \\ Q.PAT_X_ASSUM `xxx (fun2set (f5,df))` (K ALL_TAC) 2131 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` (K ALL_TAC) 2132 \\ Q.PAT_X_ASSUM `Abbrev (xxx = (zz =+ yy) ff)` (K ALL_TAC) 2133 \\ FULL_SIMP_TAC std_ss [ref_stack_def,word_arith_lemma3,STAR_ASSOC] 2134 \\ `fi (sp + 0x4w * wsp - 0x18w) = ref_heap_addr r0` by SEP_READ_TAC 2135 \\ `fi (sp + 0x4w * wsp - 0x14w) = ref_heap_addr r1` by SEP_READ_TAC 2136 \\ `fi (sp + 0x4w * wsp - 0x10w) = ref_heap_addr r2` by SEP_READ_TAC 2137 \\ `fi (sp + 0x4w * wsp - 0xCw) = ref_heap_addr r3` by SEP_READ_TAC 2138 \\ `fi (sp + 0x4w * wsp - 0x8w) = ref_heap_addr r4` by SEP_READ_TAC 2139 \\ `fi (sp + 0x4w * wsp - 0x4w) = ref_heap_addr r5` by SEP_READ_TAC 2140 \\ ASM_SIMP_TAC std_ss [] 2141 \\ `(ref_mem bp m2 0 e * ref_mem bp2 (\x. H_EMP) 0 e * 2142 ref_stack (sp + 0x4w * wsp) rs * 2143 ref_stack_space (sp + 0x4w * wsp) (w2n wsp + 6) * XX * 2144 ^STATIC) (fun2set (fi,df))` by 2145 (FULL_SIMP_TAC bool_ss [DECIDE ``n+6 = SUC (SUC (SUC (SUC (SUC (SUC n)))))``] 2146 \\ FULL_SIMP_TAC std_ss [ref_stack_space_def,word_arith_lemma1,STAR_ASSOC] 2147 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,SEP_EXISTS_THM,WORD_ADD_0] 2148 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 2149 \\ Q.LIST_EXISTS_TAC [`ref_heap_addr r5`,`ref_heap_addr r4`,`ref_heap_addr r3`, 2150 `ref_heap_addr r2`,`ref_heap_addr r1`,`ref_heap_addr r0`] 2151 \\ FULL_SIMP_TAC (std_ss++star_ss) [APPEND]) 2152 \\ SIMP_TAC std_ss [lisp_inv_def] 2153 \\ Q.LIST_EXISTS_TAC [`r0`,`r1`,`r2`,`r3`,`r4`,`r5`] 2154 \\ Q.LIST_EXISTS_TAC [`m2`,`i2`,`TAKE (LENGTH ss) rs`,`DROP (LENGTH ss) rs`,`sym`,`b`] 2155 \\ ASM_SIMP_TAC std_ss [MAP,APPEND,ref_full_stack_def,STAR_ASSOC] 2156 \\ FULL_SIMP_TAC std_ss [LENGTH,TAKE_DROP] 2157 \\ `ok_split_heap (r0::r1::r2::r3::r4::r5::rs,m2,i2,e)` by 2158 (FULL_SIMP_TAC std_ss [ok_split_heap] \\ METIS_TAC []) 2159 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [APPEND,LENGTH_APPEND] 2160 \\ `LENGTH ss <= LENGTH rs` by DECIDE_TAC 2161 \\ ASM_SIMP_TAC std_ss [LENGTH_TAKE,LENGTH_DROP] 2162 \\ Q.UNABBREV_TAC `XX` \\ FULL_SIMP_TAC (std_ss++star_ss) [WORD_ADD_ASSOC] 2163 \\ SIMP_TAC std_ss [CONJ_ASSOC] 2164 \\ `i2 <= e` by (FULL_SIMP_TAC std_ss [ok_split_heap_def]) 2165 \\ ASM_SIMP_TAC std_ss [word_add_n2w,DECIDE ``2*n = n+n:num``] 2166 \\ Q.PAT_X_ASSUM `EVERY xxx yyy` MP_TAC 2167 \\ SIMP_TAC std_ss [GSYM ZIP] 2168 \\ MATCH_MP_TAC EVERY_IMP_EVERY 2169 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC 2170 THEN1 (FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND]) 2171 \\ NTAC 2 STRIP_TAC 2172 \\ MATCH_MP_TAC (Q.INST [`c2`|->`T`] lisp_x_gc_thm) 2173 \\ ASM_SIMP_TAC std_ss []) |> SIMP_RULE std_ss [LET_DEF]; 2174 2175*) 2176 2177 2178val _ = save_thm("lisp_inv_gc",lisp_inv_gc); 2179 2180 2181(* temp string *) 2182 2183val lisp_inv_temp_string = prove( 2184 ``!n str2. 2185 ^LISP ==> n <= 520 ==> 2186 ?str p. (LENGTH str = n) /\ 2187 ((one_byte_list sa2 str * p) (fun2set (g,dg))) /\ 2188 !g2. ((one_byte_list sa2 str2 * p) (fun2set (g2,dg))) /\ 2189 (LENGTH str2 = n) ==> let g = g2 in ^LISP``, 2190 STRIP_TAC \\ STRIP_TAC 2191 \\ SIMP_TAC std_ss [lisp_inv_def,symtable_inv_def,one_symbol_list_def, 2192 SEP_EXISTS_THM,cond_STAR] \\ REPEAT STRIP_TAC 2193 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND] 2194 \\ `n <= LENGTH ys` by DECIDE_TAC 2195 \\ MP_TAC (Q.SPEC `n` (Q.ISPEC `ys:word8 list` SPLIT_LIST_LESS_EQ)) 2196 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 2197 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND] 2198 \\ Q.EXISTS_TAC `xs1'` \\ ASM_SIMP_TAC std_ss [] 2199 \\ Q.EXISTS_TAC `one_byte_list sa1 (symbol_list (INIT_SYMBOLS ++ sym)) * 2200 one_byte_list 2201 (sa1 + n2w (LENGTH (symbol_list (INIT_SYMBOLS ++ sym))) + 2202 n2w n) xs2` 2203 \\ FULL_SIMP_TAC (std_ss++star_ss) [LET_DEF] 2204 \\ REPEAT STRIP_TAC 2205 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 2206 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 2207 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `str2 ++ xs2` 2208 \\ FULL_SIMP_TAC (std_ss++star_ss) [LET_DEF,one_byte_list_APPEND] 2209 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND]) |> SIMP_RULE std_ss [LET_DEF]; 2210 2211val _ = save_thm("lisp_inv_temp_string",lisp_inv_temp_string); 2212 2213 2214(* load value of amnt *) 2215 2216val align_blast = blastLib.BBLAST_PROVE 2217 ``(a && 3w = 0w) ==> ((a - w && 3w = 0w) = (w && 3w = 0w:word64))`` 2218 2219val lisp_inv_amnt_read = prove( 2220 ``^LISP ==> 2221 (let (x0,w0) = (Val amnt, w2w (4w * (w2w (f (sp - 0x24w)) << 32 !! (w2w:word32->word64) (f (sp - 0x28w))) + 1w)) in ^LISP) /\ 2222 (sp - 0x24w) IN df /\ (sp - 0x28w) IN df /\ 2223 (sp - 0x24w && 3w = 0w) /\ (sp - 0x28w && 3w = 0w)``, 2224 SIMP_TAC std_ss [LET_DEF] \\ STRIP_TAC \\ IMP_RES_TAC lisp_inv_ds_read 2225 \\ `sp && 3w = 0w`by FULL_SIMP_TAC std_ss [lisp_inv_def] 2226 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 2227 \\ `(EL 9 ds = n2w amnt) /\ amnt < 2**30` by (FULL_SIMP_TAC std_ss [lisp_inv_def]) 2228 \\ ASM_SIMP_TAC std_ss [] 2229 \\ SIMP_TAC std_ss [w2w_def,WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 2230 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 2231 \\ `(4 * amnt + 1) < 18446744073709551616` by DECIDE_TAC 2232 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 2233 \\ MATCH_MP_TAC lisp_inv_Val_n2w \\ ASM_SIMP_TAC std_ss []) 2234 |> SIMP_RULE std_ss [LET_DEF]; 2235 2236val _ = save_thm("lisp_inv_amnt_read",lisp_inv_amnt_read); 2237 2238 2239(* load based on xbp *) 2240 2241val BLAST_LEMMA = prove(``w << 2 !! 1w = w << 2 + 1w:word32``,blastLib.BBLAST_TAC); 2242 2243val lisp_inv_xbp_load = prove( 2244 ``^LISP ==> isVal x1 /\ getVal x1 < xbp /\ xbp <= LENGTH xs ==> 2245 let wa = (w2w (f (sp - n2w (108 - 8 * 1))) << 32 !! w2w (f (sp - n2w (112 - 8 * 1)))) in 2246 let wb = wa + w2w w1 in 2247 (let (x4,w4,tw2) = (EL ((LENGTH xs + getVal x1) - xbp) xs,f wb,wa) in ^LISP) /\ 2248 wb IN df /\ (wb && 0x3w = 0x0w) /\ 2249 (sp - n2w (108 - 8 * 1)) IN df /\ ((sp - n2w (108 - 8 * 1) && 3w = 0w)) /\ 2250 (sp - n2w (112 - 8 * 1)) IN df /\ ((sp - n2w (112 - 8 * 1) && 3w = 0w))``, 2251 Cases_on `isVal x1` \\ FULL_SIMP_TAC std_ss [LET_DEF] 2252 \\ FULL_SIMP_TAC std_ss [isVal_thm,getVal_def] \\ STRIP_TAC 2253 \\ IMP_RES_TAC lisp_inv_ds_read \\ ASM_SIMP_TAC std_ss [] 2254 \\ Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2255 \\ NTAC 2 STRIP_TAC 2256 \\ Q.ABBREV_TAC `n = LENGTH xs + a - xbp` 2257 \\ `EL 1 ds + w2w w1 = sp + 0x4w * wsp + 0x4w * n2w n` by 2258 (FULL_SIMP_TAC std_ss [lisp_inv_def,MAP,CONS_11,EVERY_DEF,lisp_x_def] 2259 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (MP_TAC o GSYM) 2260 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,BLAST_LEMMA] 2261 \\ REPEAT STRIP_TAC 2262 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,WORD_MUL_LSL] 2263 \\ `(4 * a + 1) < 4294967296` by DECIDE_TAC 2264 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w] 2265 \\ ONCE_REWRITE_TAC [ADD_COMM] 2266 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_ADD,WORD_ADD_ASSOC] 2267 \\ ASM_SIMP_TAC std_ss [word_arith_lemma3] 2268 \\ Q.PAT_X_ASSUM `LENGTH ss + w2n wsp = sl` (MP_TAC o GSYM) 2269 \\ ASM_SIMP_TAC std_ss [] \\ Q.SPEC_TAC (`wsp`,`w`) 2270 \\ Cases \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,word_mul_n2w,w2n_n2w] 2271 \\ `~(4 * (LENGTH ss + n') < 4 * xbp - 4 * a)` by DECIDE_TAC 2272 \\ ASM_SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL,word_arith_lemma4] 2273 \\ REPEAT STRIP_TAC \\ AP_TERM_TAC \\ Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 2274 \\ ASM_SIMP_TAC std_ss [] 2275 \\ `n < LENGTH xs` by (Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 2276 \\ IMP_RES_TAC lisp_inv_swap4 2277 \\ IMP_RES_TAC (RW[AND_IMP_INTRO]lisp_inv_load_lemma) 2278 \\ ASM_SIMP_TAC std_ss [] 2279 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2280 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3] 2281 \\ MATCH_MP_TAC lisp_inv_swap4 2282 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ ASM_SIMP_TAC std_ss [] 2283 \\ Q.EXISTS_TAC `tw2` \\ ASM_SIMP_TAC std_ss []) 2284 |> SIMP_RULE std_ss [LET_DEF]; 2285 2286 2287(* store based on xbp *) 2288 2289val lisp_inv_xbp_store = prove( 2290 ``^LISP ==> isVal x1 /\ getVal x1 < xbp /\ xbp <= LENGTH xs ==> 2291 let wa = (w2w (f (sp - n2w (108 - 8 * 1))) << 32 !! w2w (f (sp - n2w (112 - 8 * 1)))) in 2292 let wb = wa + w2w w1 in 2293 (let (xs,f,tw2) = (UPDATE_NTH ((LENGTH xs + getVal x1) - xbp) x0 xs,(wb =+ w0) f,wa) in ^LISP) /\ 2294 wb IN df /\ (wb && 0x3w = 0x0w) /\ 2295 (sp - n2w (108 - 8 * 1)) IN df /\ ((sp - n2w (108 - 8 * 1) && 3w = 0w)) /\ 2296 (sp - n2w (112 - 8 * 1)) IN df /\ ((sp - n2w (112 - 8 * 1) && 3w = 0w))``, 2297 Cases_on `isVal x1` \\ FULL_SIMP_TAC std_ss [LET_DEF] 2298 \\ FULL_SIMP_TAC std_ss [isVal_thm,getVal_def] \\ STRIP_TAC 2299 \\ IMP_RES_TAC lisp_inv_ds_read \\ ASM_SIMP_TAC std_ss [] 2300 \\ Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2301 \\ NTAC 2 STRIP_TAC 2302 \\ Q.ABBREV_TAC `n = LENGTH xs + a - xbp` 2303 \\ `EL 1 ds + w2w w1 = sp + 0x4w * wsp + 0x4w * n2w n` by 2304 (FULL_SIMP_TAC std_ss [lisp_inv_def,MAP,CONS_11,EVERY_DEF,lisp_x_def] 2305 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (MP_TAC o GSYM) 2306 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,BLAST_LEMMA] 2307 \\ REPEAT STRIP_TAC 2308 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,WORD_MUL_LSL] 2309 \\ `(4 * a + 1) < 4294967296` by DECIDE_TAC 2310 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w] 2311 \\ ONCE_REWRITE_TAC [ADD_COMM] 2312 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_ADD,WORD_ADD_ASSOC] 2313 \\ ASM_SIMP_TAC std_ss [word_arith_lemma3] 2314 \\ Q.PAT_X_ASSUM `LENGTH ss + w2n wsp = sl` (MP_TAC o GSYM) 2315 \\ ASM_SIMP_TAC std_ss [] \\ Q.SPEC_TAC (`wsp`,`w`) 2316 \\ Cases \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,word_mul_n2w,w2n_n2w] 2317 \\ `~(4 * (LENGTH ss + n') < 4 * xbp - 4 * a)` by DECIDE_TAC 2318 \\ ASM_SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL,word_arith_lemma4] 2319 \\ REPEAT STRIP_TAC \\ AP_TERM_TAC \\ Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 2320 \\ ASM_SIMP_TAC std_ss [] 2321 \\ `n < LENGTH xs` by (Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 2322 \\ IMP_RES_TAC (RW[AND_IMP_INTRO]lisp_inv_store_lemma) 2323 \\ ASM_SIMP_TAC std_ss [] 2324 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2325 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3] 2326 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ ASM_SIMP_TAC std_ss [] 2327 \\ Q.EXISTS_TAC `tw2` \\ ASM_SIMP_TAC std_ss []) 2328 |> SIMP_RULE std_ss [LET_DEF]; 2329 2330 2331(* code heap add symbol *) 2332 2333val MEM_LIST_FIND_LEMMA = prove( 2334 ``!sym s k x. MEM s sym ==> (LIST_FIND k s (sym ++ [x]) = LIST_FIND k s sym)``, 2335 Induct \\ SIMP_TAC std_ss [MEM,APPEND,LIST_FIND_def] \\ METIS_TAC []); 2336 2337val bc_symbols_ok_IMP = prove( 2338 ``!bs sym s k. 2339 bc_symbols_ok sym bs ==> 2340 bc_symbols_ok (sym ++ [s]) bs /\ 2341 (bs2bytes (k,sym ++ [s]) bs = bs2bytes (k,sym) bs)``, 2342 Induct \\ SIMP_TAC std_ss [bc_symbols_ok_def,bs2bytes_def] \\ Cases_on `h` 2343 \\ REPEAT (Cases_on `l`) 2344 \\ ASM_SIMP_TAC std_ss [bc_symbols_ok_def,bs2bytes_def,bc_ref_def, 2345 MEM_LIST_FIND_LEMMA,MEM_APPEND]); 2346 2347val code_heap_add_symbol = store_thm("code_heap_add_symbol", 2348 ``code_heap code (sym,base_ptr,curr_ptr,space_left,dh,h) ==> 2349 code_heap code (sym ++ [s],base_ptr,curr_ptr,space_left,dh,h)``, 2350 Cases_on `code` \\ SIMP_TAC std_ss [code_heap_def] \\ REPEAT STRIP_TAC 2351 \\ Q.LIST_EXISTS_TAC [`bs`,`hs`] \\ FULL_SIMP_TAC std_ss [] 2352 \\ IMP_RES_TAC bc_symbols_ok_IMP \\ ASM_SIMP_TAC std_ss []); 2353 2354 2355val _ = export_theory(); 2356