diff options
| author | Brian Campbell | 2019-07-31 15:16:17 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-07-31 16:43:51 +0100 |
| commit | 2b64d1215c7b77d8cc37a4ab3c9ff2cc5a07e12b (patch) | |
| tree | b791c70a987fdad72fa7e1be15dea01f303fe32a /lib/coq/Sail2_prompt.v | |
| parent | 98cced7ef3cf89333e0e09d4ebf9ca3262b4e947 (diff) | |
Coq: reasoning for until loops
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
Diffstat (limited to 'lib/coq/Sail2_prompt.v')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index b5e94e46..79bf87eb 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -149,7 +149,8 @@ Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool else returnm vars else Fail "Termination limit reached". -Definition whileMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := +Definition whileMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := + let limit := measure vars in whileMT' limit vars cond body (Zwf_guarded limit). (*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> @@ -161,7 +162,8 @@ Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool if cond_val then returnm vars else untilMT' (limit - 1) vars cond body (_limit_reduces acc) else Fail "Termination limit reached". -Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := +Definition untilMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := + let limit := measure vars in untilMT' limit vars cond body (Zwf_guarded limit). (*let write_two_regs r1 r2 vec = |