Commit d194c84d authored by Magnus Myreen's avatar Magnus Myreen

Build binary for verified checker

parent d8510caf
INCLUDES = .. ../cakeml/characteristic/examples/compilation/compile
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP)
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
all: $(TARGETS) $(HOLHEAP)
.PHONY: all
BARE_THYS = ../transTheory \
../cakeml/characteristic/examples/compilation/compile/compilationLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
open preamble compilationLib transTheory
val _ = new_theory "checkerBinary"
val checker_compiled = save_thm("checker_compiled",
compile_x64 500 500 "checker" transTheory.entire_program_def);
val _ = export_theory ();
......@@ -262,18 +262,19 @@ val st = get_ml_prog_state()
val main_spec = Q.store_thm("main_spec",
`app (p:'ffi ffi_proj) ^(fetch_v "main" st)
[Conv NONE []] (STDOUT out * STDIN inp F)
[Conv NONE []] (STDOUT out * STDERR err * STDIN inp F)
(POSTv uv. &UNIT_TYPE () uv *
(STDOUT (out ++ runChecker inp) *
STDIN "" T))`,
STDOUT (out ++ runChecker inp) *
STDERR err *
STDIN "" T)`,
xcf "main" st
\\ qmatch_abbrev_tac`_ frame _`
\\ xlet`POSTv uv. &(LIST_TYPE CHAR [] uv) * frame`
>- (xcon \\ xsimpl \\ EVAL_TAC)
\\ qunabbrev_tac`frame`
\\ xlet`POSTv cv. &LIST_TYPE CHAR inp cv * STDIN "" T * STDOUT out`
\\ xlet`POSTv cv. &LIST_TYPE CHAR inp cv * STDERR err * STDIN "" T * STDOUT out`
>- (xapp \\ instantiate \\ xsimpl
\\ map_every qexists_tac[`STDOUT out`,`F`,`inp`]
\\ map_every qexists_tac[`STDERR err * STDOUT out`,`F`,`inp`]
\\ xsimpl)
\\ qmatch_abbrev_tac`_ frame _`
\\ qmatch_goalsub_abbrev_tac`STRCAT _ res`
......@@ -281,7 +282,7 @@ val main_spec = Q.store_thm("main_spec",
>- (xapp \\ instantiate \\ xsimpl)
\\ xapp \\ instantiate
\\ simp[Abbr`frame`]
\\ map_every qexists_tac[`STDIN "" T`,`out`]
\\ map_every qexists_tac[`STDERR err * STDIN "" T`,`out`]
\\ xsimpl);
val spec = main_spec |> UNDISCH_ALL |> add_basis_proj;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment