include "BitVectorTrie.ma". include "Arithmetic.ma". include "ASM.ma". ndefinition next: BitVectorTrie Byte sixteen → Word → Word × Byte ≝ λpmem,pc. let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat sixteen (S Z)) in 〈res, lookup … pc pmem (zero eight)〉. (* timings taken from SIEMENS *) ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝ λpmem,pc. let 〈pc,v〉 ≝ next pmem pc in let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,ACC_A〉))))), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,ACC_A〉)))), pc〉, one〉 else 〈〈CPL … ACC_A, pc〉, one〉 else let 〈b,v〉≝ head … v in if b then 〈〈MOVX … (Right … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉 else 〈〈MOVX … (Right … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,REGISTER v〉))))), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,DIRECT b1〉))))), pc〉, one〉 else 〈〈CLR … ACC_A, pc〉, one〉 else let 〈b,v〉≝ head … v in if b then 〈〈MOVX … (Left … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉 else 〈〈MOVX … (Left … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, two〉 else 〈〈DA … ACC_A, pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈SETB … CARRY, pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then 〈〈XCH … ACC_A (REGISTER v), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, one〉 else 〈〈SWAP … ACC_A, pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈CLR … CARRY, pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Right … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Right … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Left … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Left … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈CPL … CARRY, pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DIRECT b1〉))))), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, two〉 else 〈〈MUL … ACC_A ACC_B, pc〉, four〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈INC … DPTR, pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Right … 〈CARRY,BIT_ADDR b1〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈SUBB … ACC_A (REGISTER v), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Right … 〈BIT_ADDR b1,CARRY〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Right … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,REGISTER v〉)))), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,DIRECT b2〉)))), pc〉, two〉 else 〈〈DIV … ACC_A ACC_B, pc〉, four〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DATA b1〉))))), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,DATA b2〉)))), pc〉, three〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,DATA b1〉))))), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈JMP … INDIRECT_DPTR, pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then 〈〈XRL … (Left … 〈ACC_A,REGISTER v〉), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈XRL … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left … 〈ACC_A,DIRECT b1〉), pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left … 〈ACC_A,DATA b1〉), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (Right … 〈DIRECT b1,DATA b2〉), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Right … 〈DIRECT b1,ACC_A〉), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈ANL … (Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈ANL … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then 〈〈ORL … (Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈ORL … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈ADDC … ACC_A (REGISTER v), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈RLC … ACC_A, pc〉, one〉 else 〈〈RETI …, pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then 〈〈ADD … ACC_A (REGISTER v), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈RL … ACC_A, pc〉, one〉 else 〈〈RET …, pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈DEC … (REGISTER v), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈DEC … (INDIRECT (from_singl … v)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, one〉 else 〈〈DEC … ACC_A, pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈RRC … ACC_A, pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then 〈〈INC … (REGISTER v), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈INC … (INDIRECT (from_singl … v)), pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, one〉 else 〈〈INC … ACC_A, pc〉, one〉 else let 〈b,v〉≝ head … v in if b then let 〈b,v〉≝ head … v in if b then 〈〈RR … ACC_A, pc〉, one〉 else let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, two〉 else let 〈b,v〉≝ head … v in if b then let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉 else 〈〈NOP …, pc〉, one〉. @. nqed.