Commit 8402bdb6 authored by Heiko Becker's avatar Heiko Becker

Add ssa validation, fix bug in parser and clean up extraction

parent 23f038af
......@@ -58,50 +58,57 @@ Proof.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
if (validIntervalboundsCmd f absenv P NatSet.empty)
then (validErrorboundCmd f absenv NatSet.empty)
if (validSSA f (freeVars f))
then
if (validIntervalboundsCmd f absenv P NatSet.empty)
then (validErrorboundCmd f absenv NatSet.empty)
else false
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (E1 E2:env) outVars vR vF fVars,
approxEnv E1 absenv fVars NatSet.empty E2 ->
(forall v, NatSet.mem v fVars= true ->
forall (E1 E2:env) vR vF ,
(* The execution environments are only off by the machine epsilon *)
approxEnv E1 absenv (freeVars f) NatSet.empty E2 ->
(* All free variables are respecting the precondition *)
(forall v, NatSet.mem v (freeVars f)= true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (Commands.freeVars f) fVars ->
ssa f fVars outVars ->
(* Evaluations on the reals and on 1+delta floats *)
bstep (toRCmd f) E1 0 vR ->
bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
(* Certificate checking succeeds *)
CertificateCheckerCmd f absenv P = true ->
(* Thereby we obtain a valid roundoff error *)
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros E1 E2 outVars vR vF fVars approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float
certificate_valid.
intros E1 E2 vR vF approxE1E2 P_valid eval_real eval_float certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
rewrite <- andb_lazy_alt in certificate_valid.
repeat rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
env_assert absenv (getRetExp f) env_f.
destruct env_f as [iv [err absenv_eq]].
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply (validErrorboundCmd_sound); eauto.
- instantiate (1 := outVars).
eapply ssa_equal_set; try eauto.
hnf.
intros a; split; intros in_union.
+ rewrite NatSet.union_spec in in_union.
destruct in_union as [in_fVars | in_empty]; try auto.
inversion in_empty.
+ rewrite NatSet.union_spec; auto.
- hnf; intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
destruct in_diff.
apply fVars_subset; auto.
- intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
assert (exists outVars, ssa f (freeVars f) outVars) as ssa_f.
- apply validSSA_sound; auto.
- destruct ssa_f as [outVars ssa_f].
env_assert absenv (getRetExp f) env_f.
destruct env_f as [iv [err absenv_eq]].
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply (validErrorboundCmd_sound); eauto.
+ instantiate (1 := outVars).
eapply ssa_equal_set; try eauto.
hnf.
intros a; split; intros in_union.
* rewrite NatSet.union_spec in in_union.
destruct in_union as [in_fVars | in_empty]; try auto.
inversion in_empty.
* rewrite NatSet.union_spec; auto.
+ hnf; intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
destruct in_diff; auto.
+ intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
#############################################################################
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.6 ##
#############################################################################
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
#
# This Makefile was generated by the command line :
# coq_makefile -f _CoqProject -o Makefile
#
.DEFAULT_GOAL := all
# This Makefile may take arguments passed as environment variables:
# COQBIN to specify the directory where Coq binaries resides;
# TIMECMD set a command to log .v compilation time;
# TIMED if non empty, use the default time command as TIMECMD;
# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
# DSTROOT to specify a prefix to install path.
# VERBOSE to disable the short display of compilation rules.
VERBOSE?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
# Here is a hack to make $(eval $(shell works:
define donewline
endef
includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
$(call includecmdwithout@,$(COQBIN)coqtop -config)
TIMED?=
TIMECMD?=
STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
vo_to_obj = $(addsuffix .o,\
$(filter-out Warning: Error:,\
$(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
##########################
# #
# Libraries definitions. #
# #
##########################
COQLIBS?=\
-R "../" Daisy
COQCHKLIBS?=\
-R "../" Daisy
COQDOCLIBS?=\
-R "../" Daisy
##########################
# #
# Variables definitions. #
# #
##########################
OPT?=
COQDEP?="$(COQBIN)coqdep" -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
COQC?=$(TIMER) "$(COQBIN)coqc"
GALLINA?="$(COQBIN)gallina"
COQDOC?="$(COQBIN)coqdoc"
COQCHK?="$(COQBIN)coqchk"
COQMKTOP?="$(COQBIN)coqmktop"
##################
# #
# Install Paths. #
# #
##################
ifdef USERINSTALL
XDG_DATA_HOME?="$(HOME)/.local/share"
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
COQLIBINSTALL="${COQLIB}user-contrib"
COQDOCINSTALL="${DOCDIR}user-contrib"
COQTOPINSTALL="${COQLIB}toploop"
endif
######################
# #
# Files dispatching. #
# #
######################
VFILES:=Checker_extraction.v
ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(VFILES))
else
ifeq ($(MAKECMDGOALS),)
-include $(addsuffix .d,$(VFILES))
endif
endif
.SECONDARY: $(addsuffix .d,$(VFILES))
VO=vo
VOFILES:=$(VFILES:.v=.$(VO))
VOFILES0=$(patsubst ..//%,%,$(filter ..//%,$(VOFILES)))
GLOBFILES:=$(VFILES:.v=.glob)
GFILES:=$(VFILES:.v=.g)
HTMLFILES:=$(VFILES:.v=.html)
GHTMLFILES:=$(VFILES:.v=.g.html)
OBJFILES=$(call vo_to_obj,$(VOFILES))
ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
NATIVEFILES0=$(patsubst ..//%,%,$(filter ..//%,$(NATIVEFILES)))
ifeq '$(HASNATDYNLINK)' 'true'
HASNATDYNLINK_OR_EMPTY := yes
else
HASNATDYNLINK_OR_EMPTY :=
endif
#######################################
# #
# Definition of the toplevel targets. #
# #
#######################################
all: $(VOFILES)
quick: $(VOFILES:.vo=.vio)
vio2vo:
$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
checkproofs:
$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
gallina: $(GFILES)
html: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
gallinahtml: $(GLOBFILES) $(VFILES)
- mkdir -p html
$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
all.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.ps: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
all-gal.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
validate: $(VOFILES)
$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))
beautify: $(VFILES:=.beautified)
for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
@echo 'Do not do "make clean" until you are sure that everything went well!'
@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
####################
# #
# Special targets. #
# #
####################
byte:
$(MAKE) all "OPT:=-byte"
opt:
$(MAKE) all "OPT:=-opt"
userinstall:
+$(MAKE) USERINSTALL=true install
install:
cd "../" && for i in $(NATIVEFILES0) $(GLOBFILES0) $(VFILES0) $(VOFILES0); do \
install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Daisy/$$i`"; \
install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Daisy/$$i; \
done
install-doc:
install -d "$(DSTROOT)"$(COQDOCINSTALL)/Daisy/html
for i in html/*; do \
install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/Daisy/$$i;\
done
uninstall_me.sh: Makefile
echo '#!/bin/sh' > $@
printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/Daisy && rm -f $(NATIVEFILES0) $(GLOBFILES0) $(VFILES0) $(VOFILES0) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "Daisy" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/Daisy \\\n' >> "$@"
printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find Daisy/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
chmod +x $@
uninstall: uninstall_me.sh
sh $<
.merlin:
@echo 'FLG -rectypes' > .merlin
@echo "B $(COQLIB)kernel" >> .merlin
@echo "B $(COQLIB)lib" >> .merlin
@echo "B $(COQLIB)library" >> .merlin
@echo "B $(COQLIB)parsing" >> .merlin
@echo "B $(COQLIB)pretyping" >> .merlin
@echo "B $(COQLIB)interp" >> .merlin
@echo "B $(COQLIB)printing" >> .merlin
@echo "B $(COQLIB)intf" >> .merlin
@echo "B $(COQLIB)proofs" >> .merlin
@echo "B $(COQLIB)tactics" >> .merlin
@echo "B $(COQLIB)tools" >> .merlin
@echo "B $(COQLIB)ltacprof" >> .merlin
@echo "B $(COQLIB)toplevel" >> .merlin
@echo "B $(COQLIB)stm" >> .merlin
@echo "B $(COQLIB)grammar" >> .merlin
@echo "B $(COQLIB)config" >> .merlin
@echo "B $(COQLIB)ltac" >> .merlin
@echo "B $(COQLIB)engine" >> .merlin
clean::
rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)
find . -name .coq-native -type d -empty -delete
rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- rm -rf html mlihtml uninstall_me.sh
cleanall:: clean
rm -f $(patsubst %.v,.%.aux,$(VFILES))
archclean::
rm -f *.cmx *.o
printenv:
@"$(COQBIN)coqtop" -config
@echo 'OCAMLFIND = $(OCAMLFIND)'
@echo 'PP = $(PP)'
@echo 'COQFLAGS = $(COQFLAGS)'
@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
Makefile: _CoqProject
mv -f $@ $@.bak
"$(COQBIN)coq_makefile" -f $< -o $@
###################
# #
# Implicit rules. #
# #
###################
$(VOFILES): %.vo: %.v
$(SHOW)COQC $<
$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
$(GLOBFILES): %.glob: %.v
$(COQC) $(COQDEBUG) $(COQFLAGS) $<
$(VFILES:.v=.vio): %.vio: %.v
$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
$(GFILES): %.g: %.v
$(GALLINA) $<
$(VFILES:.v=.tex): %.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
$(HTMLFILES): %.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
$(VFILES:.v=.g.tex): %.g.tex: %.v
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
$(GHTMLFILES): %.g.html: %.v %.glob
$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
$(addsuffix .d,$(VFILES)): %.v.d: %.v
$(SHOW)'COQDEP $<'
$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
$(addsuffix .beautified,$(VFILES)): %.v.beautified:
$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
# WARNING
#
# This Makefile has been automagically generated
# Edit at your own risks !
#
# END OF WARNING
-R ../ Daisy
Checker_extraction.v
#load "CoqChecker.cmo";;
open Printf;;
open Format;;
open CoqChecker;;
open List;;
open String;;
open Char;;
open Big_int;;
let str_join s1 s2 = String.concat "" [s1;s2];;
let explode s = let rec exp i l = if i < 0 then l else exp (i - 1) ((s.[i]) :: l) in exp (String.length s - 1) [];;
let rec implode sl =
match sl with
|c :: sl' -> str_join (String.make 1 c) (implode sl')
|[] -> "";;
(*
Based on:
https://stackoverflow.com/questions/5774934/how-do-i-read-in-lines-from-a-text-file-in-ocaml
*)
let read_file filename =
let text = ref "" in
let chan = open_in filename in
try
while true; do
text := str_join (!text)(input_line chan)
done; !text
with End_of_file ->
close_in chan;
!text;;
let input = read_file (Sys.argv.(1));;
let res = implode (CoqChecker.runChecker (explode (input)));;
let () = printf "%s\n" res;;
(* let rec pow a = function
| 0 -> 1
......@@ -47,17 +75,13 @@ let ascii_to_char (c:CoqChecker.ascii) =
let eth_val = if (eth = CoqChecker.True) then 1 else 0 in
chr (fst_val + snd_val + thd_val + fth_val + fft_val + sxt_val + svt_val + eth_val);; *)
let str_join s1 s2 = String.concat "" [s1;s2];;
(*
let explode s =
let rec exp i l =
if i < 0 then l else exp (i - 1) ((s.[i]) :: l) in
exp (String.length s - 1) [];;
*)
let rec implode sl =
match sl with
|c :: sl' -> str_join (String.make 1 c) (implode sl')
|[] -> "";;
(*
let rec str_to_coq_str (s:char CoqChecker.list) :CoqChecker.string =
match s with
......@@ -69,12 +93,16 @@ let rec str_coq_to_str (s:CoqChecker.string) =
|CoqChecker.String (c, s') -> String.concat "" [(String.make 1 (ascii_to_char c)); str_coq_to_str s']
|CoqChecker.EmptyString -> "";; *)
implode (CoqChecker.runChecker dParse(lex (explode "1 Ret + 1657#5 Var 1 PRE ? Var 1 ~100#1 100#1 ABS ? + 1657#5 Var 1 1157#5 2157#5 7771411516990528329#81129638414606681695789005144064 ? 1657#5 1657#5 1657#5 1657#45035996273704960 ? Var 1 ~100#1 100#1 25#2251799813685248 ")) 1000);;
(*let () = printf "%s@." Sys.argv.(1);; *)
let () = printf "%s\n" Sys.argv.(1);;
(* let parse = dParse (lex (explode (Sys.argv.(1))) (big_int_of_int 1000)) (big_int_of_int 1000);; *)
(* let ( )= printf "%s\n" parse;; *)
(* let () = printf "Parsing done";; *)
(*t res = implode (CoqChecker.runChecker (explode (Array.get (Sys.argv) 1)));;*)
(* let () = printf "%s\n" res;; *)
(*
let () = printf "%s\n" (str_coq_to_str (str_to_coq_str (explode (Array.get (Sys.argv) 1))));;
let res = str_coq_to_str (CoqChecker.runChecker (str_to_coq_str (explode "1 Ret")));;
let res = CoqChecker.runChecker (str_to_coq_str (explode (Array.get (Sys.argv) 1)));;
let () = printf "%s\n" (str_coq_to_str res);;
let () = printf "%s\n" foo
let () = printf "%s\n" foo *)
......@@ -11,13 +11,14 @@ Inductive Token:Type :=
| DABS
| DCOND
| DVAR
| DCONST: nat -> Token
| DCONST: N -> Token
| DNEG
| DPLUS
| DSUB
| DMUL
| DDIV
| DFRAC.
| DFRAC
| DFAIL: ascii -> Token.
Open Scope string_scope.
......@@ -28,7 +29,7 @@ Definition getChar (input:string):=
end.
Definition getConst (c:ascii) :=
((nat_of_ascii c) - 48)%nat.
((N_of_ascii c) - 48)%N.
Definition suffix (s:string) :=
match s with
......@@ -46,12 +47,12 @@ Definition isAlpha (c:ascii) :bool :=
Definition isAlphaNum (c :ascii) :bool :=
isDigit c || isAlpha c.
Fixpoint lexConst (input:string) (akk:nat) :=
Fixpoint lexConst (input:string) (akk:N) :=
match input with
|String c input' =>
if (isDigit c)
then lexConst input' (akk * 10 + getConst c)
else (akk, input')
else (akk, input)
|EmptyString => (akk, input)
end.
......@@ -99,12 +100,12 @@ match fuel with
| "-"%char => DSUB :: lex input' fuel'
| "*"%char => DMUL :: lex input' fuel'
| "/"%char => DDIV :: lex input' fuel'
| "#"%char => DFRAC :: lex input' fuel'
| "035"%char => DFRAC :: lex input' fuel'
| "?"%char => DCOND :: lex input' fuel'
| "~"%char => DNEG :: lex input' fuel'
| " "%char => lex input' fuel'
| "010"%char => lex input' fuel'
| _ => []
| _ => DFAIL char :: []
end
| _ => []
end
......@@ -119,6 +120,7 @@ Fixpoint str_of_num (n:nat) (m:nat):=
|_ => ""
end .
(*
Definition pp_token (token:Token) :=
match token with
| DLET => "Let"
......@@ -148,15 +150,18 @@ Fixpoint pp (tokList:list Token) :=
| token :: tokRest => str_join (pp_token token) (pp tokRest)
| [] => ""
end.
*)
(** Prefix form parser for expressions **)
Fixpoint parseExp (tokList:list Token) (fuel:nat):option (exp Q * list Token) :=
match fuel with
|S fuel' =>
match tokList with
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
if (m =? 0) then None else Some (Const (Z.of_nat n # Pos.of_nat m), tokRest)
| DVAR :: DCONST n :: tokRest => Some (Var Q n, tokRest)
match m with
|N0 => None
|Npos p => Some (Const (Z.of_N n # p), tokRest)
end
| DVAR :: DCONST n :: tokRest => Some (Var Q (N.to_nat n), tokRest)
| DNEG :: tokRest =>
match (parseExp tokRest fuel') with
| Some (Const c, tokRest) => Some (Const (- c), tokRest)
......@@ -225,7 +230,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* Parse it *)
match (parseLet letBodyRest fuel') with
(* And construct a result from it *)
| Some (letCmd, arbRest) => Some (Let n e letCmd, arbRest)
| Some (letCmd, arbRest) => Some (Let (N.to_nat n) e letCmd, arbRest)
| _ => None
end
(* But if we have a return *)
......@@ -233,7 +238,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* parse only this *)
match (parseRet retBodyRest fuel) with
(* and construct the result *)
| Some (retCmd, arbRest) => Some (Let n e retCmd, arbRest)
| Some (retCmd, arbRest) => Some (Let (N.to_nat n) e retCmd, arbRest)
| _ => None
end
| _ => None (* fail if there is no continuation for the let *)
......@@ -248,9 +253,15 @@ end.
Definition parseFrac (input:list Token) :option (Q * list Token) :=
match input with
| DNEG :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
if (m =? 0) then None else Some ((- Z.of_nat n # Pos.of_nat m),tokRest)
match m with
|N0 => None
|Npos p => Some ((- Z.of_N n # p),tokRest)
end
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
if (m =? 0) then None else Some ((Z.of_nat n # Pos.of_nat m),tokRest)
match m with
|N0 => None
|Npos p => Some ((Z.of_N n # p),tokRest)
end
| _ => None
end.
......@@ -282,8 +293,8 @@ Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list T
match parseIV fracRest with
| Some (iv, precondRest) =>
match parsePrecondRec precondRest fuel' with
| Some (P, tokRest) => Some (updPre n iv P, tokRest)
| None => Some (updPre n iv defaultPre, precondRest)
| Some (P, tokRest) => Some (updPre (N.to_nat n) iv P, tokRest)
| None => Some (updPre (N.to_nat n) iv defaultPre, precondRest)
end
| _ => None
end
......@@ -386,7 +397,7 @@ Fixpoint check_rec (input:list Token) (num_fun:nat) fuel:=
if CertificateCheckerCmd dCmd A P
then check_rec residual n' fuel
else "False\n"
| None => pp input(*"parse failure\n"*)
| None => "parse failure\n"
end
| _ => "failure num of functions given"
end.
......@@ -397,11 +408,35 @@ Fixpoint str_length s :=
|"" => O
end.
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) (n:nat) :=
match n with
|S n' => CertificateCheckerCmd f A P && (check f P A n')
|_ => true
end.
Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
match num_fun with
|S nf =>
match (dParse input fuel) with
|Some ((f,P,A), residual) =>
if (check f P A iters)
then
match residual with
|a :: b => check_all nf iters residual fuel
|[] => "True"
end
else
"False"
|None => "Failure: Parse"
end