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