NameDateSize

..25-Jul-20196

arm_emitScript.smlH A D25-Jul-201910.1 KiB

arm_evalLib.sigH A D25-Jul-20191.6 KiB

arm_evalLib.smlH A D25-Jul-201927.9 KiB

arm_evalScript.smlH A D25-Jul-201957.7 KiB

arm_rulesLib.sigH A D25-Jul-2019371

arm_rulesLib.smlH A D25-Jul-20194.3 KiB

arm_rulesScript.smlH A D25-Jul-201932.5 KiB

armLib.sigH A D25-Jul-2019426

armLib.smlH A D25-Jul-20192.8 KiB

armParser.grmH A D25-Jul-201912.6 KiB

armParser.lexH A D25-Jul-20199.3 KiB

armScript.smlH A D25-Jul-201933.2 KiB

assemblerML.sigH A D25-Jul-20191.1 KiB

assemblerML.smlH A D25-Jul-201932.4 KiB

Data.smlH A D25-Jul-20193.1 KiB

HolmakefileH A D25-Jul-20191.2 KiB

instructionScript.smlH A D25-Jul-201910.8 KiB

instructionSyntax.sigH A D25-Jul-2019468

instructionSyntax.smlH A D25-Jul-201931.3 KiB

mlton/H25-Jul-20197

my_listScript.smlH A D25-Jul-20196 KiB

READMEH A D25-Jul-2019661

run_arm_evalScript.smlH A D25-Jul-20194.5 KiB

systemScript.smlH A D25-Jul-201928.6 KiB

updateScript.smlH A D25-Jul-20198.5 KiB

README

1A model of the ARM instructions set.
2
3The files are as follows:  
4
5 * armScript.sml: A HOL specification of the ARM instruction set.
6
7 * instructionScript.sml: Datatype and encoding functions for ARM instructions.
8
9 * bsubstScript.sml: Substitution using a list.
10
11 * my_listScript.sml: A collection of list lemmas.
12
13 * arm_evalScript.sml: Theorems about the ARM model and instruction encoding.
14
15 * arm_rulesScript.sml: Derived rules.
16
17 * arm_evalLib: Functions for assembling ARM code and running the model.
18
19 * run_arm_evalLib.sml: Some examples of running the model.
20
21 * Data.sml, Lexer.lex, Parser.grm, instructionSyntax.sml:
22     A parser and disassembler.
23