From e4edfe6242c1f87bcae3beb17c398486b525dd77 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Thu, 6 May 2021 20:53:16 +0100 Subject: Prove a spec for the mapping of function params Extracted the traversal of call args into a function and gave it a spec, so that it can be used to prove the overall spec for the Icall instruction. --- src/common/Monad.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'src/common') diff --git a/src/common/Monad.v b/src/common/Monad.v index 68233b1..c9cdc1a 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -50,19 +50,18 @@ Module MonadExtra(M : Monad). End MonadNotation. Import MonadNotation. - Fixpoint sequence {A: Type} (l: list (mon A)) {struct l}: mon (list A) := + Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := match l with | nil => ret nil | x::xs => - do r <- x; - do rs <- sequence xs; + do r <- f x; + do rs <- traverselist f xs; ret (r::rs) end. - Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := - sequence (map f l). + Definition sequence {A} : list (mon A) -> mon (list A) := traverselist (fun x => x). - Fixpoint traverseoption {A B: Type} (f: A -> mon B) (opt: option A) {struct opt}: mon (option B) := + Definition traverseoption {A B: Type} (f: A -> mon B) (opt: option A) : mon (option B) := match opt with | None => ret None | Some x => -- cgit