1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory bit_listTheory listTheory opmonTheory combinTheory; 4 5open x86_coretypesTheory; 6 7val _ = new_theory "x86_seq_monad"; 8val _ = ParseExtras.temp_loose_equality() 9 10 11val _ = Hol_datatype `x86_permission = Xread | Xwrite | Xexecute`; 12 13val _ = type_abbrev("x86_memory",``: word32 -> ((word8 # x86_permission set) option)``); 14 15val _ = type_abbrev("x86_state", (* state = tuple consisting of: *) 16 ``: (Xreg -> word32) # (* - general-purpose 32-bit registers *) 17 (word32) # (* - eip *) 18 (Xeflags -> bool option) # (* - eflags *) 19 x86_memory # (* - unsegmented memory *) 20 x86_memory (* - instruction cache *) ``); 21 22(* functions for reading/writing state *) 23 24val XREAD_REG_def = Define `XREAD_REG x ((r,p,s,m,i):x86_state) = r x `; 25val XREAD_EIP_def = Define `XREAD_EIP ((r,p,s,m,i):x86_state) = p `; 26val XREAD_EFLAG_def = Define `XREAD_EFLAG x ((r,p,s,m,i):x86_state) = s x `; 27 28val XREAD_MEM_def = Define ` 29 XREAD_MEM x ((r,p,s,m,i):x86_state) = 30 case m x of 31 NONE => NONE 32 | SOME (w,perms) => if Xread IN perms then SOME w else NONE`; 33 34val XREAD_INSTR_def = Define ` 35 XREAD_INSTR x ((r,p,s,m,i):x86_state) = 36 case (i x, m x) of 37 (NONE, NONE) => NONE 38 | (NONE, SOME (w,perms)) => if {Xread;Xexecute} SUBSET perms then SOME w else NONE 39 | (SOME (w,perms), _) => if {Xread;Xexecute} SUBSET perms then SOME w else NONE`; 40 41val X86_ICACHE_EMPTY_def = Define `X86_ICACHE_EMPTY = (\addr. NONE):x86_memory`; 42 43val XCLEAR_ICACHE_def = Define ` 44 XCLEAR_ICACHE ((r,p,s,m,i):x86_state) = (r,p,s,m,X86_ICACHE_EMPTY):x86_state`; 45 46val XWRITE_REG_def = Define `XWRITE_REG x y ((r,p,s,m,i):x86_state) = ((x =+ y) r,p,s,m,i):x86_state `; 47val XWRITE_EIP_def = Define `XWRITE_EIP y ((r,p,s,m,i):x86_state) = (r,y,s,m,i):x86_state `; 48val XWRITE_EFLAG_def = Define `XWRITE_EFLAG x y ((r,p,s,m,i):x86_state) = (r,p,(x =+ y) s,m,i):x86_state `; 49 50val XWRITE_MEM_def = Define ` 51 XWRITE_MEM x y ((r,p,s,m,i):x86_state) = 52 case m x of 53 NONE => NONE 54 | SOME (w,perms) => if Xwrite IN perms then SOME ((r,p,s,(x =+ SOME (y,perms)) m,i):x86_state) else NONE`; 55 56val XREAD_MEM_BYTES_def = Define ` 57 XREAD_MEM_BYTES n a s = 58 if n = 0 then [] else XREAD_MEM a s :: XREAD_MEM_BYTES (n-1) (a+1w) s`; 59 60val XREAD_INSTR_BYTES_def = Define ` 61 XREAD_INSTR_BYTES n a s = 62 if n = 0 then [] else XREAD_INSTR a s :: XREAD_INSTR_BYTES (n-1) (a+1w) s`; 63 64val w2bits_EL = store_thm("w2bits_EL", 65 ``(w2bits (w:word8) ++ ys = x1::x2::x3::x4::x5::x6::x7::x8::xs) = 66 (EL 0 (w2bits (w:word8)) = x1) /\ 67 (EL 1 (w2bits (w:word8)) = x2) /\ 68 (EL 2 (w2bits (w:word8)) = x3) /\ 69 (EL 3 (w2bits (w:word8)) = x4) /\ 70 (EL 4 (w2bits (w:word8)) = x5) /\ 71 (EL 5 (w2bits (w:word8)) = x6) /\ 72 (EL 6 (w2bits (w:word8)) = x7) /\ 73 (EL 7 (w2bits (w:word8)) = x8) /\ (ys = xs)``, 74 SIMP_TAC (std_ss++wordsLib.SIZES_ss) [w2bits_def] 75 THEN NTAC 9 (ONCE_REWRITE_TAC [n2bits_def] THEN SIMP_TAC std_ss [CONS_11]) 76 THEN SIMP_TAC std_ss [APPEND,CONS_11,EL,rich_listTheory.EL_CONS,HD]); 77 78val expand_mem_read_bytes = 79 (ONCE_REWRITE_CONV [XREAD_MEM_BYTES_def,word2bytes_def] THENC 80 ONCE_REWRITE_CONV [XREAD_MEM_BYTES_def,word2bytes_def] THENC 81 ONCE_REWRITE_CONV [XREAD_MEM_BYTES_def,word2bytes_def] THENC 82 ONCE_REWRITE_CONV [XREAD_MEM_BYTES_def,word2bytes_def] THENC 83 ONCE_REWRITE_CONV [XREAD_MEM_BYTES_def,word2bytes_def] THENC 84 SIMP_CONV std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,ASR_ADD]) 85 86val XREAD_MEM_BYTES_thm = save_thm("XREAD_MEM_BYTES_thm", 87 CONJ (expand_mem_read_bytes ``XREAD_MEM_BYTES 1 a s``) 88 (CONJ (expand_mem_read_bytes ``XREAD_MEM_BYTES 2 a s``) 89 (expand_mem_read_bytes ``XREAD_MEM_BYTES 4 a s``))); 90 91val word2bytes_thm = save_thm("word2bytes_thm", 92 CONJ (expand_mem_read_bytes ``word2bytes 1 w``) 93 (CONJ (expand_mem_read_bytes ``word2bytes 2 w``) 94 (expand_mem_read_bytes ``word2bytes 4 w``))); 95 96val EL_thm = save_thm("EL_thm", 97 CONJ (EVAL ``EL 0 ((x0:'a)::xs)``) 98 (CONJ (EVAL ``EL 1 ((x0:'a)::x2::xs)``) 99 (CONJ (EVAL ``EL 2 ((x0:'a)::x2::x3::xs)``) 100 (EVAL ``EL 3 ((x0:'a)::x2::x3::x4::xs)``)))) 101 102 103(* ---------------------------------------------------------------------------------- *> 104 105 We define a state and monads for constructing a sequential version of the semantics. 106 107<* ---------------------------------------------------------------------------------- *) 108 109(* val _ = type_abbrev("Xstate",``:x86_state -> ('a # x86_state) option``); *) 110 111val _ = type_abbrev("x86_M",``:x86_state -> ('a # x86_state) option``); 112 113 114(* sequential monads for an option state *) 115 116val constT_seq_def = Define ` 117 (constT_seq: 'a -> 'a x86_M) x = \y. SOME (x,y)`; 118 119val addT_seq_def = Define ` 120 (addT_seq: 'a -> 'b x86_M -> ('a # 'b) x86_M) x s = 121 \y. case s y of NONE => NONE | SOME (z,t) => SOME ((x,z),t)`; 122 123val lockT_seq_def = Define ` 124 (lockT_seq: 'a x86_M -> 'a x86_M) s = s`; 125 126val failureT_seq_def = Define ` 127 (failureT_seq: 'a x86_M) = \y. NONE`; 128 129val seqT_seq_def = Define ` 130 (seqT_seq: 'a x86_M -> ('a -> 'b x86_M) -> 'b x86_M) s f = 131 \y. case s y of NONE => NONE | SOME (z,t) => f z t`; 132 133val parT_seq_def = Define ` 134 (parT_seq: 'a x86_M -> 'b x86_M -> ('a # 'b) x86_M) s t = 135 \y. case s y of NONE => NONE | SOME (a,z) => 136 case t z of NONE => NONE | SOME (b,x) => SOME ((a,b),x)`; 137 138val parT_unit_seq_def = Define ` 139 (parT_unit_seq: unit x86_M -> unit x86_M -> unit x86_M) s t = 140 \y. case s y of NONE => NONE | SOME (a,z) => 141 case t z of NONE => NONE | SOME (b,x) => SOME ((),x)`; 142 143(* register reads/writes always succeed. *) 144 145val write_reg_seq_def = Define `(write_reg_seq ii r x):unit x86_M = 146 \s. SOME ((),XWRITE_REG r x s)`; 147 148val read_reg_seq_def = Define `(read_reg_seq ii r):Ximm x86_M = 149 \s. SOME (XREAD_REG r s,s)`; 150 151(* eflags can always be written, but reading a NONE eflag causes a failure *) 152 153val write_eflag_seq_def = Define `(write_eflag_seq ii f x):unit x86_M = 154 (\s. SOME ((),XWRITE_EFLAG f x s))`; 155 156val read_eflag_seq_def = Define `(read_eflag_seq ii f):bool x86_M = 157 (\s. case XREAD_EFLAG f s of NONE => NONE | SOME b => SOME (b,s))`; 158 159(* eip reads/writes always succeed. *) 160 161val write_eip_seq_def = Define `(write_eip_seq ii x):unit x86_M = 162 \s. SOME ((),XWRITE_EIP x s)`; 163 164val read_eip_seq_def = Define `(read_eip_seq ii):Ximm x86_M = 165 \s. SOME (XREAD_EIP s,s)`; 166 167(* memory writes are only allowed to modelled memory, i.e. locations containing SOME ... *) 168 169val write_mem_seq_def = Define `(write_mem_seq ii a x):unit x86_M = 170 (\s. case XWRITE_MEM a x s of NONE => NONE | SOME s2 => SOME ((),s2))`; 171 172(* a memory read to an unmodelled memory location causes a failure *) 173 174val read_mem_seq_def = Define `(read_mem_seq ii a):word8 x86_M = 175 (\s. case XREAD_MEM a s of NONE => NONE | SOME x => SOME (x,s))`; 176 177(* reading and writing 32-bit entities *) 178 179val read_m32_seq_def = Define `(read_m32_seq ii a):Ximm x86_M = 180 seqT_seq (parT_seq (read_mem_seq ii (a+0w)) (parT_seq (read_mem_seq ii (a+1w)) 181 (parT_seq (read_mem_seq ii (a+2w)) (read_mem_seq ii (a+3w))))) 182 (\(x0,x1,x2,x3). constT_seq (bytes2word [x0;x1;x2;x3]))`; 183 184val write_m32_seq_def = Define `(write_m32_seq ii a w):unit x86_M = 185 (let bs = word2bytes 4 w in 186 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs)) (parT_unit_seq (write_mem_seq ii (a+1w) (EL 1 bs)) 187 (parT_unit_seq (write_mem_seq ii (a+2w) (EL 2 bs)) (write_mem_seq ii (a+3w) (EL 3 bs)))))`; 188 189val read_m8_seq_def = Define `(read_m8_seq ii a):word8 x86_M = 190 read_mem_seq ii a`; 191 192val write_m8_seq_def = Define `(write_m8_seq ii a w):unit x86_M = 193 write_mem_seq ii a (w:word8)`; 194 195(* clear the icache *) 196 197val clear_icache_seq_def = Define `(clear_icache_seq ii):unit x86_M = 198 \s. SOME ((),XCLEAR_ICACHE s)`; 199 200 201(* export *) 202 203val _ = Define `(constT: 'a -> 'a x86_M) = constT_seq`; 204val _ = Define `(addT: 'a -> 'b x86_M -> ('a # 'b) x86_M) = addT_seq`; 205val _ = Define `(lockT: unit x86_M -> unit x86_M) = lockT_seq`; 206val _ = Define `(failureT: unit x86_M) = failureT_seq`; 207val _ = Define `(seqT: 'a x86_M -> (('a -> 'b x86_M) -> 'b x86_M)) = seqT_seq`; 208val _ = Define `(parT: 'a x86_M -> 'b x86_M -> ('a # 'b) x86_M) = parT_seq`; 209val _ = Define `(parT_unit: unit x86_M -> unit x86_M -> unit x86_M) = parT_unit_seq`; 210val _ = Define `(write_reg: iiid -> Xreg -> Ximm -> unit x86_M) = write_reg_seq`; 211val _ = Define `(read_reg: iiid -> Xreg -> Ximm x86_M) = read_reg_seq`; 212val _ = Define `(write_eip: iiid -> Ximm -> unit x86_M) = write_eip_seq`; 213val _ = Define `(read_eip: iiid -> Ximm x86_M) = read_eip_seq`; 214val _ = Define `(write_eflag: iiid -> Xeflags -> bool option -> unit x86_M) = write_eflag_seq`; 215val _ = Define `(read_eflag: iiid -> Xeflags -> bool x86_M) = read_eflag_seq`; 216val _ = Define `(write_m32: iiid -> Ximm -> Ximm-> unit x86_M) = write_m32_seq`; 217val _ = Define `(read_m32: iiid -> Ximm -> Ximm x86_M) = read_m32_seq`; 218val _ = Define `(write_m8: iiid -> Ximm -> word8 -> unit x86_M) = write_m8_seq`; 219val _ = Define `(read_m8: iiid -> Ximm -> word8 x86_M) = read_m8_seq`; 220val _ = Define `(clear_icache: iiid -> unit x86_M) = clear_icache_seq`; 221 222 223 224(* some rewriter-friendly theorems *) 225 226val option_apply_def = Define ` 227 option_apply x f = if x = NONE then NONE else f (THE x)`; 228 229val option_apply_SOME = prove( 230 ``!x f. option_apply (SOME x) f = f x``,SRW_TAC [] [option_apply_def]); 231 232val XWRITE_MEM2_def = Define ` 233 XWRITE_MEM2 a w ((r,e,t,m,i):x86_state) = (r,e,t,(a =+ SOME (w, SND (THE (m a)))) m,i)`; 234 235val XREAD_MEM2_def = Define ` 236 XREAD_MEM2 a ((r,e,t,m,i):x86_state) = FST (THE (m a))`; 237 238val XREAD_MEM2_WORD_def = Define ` 239 XREAD_MEM2_WORD a (s:x86_state) = (bytes2word 240 [XREAD_MEM2 (a + 0x0w) s; XREAD_MEM2 (a + 0x1w) s; 241 XREAD_MEM2 (a + 0x2w) s; XREAD_MEM2 (a + 0x3w) s]) :word32`; 242 243val XWRITE_MEM2_WORD_def = Define ` 244 XWRITE_MEM2_WORD a (w:word32) (s:x86_state) = 245 XWRITE_MEM2 (a + 3w) (EL 3 (word2bytes 4 w)) 246 (XWRITE_MEM2 (a + 2w) (EL 2 (word2bytes 4 w)) 247 (XWRITE_MEM2 (a + 1w) (EL 1 (word2bytes 4 w)) 248 (XWRITE_MEM2 (a + 0w) (EL 0 (word2bytes 4 w)) s)))`; 249 250val CAN_XWRITE_MEM_def = Define ` 251 CAN_XWRITE_MEM a s = !w. ~(XWRITE_MEM a w s = NONE)`; 252 253val CAN_XREAD_MEM_def = Define ` 254 CAN_XREAD_MEM a s = ~(XREAD_MEM a s = NONE)`; 255 256val mem_seq_lemma = prove( 257 ``(read_mem_seq ii a s = option_apply (XREAD_MEM a s) (\x. SOME (x,s))) /\ 258 (write_mem_seq ii a y s = option_apply (XWRITE_MEM a y s) (\s. SOME ((),s)))``, 259 SRW_TAC [] [option_apply_def,read_mem_seq_def,write_mem_seq_def] 260 THEN Cases_on `XREAD_MEM a s` THEN FULL_SIMP_TAC std_ss [] 261 THEN Cases_on `XWRITE_MEM a y s` THEN FULL_SIMP_TAC std_ss []); 262 263val read_eflag_seq_lemma = prove( 264 ``read_eflag_seq ii f s = option_apply (XREAD_EFLAG f s) (\x. SOME (x,s))``, 265 SRW_TAC [] [option_apply_def,read_eflag_seq_def] 266 THEN Cases_on `XREAD_EFLAG f s` THEN FULL_SIMP_TAC std_ss []); 267 268val parT_unit_seq_lemma = prove( 269 ``(parT_unit_seq s t = \y. option_apply (s y) (\z. 270 option_apply (t (SND z)) (\x. SOME ((),SND x))))``, 271 SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `s y` 272 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x` 273 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] 274 THEN FULL_SIMP_TAC std_ss [] THEN Cases_on `t r` 275 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x` 276 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def]); 277 278val monad_simp_lemma = prove( 279 ``(constT_seq x = \y. SOME (x,y)) /\ (failureT_seq = \y. NONE) /\ (lockT_seq d = d) /\ 280 (addT_seq q s = \y. option_apply (s y) (\t. SOME ((q,FST t),SND t))) /\ 281 (seqT_seq s f = \y. option_apply (s y) (\t. f (FST t) (SND t))) /\ 282 (parT_seq s t = \y. option_apply (s y) (\z. 283 option_apply (t (SND z)) (\x. SOME ((FST z,FST x),SND x))))``, 284 SRW_TAC [] [parT_seq_def,seqT_seq_def,failureT_seq_def,lockT_seq_def, 285 addT_seq_def,constT_seq_def,FUN_EQ_THM] 286 THEN Cases_on `s y` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def] 287 THEN Cases_on `x` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def] 288 THEN Cases_on `t r` THEN SRW_TAC [] [option_apply_def] THEN FULL_SIMP_TAC std_ss [] 289 THEN Cases_on `x` THEN SRW_TAC [] [option_apply_def]); 290 291val seq_monad_thm = save_thm("seq_monad_thm",let 292 val xs = option_apply_SOME :: mem_seq_lemma :: read_eflag_seq_lemma :: 293 parT_unit_seq_lemma :: (CONJUNCTS monad_simp_lemma) 294 in LIST_CONJ (map GEN_ALL xs) end); 295 296val CAN_XWRITE_MEM = store_thm("CAN_XWRITE_MEM", 297 ``CAN_XWRITE_MEM a (r,e,s,m,i) = 298 ~(m a = NONE) /\ Xwrite IN SND (THE (m a))``, 299 SIMP_TAC std_ss [XWRITE_MEM_def,CAN_XWRITE_MEM_def] 300 THEN Cases_on `m a` THEN ASM_SIMP_TAC std_ss [] THEN SRW_TAC [] [] 301 THEN Cases_on `x` THEN Cases_on `Xwrite IN r'` THEN SRW_TAC [] []); 302 303val CAN_XREAD_MEM = store_thm("CAN_XREAD_MEM", 304 ``CAN_XREAD_MEM a (r,e,s,m,i) = 305 ~(m a = NONE) /\ Xread IN SND (THE (m a))``, 306 SIMP_TAC std_ss [XREAD_MEM_def,CAN_XREAD_MEM_def] 307 THEN Cases_on `m a` THEN ASM_SIMP_TAC std_ss [] THEN SRW_TAC [] [] 308 THEN Cases_on `x` THEN SRW_TAC [] []); 309 310val CAN_XREAD_XWRITE_THM = store_thm("CAN_XREAD_XWRITE_THM", 311 ``!s. (CAN_XWRITE_MEM a s ==> CAN_XWRITE_MEM a (XWRITE_REG r2 w s)) /\ 312 (CAN_XWRITE_MEM a s ==> CAN_XWRITE_MEM a (XWRITE_EIP e s)) /\ 313 (CAN_XWRITE_MEM a s ==> CAN_XWRITE_MEM a (XWRITE_EFLAG f b s)) /\ 314 (CAN_XWRITE_MEM a s ==> CAN_XWRITE_MEM a (XCLEAR_ICACHE s)) /\ 315 (CAN_XWRITE_MEM a s ==> CAN_XWRITE_MEM a (XWRITE_MEM2 c x s)) /\ 316 (CAN_XREAD_MEM a s ==> CAN_XREAD_MEM a (XWRITE_REG r2 w s)) /\ 317 (CAN_XREAD_MEM a s ==> CAN_XREAD_MEM a (XWRITE_EIP e s)) /\ 318 (CAN_XREAD_MEM a s ==> CAN_XREAD_MEM a (XWRITE_EFLAG f b s)) /\ 319 (CAN_XREAD_MEM a s ==> CAN_XREAD_MEM a (XCLEAR_ICACHE s)) /\ 320 (CAN_XREAD_MEM a s /\ CAN_XWRITE_MEM c s ==> CAN_XREAD_MEM a (XWRITE_MEM2 c x s))``, 321 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR] 322 THEN ASM_SIMP_TAC std_ss [XREAD_REG_def,XREAD_EIP_def, 323 XREAD_EFLAG_def, XWRITE_REG_def, XWRITE_MEM2_def, XREAD_MEM2_def, 324 combinTheory.APPLY_UPDATE_THM, XWRITE_EIP_def,CAN_XREAD_MEM, 325 XWRITE_EFLAG_def,XCLEAR_ICACHE_def,CAN_XWRITE_MEM] 326 THEN Cases_on `c = a` THEN ASM_SIMP_TAC std_ss []); 327 328val x86_else_none_write_mem_lemma = store_thm("x86_else_none_write_mem_lemma", 329 ``!a x t f. CAN_XWRITE_MEM a t ==> 330 (option_apply (XWRITE_MEM a x t) f = f (XWRITE_MEM2 a x t))``, 331 REPEAT STRIP_TAC 332 THEN `?r e s m i. t = (r,e,s,m,i)` by METIS_TAC [pairTheory.PAIR] 333 THEN FULL_SIMP_TAC std_ss [CAN_XWRITE_MEM,XWRITE_MEM_def,XWRITE_MEM2_def] 334 THEN Cases_on `m a` THEN FULL_SIMP_TAC std_ss [] 335 THEN Cases_on `x'` THEN FULL_SIMP_TAC (srw_ss()) [] 336 THEN SRW_TAC [] [option_apply_def]); 337 338val x86_else_none_read_mem_lemma = store_thm("x86_else_none_read_mem_lemma", 339 ``!a x t f. CAN_XREAD_MEM a t ==> 340 (option_apply (XREAD_MEM a t) f = f (XREAD_MEM2 a t))``, 341 REPEAT STRIP_TAC 342 THEN `?r e s m i. t = (r,e,s,m,i)` by METIS_TAC [pairTheory.PAIR] 343 THEN FULL_SIMP_TAC std_ss [CAN_XREAD_MEM,XREAD_MEM2_def,XREAD_MEM_def] 344 THEN Cases_on `m a` THEN FULL_SIMP_TAC std_ss [] 345 THEN Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] 346 THEN SRW_TAC [] [option_apply_def]); 347 348val x86_else_none_eflag_lemma = store_thm("x86_else_none_eflag_lemma", 349 ``!m a f. ~(m a = NONE) ==> 350 (option_apply ((m:x86_state->bool option) a) (f:bool->'a option) = f (THE (m a)))``, 351 SIMP_TAC std_ss [option_apply_def]); 352 353val x86_state_EXPAND = store_thm("x86_state_EXPAND", 354 ``?r i f m. s:x86_state = (r,i,f,m)``, 355 Cases_on `s` THEN Cases_on `r` THEN Cases_on `r'` THEN SIMP_TAC std_ss []); 356 357val XREAD_EIP_ADD_0 = store_thm("XREAD_EIP_ADD_0", 358 ``XREAD_MEM (XREAD_EIP s) s = XREAD_MEM (XREAD_EIP s + 0w) s``, 359 REWRITE_TAC [WORD_ADD_0]); 360 361val x86_address_lemma = store_thm("x86_address_lemma", 362 ``~(0w = 1w:word32) /\ ~(0w = 2w:word32) /\ ~(0w = 3w:word32) /\ 363 ~(1w = 2w:word32) /\ ~(1w = 3w:word32) /\ ~(2w = 3w:word32)``, 364 EVAL_TAC); 365 366val _ = export_theory (); 367