% For HTML verification [wordt, addrt: TYPE+]: THEORY BEGIN IMPORTING trace_equiv, wordth[wordt, addrt], soft[wordt, addrt], hard2[wordt, addrt], verification_rewrites[wordt, addrt], microrom_rewrite[wordt, addrt] hs: VAR hard_statet ir, acc: VAR wordt mpc: VAR microaddrt opcode: VAR opcodet i,j,k: VAR nat iteratehard ((hs: hard_statet), (cycle: nat)): RECURSIVE hard_statet = (IF cycle = 0 THEN hs ELSE iteratehard(hardstep(hs), cycle-1) ENDIF) MEASURE (LAMBDA hs, i: i) start_condn ((hs: hard_statet)): bool = (mpcp(hs) = 0) visible_hard_state: TYPE = {hs: hard_statet | start_condn(hs)} vhs: VAR visible_hard_state oracle(vhs): nat = LET opcode = instr_part((memp(vhs))(addr_part(pcp(vhs)))) IN IF jump_op?(opcode) THEN 4 ELSIF jump_zero_op?(opcode) THEN IF is_zero(accp(vhs)) THEN 5 ELSE 6 ENDIF ELSIF load_op?(opcode) THEN 6 ELSIF store_op?(opcode) THEN 6 ELSIF add_op?(opcode) THEN 8 ELSIF nop?(opcode) THEN 5 ELSE 8 ENDIF I(vhs): visible_hard_state = iteratehard(vhs, oracle(vhs)) abs (vhs): soft_statet = (# mempart := memp(vhs), pcpart := pcp(vhs), accpart := accp(vhs) #) mem_abs: LEMMA mempart(abs(vhs)) = memp(vhs) pc_abs: LEMMA pcpart(abs(vhs)) = pcp(vhs) acc_abs: LEMMA accpart(abs(vhs)) = accp(vhs) verif: THEORY = trace_equiv[soft_statet, softstep, visible_hard_state, I, abs] END verification