1 2 3%----------------------------------------------------------------------------% 4% In this file we specify and verify a resetable parity checker. % 5% This computes the parity of the input since the last reset. % 6% % 7% reset in % 8% | | % 9% | | % 10% *--------------* % 11% | RESET_PARITY | % 12% *--------------* % 13% | % 14% | % 15% out % 16% % 17%----------------------------------------------------------------------------% 18 19new_theory `RESET_PARITY`;; 20 21%----------------------------------------------------------------------------% 22% % 23% To specify RESET_PARITY we first define: % 24% % 25% *- % 26% | T if t1 was the last time before t2 that f was T % 27% LAST (t1,t2) f = < % 28% | F otherwise % 29% *- % 30% % 31% Formally: % 32% % 33% LAST (t1,t2) f = (t1 <= t2) /\ (f t1) /\ !t. t1<t /\ t<=t2 ==> ~(f t) % 34% % 35%----------------------------------------------------------------------------% 36 37let LAST = 38 new_definition 39 (`LAST`, 40 "LAST (t1,t2) f = 41 (t1 <= t2) /\ (f t1) /\ !t. (t1<t) /\ (t<=t2) ==> ~(f t)");; 42 43let LAST_LEMMA1 = 44 prove_thm 45 (`LAST_LEMMA1`, 46 "LAST(t, SUC(t+d))f ==> LAST(t,t+d)f", 47 REWRITE_TAC[LAST] 48 THEN STRIP_TAC 49 THEN STRIP_TAC 50 THEN ASM_REWRITE_TAC[LESS_EQ_ADD] 51 THEN STRIP_TAC 52 THEN STRIP_TAC 53 THEN ASSUME_TAC (SPEC "t + d" LESS_EQ_SUC_REFL) 54 THEN IMP_RES_TAC LESS_EQ_TRANS 55 THEN RES_TAC);; 56 57let SUC_ADD = 58 prove_thm 59 (`SUC_ADD`, 60 "!d. t < SUC(t + d)", 61 INDUCT_TAC 62 THEN ASM_REWRITE_TAC[LESS_THM;ADD_CLAUSES]);; 63 64let LAST_LEMMA2 = 65 prove_thm 66 (`LAST_LEMMA2`, 67 "LAST(t, SUC(t+d))f ==> ~f(SUC(t+d))", 68 REWRITE_TAC[LAST] 69 THEN STRIP_TAC 70 THEN ASSUME_TAC (SPEC "d:num" SUC_ADD) 71 THEN ASSUME_TAC (SPEC "SUC(t+d)" LESS_EQ_REFL) 72 THEN RES_TAC);; 73 74%----------------------------------------------------------------------------% 75% LAST_LEMMA3 = |- LAST(t,SUC t)f ==> ~f(SUC t) % 76%----------------------------------------------------------------------------% 77 78let LAST_LEMMA3 = 79 REWRITE_RULE[ADD_CLAUSES](INST["0","d:num"]LAST_LEMMA2);; 80 81%----------------------------------------------------------------------------% 82% % 83% We also define: % 84% % 85% *- % 86% | T if f is T an even number of times between t1 and t2% 87% PTY (t1,t2) f = < % 88% | F if f is T an odd number of times between t1 and t2 % 89% *- % 90% % 91% Using the function PARITY (from the theory PARITY; see PARITY.ml) we can % 92% define PTY by: % 93% % 94% PTY (t1,t2) f = PARITY (t2-t1) (\t. f(t+t1)) % 95% % 96%----------------------------------------------------------------------------% 97 98new_parent `PARITY`;; 99 100let PTY = 101 new_definition 102 (`PTY`, "PTY (t1,t2) f = PARITY (t2-t1) (\t. f(t+t1))");; 103 104%----------------------------------------------------------------------------% 105% % 106% From this definition it follows that: % 107% % 108% PTY (t,t) f = T % 109% % 110% PTY (t1, SUC t2) f = (f(SUC t2) => ~PTY(t1,t2)f | PTY(t1,t2)f) % 111% % 112%----------------------------------------------------------------------------% 113 114let PARITY = theorem `PARITY` `PARITY_DEF`;; 115 116%----------------------------------------------------------------------------% 117% SUB_REFL = |- n - n = 0 % 118%----------------------------------------------------------------------------% 119 120let SUB_REFL = 121 prove_thm 122 (`SUB_REFL`, 123 "!n. n-n = 0", 124 REWRITE_TAC[SUB_EQ_0;LESS_EQ_REFL]);; 125 126let SUB_SUC = 127 prove_thm 128 (`SUB_SUC`, 129 "!m n. (n <= m) ==> (((SUC m) - n) = SUC(m -n))", 130 REWRITE_TAC[SYM(SPEC_ALL NOT_LESS)] 131 THEN REPEAT STRIP_TAC 132 THEN REWRITE_TAC[REWRITE_RULE[ASSUME "~(m<n)"]SUB]);; 133 134 135let PTY_LEMMA1 = 136 prove_thm 137 (`PTY_LEMMA1`, 138 "(!t f. PTY (t,t) f = T) /\ 139 (!t1 t2 f. 140 (t1 <= t2) ==> 141 (PTY (t1, SUC t2) f = (f(SUC t2) => ~PTY(t1,t2)f | PTY(t1,t2)f)))", 142 REWRITE_TAC[PTY;SUB_REFL;PARITY] 143 THEN BETA_TAC 144 THEN REPEAT STRIP_TAC 145 THEN IMP_RES_TAC SUB_SUC 146 THEN ASM_REWRITE_TAC[PARITY] 147 THEN BETA_TAC 148 THEN REWRITE_TAC[SYM(ASSUME "(SUC t2) - t1 = SUC(t2 - t1)")] 149 THEN ASSUME_TAC(SPEC "t2:num" LESS_EQ_SUC_REFL) 150 THEN IMP_RES_TAC LESS_EQ_TRANS 151 THEN IMP_RES_TAC SUB_ADD 152 THEN ASM_REWRITE_TAC[]);; 153 154%----------------------------------------------------------------------------% 155% A useful corollary. % 156%----------------------------------------------------------------------------% 157 158let PTY_LEMMA2 = 159 prove_thm 160 (`PTY_LEMMA2`, 161 "PTY (t, SUC(t+d)) f = (f(SUC(t+d)) => ~PTY(t,(t+d))f | PTY(t,(t+d))f)", 162 REWRITE_TAC 163 [MATCH_MP (CONJUNCT2 PTY_LEMMA1) (SPECL["t:num";"d:num"]LESS_EQ_ADD)]);; 164 165%----------------------------------------------------------------------------% 166% PTY_LEMMA3 = |- PTY(t,SUC t)f = (f(SUC t) => ~PTY(t,t)f | PTY(t,t)f) % 167%----------------------------------------------------------------------------% 168 169let PTY_LEMMA3 = 170 REWRITE_RULE[ADD_CLAUSES](INST["0","d:num"]PTY_LEMMA2);; 171 172%----------------------------------------------------------------------------% 173% % 174% We can now specify our resetable parity checker by: % 175% % 176% RESET_PARITY(reset,in,out) = % 177% !t1 t2. LAST(t1,t2)reset ==> (out t2 = PTY(t1,t2)in) % 178% % 179%----------------------------------------------------------------------------% 180 181 182let RESET_PARITY = 183 new_definition 184 (`RESET_PARITY`, 185 "RESET_PARITY(reset,in,out) = 186 !t1 t2. LAST(t1,t2)reset ==> (out t2 = PTY(t1,t2)in)");; 187 188% % 189 190%----------------------------------------------------------------------------% 191% % 192% We implement this specification using a resetable register: % 193% % 194% reset in % 195% | | |------------| % 196% | | | | % 197% | | *-----* | % 198% | | | NOT | | % 199% | | *-----* | % 200% | | |l1 |-----|l2 % 201% | | | | | % 202% | *-----------------* | % 203% | | MUX | | % 204% | *-----------------* | % 205% | | | % 206% |---------| |------|l3 | % 207% | | | | | % 208% | *-----------* | | % 209% | | RESET_REG | | | % 210% | *-----------* | | % 211% | | | | % 212% |--| |---------------| % 213% | | | % 214% *-----------------------* % 215% | MUX | % 216% *-----------------------* % 217% | % 218% out % 219% % 220%----------------------------------------------------------------------------% 221 222 223new_parent `RESET_REG`;; 224 225let RESET_PARITY_IMP = 226 new_definition 227 (`RESET_PARITY_IMP`, 228 "RESET_PARITY_IMP(reset,in,out) = 229 ?l1 l2 l3. NOT(l2,l1) /\ 230 MUX(in,l1,l2,l3) /\ 231 RESET_REG(reset,l3,l2) /\ 232 MUX(reset,l2,l3,out)");; 233 234 235let NOT = definition `PARITY` `NOT_DEF` 236and MUX = definition `PARITY` `MUX_DEF` 237and RESET_REG = definition `RESET_REG` `RESET_REG`;; 238 239 240let RESET_PARITY_IMP_LEMMA1 = 241 prove_thm 242 (`RESET_PARITY_IMP_LEMMA1`, 243 "RESET_PARITY_IMP(reset,in,out) 244 ==> 245 !d t. LAST(t,t)reset ==> (out t = PTY(t,t)in)", 246 REWRITE_TAC[RESET_PARITY_IMP;MUX;RESET_REG;LAST;PTY_LEMMA1] 247 THEN REPEAT STRIP_TAC 248 THEN RES_TAC 249 THEN ASM_REWRITE_TAC[]);; 250 251 252%----------------------------------------------------------------------------% 253% The proof that follows is a bad example of `proof hacking', i.e. the use % 254% of ad-hoc low-level manipulations instead of thought. It is likely that % 255% a much more elegant proof is possible. % 256% % 257% First we prove a lemma and then define a couple of special purpose % 258% functions. % 259%----------------------------------------------------------------------------% 260 261%----------------------------------------------------------------------------% 262% LAST(t,t + (SUC d))reset |- ~reset(t + (SUC d)) % 263%----------------------------------------------------------------------------% 264 265let reset_LEMMA = 266 let [();();();th] = CONJUNCTS ADD_CLAUSES 267 in 268 REWRITE_RULE[SYM th] 269 (MATCH_MP (GEN_ALL LAST_LEMMA2) 270 (REWRITE_RULE[ADD_CLAUSES](ASSUME "LAST(t,t + (SUC d))reset")));; 271 272%----------------------------------------------------------------------------% 273% lines `l1 l2 ... ln` tm is true if tm has the form "!t. li t = ..." % 274% for some li. % 275%----------------------------------------------------------------------------% 276 277let lines tok t = 278 (let x = (fst o dest_var o rator o lhs o snd o dest_forall) t 279 in 280 mem x (words tok)) ? false;; 281 282%----------------------------------------------------------------------------% 283% UNWIND_LINES_TAC `l` tm finds an assumption "!t. l t = ... t ..." % 284% and then unwinds with "l tm = ... tm ...". % 285%----------------------------------------------------------------------------% 286 287let UNWIND_LINES_TAC l t = 288 FIRST_ASSUM 289 (\th. if lines l (concl th) then SUBST_TAC[SPEC t th] else NO_TAC);; 290 291 292let RESET_PARITY_IMP_LEMMA2 = 293 prove_thm 294 (`RESET_PARITY_IMP_LEMMA2`, 295 "RESET_PARITY_IMP(reset,in,out) 296 ==> 297 !d t. LAST(t, t+(SUC d))reset 298 ==> 299 (out(t+(SUC d)) = PTY(t, t+(SUC d))in)", 300 REWRITE_TAC[NOT;MUX;RESET_REG;RESET_PARITY_IMP] 301 THEN STRIP_TAC 302 THEN INDUCT_TAC 303 THENL 304 [REWRITE_TAC[ADD_CLAUSES] 305 THEN STRIP_TAC 306 THEN STRIP_TAC 307 THEN IMP_RES_TAC LAST_LEMMA3 308 THEN IMP_RES_TAC (fst (EQ_IMP_RULE LAST)) 309 THEN RES_TAC 310 THEN ASM_REWRITE_TAC[PTY_LEMMA1;PTY_LEMMA3;ADD1]; 311 ALL_TAC] 312 THEN ONCE_REWRITE_TAC[ADD_CLAUSES] 313 THEN STRIP_TAC 314 THEN STRIP_TAC 315 THEN IMP_RES_TAC LAST_LEMMA1 316 THEN IMP_RES_TAC LAST_LEMMA2 317 THEN REWRITE_TAC[PTY_LEMMA2] 318 THEN RES_THEN (\th. REWRITE_TAC[SYM th]) 319 THEN UNWIND_LINES_TAC `out` "SUC(t+(SUC d))" 320 THEN FILTER_ASM_REWRITE_TAC is_neg [] 321 THEN UNWIND_LINES_TAC `l3` "SUC(t+(SUC d))" 322 THEN UNWIND_LINES_TAC `l1` "SUC(t+(SUC d))" 323 THEN ONCE_REWRITE_TAC[ADD1] 324 THEN UNWIND_LINES_TAC `l2` "t+(SUC d)" 325 THEN UNWIND_LINES_TAC `out` "t+(d+1)" 326 THEN REWRITE_TAC [SYM(SPEC_ALL ADD1)] 327 THEN ASSUME_TAC reset_LEMMA 328 THEN FILTER_ASM_REWRITE_TAC is_neg []);; 329 330let RESET_PARITY_IMP_LEMMA3 = 331 prove_thm 332 (`RESET_PARITY_IMP_LEMMA3`, 333 "RESET_PARITY_IMP(reset,in,out) 334 ==> 335 !d t. LAST(t,t+d)reset ==> (out(t+d) = PTY(t,t+d)in)", 336 STRIP_TAC 337 THEN INDUCT_TAC 338 THENL 339 [REWRITE_TAC[ADD_CLAUSES] 340 THEN IMP_RES_TAC RESET_PARITY_IMP_LEMMA1; 341 IMP_RES_TAC RESET_PARITY_IMP_LEMMA2] 342 THEN ASM_REWRITE_TAC[]);; 343 344%----------------------------------------------------------------------------% 345% RESET_PARITY_IMP_LEMMA4 = % 346% |- RESET_PARITY_IMP(reset,in,out) ==> % 347% t1 <= t2 ==> % 348% LAST(t1,t2)reset ==> % 349% (out t2 = PTY(t1,t2)in) % 350%----------------------------------------------------------------------------% 351 352let RESET_PARITY_IMP_LEMMA4 = 353 let th1 = UNDISCH RESET_PARITY_IMP_LEMMA3 354 in 355 let th2 = SPECL["t2-t1";"t1:num"]th1 356 in 357 let th3 = ONCE_REWRITE_RULE[ADD_SYM]th2 358 in 359 let th4 = REWRITE_RULE[MATCH_MP SUB_ADD (ASSUME "t1<=t2")]th3 360 in 361 DISCH_ALL th4;; 362 363 364%----------------------------------------------------------------------------% 365% From the various lemmas we can now prove the implementation correct. % 366%----------------------------------------------------------------------------% 367 368let RESET_PARITY_IMP_CORRECT = 369 prove_thm 370 (`RESET_PARITY_IMP_CORRECT`, 371 "!reset in out. 372 RESET_PARITY_IMP(reset,in,out) ==> RESET_PARITY(reset,in,out)", 373 REWRITE_TAC[RESET_PARITY] 374 THEN REPEAT GEN_TAC 375 THEN DISCH_TAC 376 THEN REPEAT GEN_TAC 377 THEN ASM_CASES_TAC "t1<=t2" 378 THENL 379 [IMP_RES_TAC RESET_PARITY_IMP_LEMMA4; 380 ASM_REWRITE_TAC[LAST]]);; 381