Merge pull request #967 from CakeML/lpr_arm8

ARM8 version of LPR checker & proof

developers/build-sequence

@@ -108,6 +108,7 @@ examples/lpr_checker
 examples/lpr_checker/array
 examples/lpr_checker/array/compilation
 examples/lpr_checker/array/compilation/proofs
+examples/lpr_checker/array/compilation/proofsARM8
 examples/opentheory
 examples/opentheory
 examples/opentheory/compilation

examples/lpr_checker/array/compilation/Holmakefile

@@ -1,21 +1,14 @@
 INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/basis $(CAKEMLDIR)/compiler ..
 CLINE_OPTIONS =
 
-all: $(DEFAULT_TARGETS) README.md exec
+all: $(DEFAULT_TARGETS) README.md
 .PHONY: all
 
 README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
 	$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
 
-ifndef CC
-CC=gcc
-endif
-lpr_array.S: *lpr_arrayCompileScript.sml
-lpr_ramsey.S: *lpr_arrayRamseyCompileScript.sml
-cake_lpr_array: lpr_array.S $(CAKEMLDIR)/basis/basis_ffi.o
-	$(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@
-
-exec: cake_lpr_array
-.PHONY: exec
+cake_lpr.S: *lpr_arrayCompileScript.sml
+cake_lpr_arm8.S: *lpr_arrayCompileARM8Script.sml
+cake_lpr_ramsey.S: *lpr_arrayRamseyCompileScript.sml

examples/lpr_checker/array/compilation/README.md

@@ -1,5 +1,8 @@
 An LRAT checker built on CakeML with arrays
 
+[lpr_arrayCompileARM8Script.sml](lpr_arrayCompileARM8Script.sml):
+Compiles the lpr example by evaluation inside the logic of HOL
+
 [lpr_arrayCompileScript.sml](lpr_arrayCompileScript.sml):
 Compiles the lpr example by evaluation inside the logic of HOL
 
@@ -11,3 +14,7 @@ Compiles the lpr example by evaluation inside the logic of HOL
 
 [proofs](proofs):
 Prove end-to-end correctness theorem for LPR checker with arrays
+
+[proofsARM8](proofsARM8):
+Prove end-to-end correctness theorem for LPR checker with arrays
+against ARM8 model

examples/lpr_checker/array/compilation/lpr_arrayCompileARM8Script.sml

@@ -0,0 +1,11 @@
+(*
+  Compiles the lpr example by evaluation inside the logic of HOL
+*)
+open preamble compilationLib lpr_arrayFullProgTheory
+
+val _ = new_theory "lpr_arrayCompileARM8"
+
+val lpr_array_compiled = save_thm("lpr_array_compiled",
+  compile_arm8 "cake_lpr_arm8" check_unsat_prog_def);
+
+val _ = export_theory ();

examples/lpr_checker/array/compilation/lpr_arrayCompileScript.sml

@@ -6,6 +6,6 @@ open preamble compilationLib lpr_arrayFullProgTheory
 val _ = new_theory "lpr_arrayCompile"
 
 val lpr_array_compiled = save_thm("lpr_array_compiled",
-  compile_x64 "lpr_array" check_unsat_prog_def);
+  compile_x64 "cake_lpr" check_unsat_prog_def);
 
 val _ = export_theory ();

examples/lpr_checker/array/compilation/lpr_arrayRamseyCompileScript.sml

@@ -6,6 +6,6 @@ open preamble compilationLib lpr_arrayRamseyProgTheory
 val _ = new_theory "lpr_arrayRamseyCompile"
 
 val lpr_array_compiled = save_thm("lpr_ramsey_compiled",
-  compile_x64 "lpr_ramsey" check_unsat_prog_def);
+  compile_x64 "cake_lpr_ramsey" check_unsat_prog_def);
 
 val _ = export_theory ();

examples/lpr_checker/array/compilation/proofsARM8/Holmakefile

@@ -0,0 +1,15 @@
+INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics/proofs\
+					 $(CAKEMLDIR)/compiler/backend/proofs\
+					 $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv \
+					 $(CAKEMLDIR)/compiler/encoders/arm8_asl \
+					 $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs\
+					 $(CAKEMLDIR)/compiler/backend/arm8_asl \
+					 .. ../..
+
+all: $(DEFAULT_TARGETS) README.md
+.PHONY: all
+
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+DIRS = $(wildcard */)
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)

examples/lpr_checker/array/compilation/proofsARM8/README.md

@@ -0,0 +1,7 @@
+Prove end-to-end correctness theorem for LPR checker with arrays
+against ARM8 model
+
+[lpr_arrayProofARM8Script.sml](lpr_arrayProofARM8Script.sml):
+Compose the semantics theorem and the compiler correctness
+theorem with the compiler evaluation theorem to produce end-to-end
+correctness theorem that reaches final machine code.