From dbf31b37955a0f2bba36e5b1ac807469e70411c6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 30 Aug 2022 19:03:05 -0400 Subject: [PATCH 1/6] ToCString: avoid name collisions in declaratins --- bedrock2/src/bedrock2/ToCString.v | 36 ++++++++++++----------- bedrock2/src/bedrock2Examples/lightbulb.v | 2 ++ 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/bedrock2/src/bedrock2/ToCString.v b/bedrock2/src/bedrock2/ToCString.v index ca1bac41f..2b5c652b2 100644 --- a/bedrock2/src/bedrock2/ToCString.v +++ b/bedrock2/src/bedrock2/ToCString.v @@ -133,6 +133,22 @@ Fixpoint c_cmd (indent : string) (c : cmd) : string := indent ++ c_act binds action (List.map c_expr es) end. +Definition rename_away_from x xs := + let x' := "_" ++ x in + if List.existsb (String.eqb x') xs + then "#error rename_away_from '" ++ x ++"' = '" ++ x' ++"'" + else x'. + +Fixpoint rename_outs (outs : list String.string) (used : list String.string) : list (String.string*String.string) * list String.string := + match outs with + | cons o outs' => + let rec := rename_outs outs' used in + let (outrenames, used) := (fst rec, snd rec) in + let optr := rename_away_from o used in + (cons (o, optr) outrenames, cons o used) + | nil => (nil, used) + end. + Definition fmt_c_decl (rett : string) (args : list String.string) (name : String.string) (retptrs : list String.string) : string := let argstring : String.string := (match args, retptrs with @@ -148,25 +164,11 @@ Definition c_decl (f : String.string * (list String.string * list String.string let '(name, (args, rets, body)) := f in match rets with | nil => fmt_c_decl "void" args name nil - | cons _ _ => fmt_c_decl "uintptr_t" args name (List.removelast rets) + | cons _ _ => + let retrenames := fst (rename_outs (List.removelast rets) (cmd.vars body)) in + fmt_c_decl "uintptr_t" args name (List.map snd retrenames) end ++ ";". -Definition rename_away_from x xs := - let x' := "_" ++ x in - if List.existsb (String.eqb x') xs - then "#error rename_away_from '" ++ x ++"' = '" ++ x' ++"'" - else x'. - -Fixpoint rename_outs (outs : list String.string) (used : list String.string) : list (String.string*String.string) * list String.string := - match outs with - | cons o outs' => - let rec := rename_outs outs' used in - let (outrenames, used) := (fst rec, snd rec) in - let optr := rename_away_from o used in - (cons (o, optr) outrenames, cons o used) - | nil => (nil, used) - end. - (* `globals` is a list of varnames that should be treated as global variables, that is, they are removed from the list of local declarations, and it is diff --git a/bedrock2/src/bedrock2Examples/lightbulb.v b/bedrock2/src/bedrock2Examples/lightbulb.v index 12fa8dfe6..b9d02af0a 100644 --- a/bedrock2/src/bedrock2Examples/lightbulb.v +++ b/bedrock2/src/bedrock2Examples/lightbulb.v @@ -654,11 +654,13 @@ Section WithParameters. (* Print Assumptions link_lightbulb. *) + (* From bedrock2 Require Import ToCString. Goal True. let c_code := eval cbv in ((* of_string *) (c_module function_impls)) in pose c_code. Abort. + *) (* From bedrock2 Require Import ToCString Byte Bytedump. From 149e447fd4df5750b853a24138f75472c3081590 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 30 Aug 2022 19:04:04 -0400 Subject: [PATCH 2/6] LAN9250 tx (memory safety proof only) --- bedrock2/src/bedrock2Examples/LAN9250.v | 116 ++++++++++++++++++ .../src/bedrock2Examples/lightbulb_spec.v | 1 + 2 files changed, 117 insertions(+) diff --git a/bedrock2/src/bedrock2Examples/LAN9250.v b/bedrock2/src/bedrock2Examples/LAN9250.v index 566e959e7..aa9ce4a67 100644 --- a/bedrock2/src/bedrock2Examples/LAN9250.v +++ b/bedrock2/src/bedrock2Examples/LAN9250.v @@ -110,6 +110,22 @@ Definition lan9250_init : function := unpack! err = lan9250_writeword($0x070, coq:(Z.lor (Z.shiftl 1 2) (Z.shiftl 1 1))) ))). +Definition lan9250_tx : function := + ("lan9250_tx", (("p"::"l"::nil), ("err"::nil), bedrock_func_body:( + (* A: first segment, last segment, length *) + unpack! err = lan9250_writeword($lightbulb_spec.TX_DATA_FIFO, $(2^13)|$(2^12)|l); + require !err; + (* B: length *) + unpack! err = lan9250_writeword($lightbulb_spec.TX_DATA_FIFO, l); + require !err; + while ($3 < l) { + unpack! err = lan9250_writeword($lightbulb_spec.TX_DATA_FIFO, load4(p)); + if err { l = $0 } else { + p = p + $4; + l = l - $4 + }} + ))). + Require Import bedrock2.ProgramLogic. Require Import bedrock2.FE310CSemantics. Require Import coqutil.Word.Interface. @@ -759,4 +775,104 @@ Section WithParameters. all : rewrite ?Z.shiftl_mul_pow2 by blia. all : try (Z.div_mod_to_equations; blia). Qed. + + Require Import bedrock2.ZnWords. + + Import WeakestPrecondition SeparationLogic Array Scalars ProgramLogic.Coercions. + Global Instance spec_of_lan9250_tx : ProgramLogic.spec_of "lan9250_tx" := + fnspec! "lan9250_tx" p l / bs R ~> err, + { requires t m := word.unsigned l = length bs /\ + word.unsigned l mod 4 = 0 /\ + (array ptsto (word.of_Z 1) p bs * R)%sep m; + ensures t' m' := m' = m /\ (fun _ => True) t }. + + Import symmetry autoforward. + + Lemma lan9250_tx_ok : program_logic_goal_for_function! lan9250_tx. + Proof. + + repeat (subst || straightline || straightline_call || ZnWords || intuition idtac || esplit). + repeat (straightline || esplit). + straightline_call; [ZnWords|]; repeat (intuition idtac; repeat straightline). + 1 : eexists; split; repeat (straightline; intuition idtac; eauto). + eexists; split; repeat (straightline; intuition idtac; eauto). + + refine (Loops.tailrec_earlyout + (HList.polymorphic_list.cons (list Byte.byte) (HList.polymorphic_list.cons (mem -> Prop) HList.polymorphic_list.nil)) + ["p";"l";"err"] + (fun v bs R t m p l err => PrimitivePair.pair.mk ( + word.unsigned l = length bs /\ + word.unsigned l mod 4 = 0 /\ + (array ptsto (word.of_Z 1) p bs * R)%sep m /\ + v = word.unsigned l + ) + (fun T M P L ERR => + M = m + ) + ) _ (Z.lt_wf 0) _ _ _ _ _ _); + (* TODO wrap this into a tactic with the previous refine? *) + cbn [HList.hlist.foralls HList.tuple.foralls + HList.hlist.existss HList.tuple.existss + HList.hlist.apply HList.tuple.apply + HList.hlist + List.repeat Datatypes.length + HList.polymorphic_list.repeat HList.polymorphic_list.length + PrimitivePair.pair._1 PrimitivePair.pair._2] in *. + { repeat straightline. } + { repeat straightline; eauto. } + { repeat straightline. + subst br. + rename l into l0. + rename x8 into l. + rewrite word.unsigned_ltu in H16. + destr.destr Z.ltb. + 2: { contradiction H16. rewrite word.unsigned_of_Z_0; trivial. } + pose proof word.unsigned_range l as Hl. rewrite H13 in Hl. + eapply (f_equal word.of_Z) in H13. rewrite word.of_Z_unsigned in H13. + rewrite word.unsigned_of_Z in E; cbv [word.wrap] in E; rewrite Z.mod_small in E by blia. + subst l. + rename bs into bs0. + rename x5 into bs. + rewrite <-(firstn_skipn 4 bs) in H15. + seprewrite_in @array_append H15. + seprewrite_in @scalar32_of_bytes H15. + { autoforward with typeclass_instances in E. + rewrite firstn_length. ZnWords. } + + eexists; split; repeat straightline. + straightline_call; repeat straightline. + { ZnWords. } + + seprewrite_in (symmetry! @scalar32_of_bytes) H15. + { autoforward with typeclass_instances in E. + rewrite firstn_length. ZnWords. } + + eexists; split; repeat straightline; intuition idtac. + { seprewrite_in (symmetry! @array_append) H15. + rewrite (firstn_skipn 4 bs) in H15. + repeat straightline. + left; repeat straightline. + subst l br. + rewrite word.unsigned_ltu; rewrite ?word.unsigned_of_Z; cbn; ZnWords. } + + autoforward with typeclass_instances in E. + repeat straightline. + right; repeat straightline. + subst l p. + Set Printing Coercions. + rewrite word.unsigned_of_Z_1, Z.mul_1_l, firstn_length, min_l in H15 by ZnWords. + progress change (Z.of_nat 4) with 4%Z in H15. + eexists _, _, _; split; intuition eauto. + 3: ecancel_assumption. + 1: rewrite skipn_length; ZnWords. + 1 : ZnWords. + split; repeat straightline. + ZnWords. } + + { repeat straightline. + eauto. } + + Unshelve. + all : constructor. + Qed. End WithParameters. diff --git a/bedrock2/src/bedrock2Examples/lightbulb_spec.v b/bedrock2/src/bedrock2Examples/lightbulb_spec.v index b58f8c996..b411944d8 100644 --- a/bedrock2/src/bedrock2Examples/lightbulb_spec.v +++ b/bedrock2/src/bedrock2Examples/lightbulb_spec.v @@ -100,6 +100,7 @@ Section LightbulbSpec. Definition LAN9250_WRITE : byte := Byte.x02. Definition HW_CFG : Z := 0x074. + Definition TX_DATA_FIFO : Z := 0x20. Definition lan9250_write4 (a v : word) t := exists a0 a1 b0 b1 b2 b3, ( From 42c8d3e143773b7ed109c59cab8a10d5e4337e75 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 31 Aug 2022 12:35:20 -0400 Subject: [PATCH 3/6] bytedump.sh: ulimit -s unlimited --- etc/bytedump.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/etc/bytedump.sh b/etc/bytedump.sh index 4f217ebd3..c19cf42f0 100755 --- a/etc/bytedump.sh +++ b/etc/bytedump.sh @@ -1,5 +1,6 @@ #/bin/sh set -eu +ulimit -s unlimited { coqtop -q -quiet $COQFLAGS 2>/dev/null << EOF From 876ab37897562b85d97e49e8cd8c057ef069fffb Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 4 Sep 2022 14:57:29 -0400 Subject: [PATCH 4/6] compiler.ToplevelLoop: fix symbols --- compiler/src/compiler/ToplevelLoop.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/compiler/src/compiler/ToplevelLoop.v b/compiler/src/compiler/ToplevelLoop.v index 52686b32f..483e4906e 100644 --- a/compiler/src/compiler/ToplevelLoop.v +++ b/compiler/src/compiler/ToplevelLoop.v @@ -127,6 +127,8 @@ Section Pipeline1. | None => error:("No function named" "loop" "found") end;; let to_prepend := init_sp_insts ++ init_insts init_fun_pos ++ loop_insts loop_fun_pos ++ backjump_insts in + let adjust := Z.add (4 * Z.of_nat (length to_prepend)) in + let positions := map.fold (fun m f p => map.put m f (adjust p)) map.empty positions in Success (to_prepend ++ functions_insts, positions, required_stack_space). Context (spec: ProgramSpec). @@ -259,7 +261,7 @@ Section Pipeline1. - eapply runsToDone. split; [exact I|reflexivity]. } match goal with - | H: map.get positions "init"%string = Some ?pos |- _ => + | H: map.get ?positions "init"%string = Some ?pos |- _ => rename H into GetPos, pos into f_entry_rel_pos end. subst. @@ -368,7 +370,7 @@ Section Pipeline1. rewrite map.get_put_same. unfold init_sp. rewrite word.of_Z_unsigned. reflexivity. - cbv beta. unfold ll_good. intros. fwd. match goal with - | _: map.get positions "loop"%string = Some ?z |- _ => rename z into f_loop_rel_pos + | _: map.get ?positions "loop"%string = Some ?z |- _ => rename z into f_loop_rel_pos end. unfold compile_prog in CP. fwd. repeat match goal with From f5a4310755e4202534eb050658f4c5447e6967bc Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 5 Sep 2022 12:50:22 -0400 Subject: [PATCH 5/6] compiler: print symbols in gcc-compatible format --- compiler/src/compiler/Symbols.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 compiler/src/compiler/Symbols.v diff --git a/compiler/src/compiler/Symbols.v b/compiler/src/compiler/Symbols.v new file mode 100644 index 000000000..a834837d9 --- /dev/null +++ b/compiler/src/compiler/Symbols.v @@ -0,0 +1,24 @@ +Require Import Coq.Strings.String Coq.Strings.HexString. +Require Import Coq.Init.Byte coqutil.Byte. +Require Import Coq.Lists.List. +Require Import coqutil.Map.Interface. +Require Import coqutil.Map.Z_keyed_SortedListMap. +Local Open Scope string_scope. +Local Open Scope list_scope. +Import ListNotations. +Local Coercion String.list_byte_of_string : string >-> list. + +(* USAGE: +Definition mysymbols := Symbols.symbols myfinfo. +./etc/bytedump.sh MyRepo.MyFile.mysymbols > /tmp/l.s +riscv64-elf-gcc -T mylinkerscript.lds -g -nostdlib /tmp/l.s -o /tmp/l +*) + +Definition symbols {map : map.map string BinNums.Z} (finfo : map) : list byte := + "globl _start" ++ [x0a] ++ + "_start:" ++ [x0a] ++ + List.flat_map (A:=_*string) (fun '(a, s) => + ".org " ++ HexString.of_Z a ++ [x0a] ++ + ".local " ++ s ++ [x0a] ++ + s ++ ":" ++ [x0a]) + (SortedList.value (map.fold (fun m k v => map.put m v k) map.empty finfo)). From 83f58f4010e1952b7d07e7abbd1d687aa75721e1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 4 Sep 2022 23:01:51 -0400 Subject: [PATCH 6/6] memmove --- bedrock2/src/bedrock2Examples/memmove.v | 382 +++++++++++++++++++++++- deps/coqutil | 2 +- 2 files changed, 377 insertions(+), 7 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/memmove.v b/bedrock2/src/bedrock2Examples/memmove.v index d811f214e..3e2b394cf 100644 --- a/bedrock2/src/bedrock2Examples/memmove.v +++ b/bedrock2/src/bedrock2Examples/memmove.v @@ -6,6 +6,9 @@ Local Open Scope string_scope. Local Open Scope Z_scope. Local Open Scope list_s Require Import bedrock2.WeakestPrecondition bedrock2.Semantics bedrock2.ProgramLogic. Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. Require Import coqutil.Map.Interface bedrock2.Map.SeparationLogic. +Require Import bedrock2.ZnWords. +Import Coq.Init.Byte coqutil.Byte. +Local Notation string := String.string. (*Require Import bedrock2.ptsto_bytes.*) Require Import coqutil.Map.OfListWord. @@ -14,15 +17,382 @@ Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment Section WithParameters. Context {width} {BW: Bitwidth width}. - Context {word: word.word width} {mem: map.map word Byte.byte} {locals: map.map String.string word}. + Context {word: word.word width} {mem: map.map word byte} {locals: map.map string word}. Context {ext_spec: ExtSpec}. - Context {word_ok: word.ok word} {mem_ok: map.ok mem}. Import ProgramLogic.Coercions. - Instance spec_of_memmove : spec_of "memmove" := - fnspec! "memmove" dst src (n : word) / d s R Rs, + Local Instance spec_of_memmove : spec_of "memmove" := + fnspec! "memmove" (dst src n : word) / (d s : list byte) (R Rs : mem -> Prop), { requires t m := m =* s$@src * Rs /\ m =* d$@dst * R /\ - length s = n :> Z /\ length d = n :> Z /\ n < 2^(width-1); - ensures t' m' := t=t' /\ sep (eq(s$@dst)) R m }. + length s = n :> Z /\ length d = n :> Z /\ n <= 2^(width-1); + ensures t' m := m =* s$@dst * R /\ t=t' }. + + + Definition memmove : Syntax.func := + ("memmove", (["dst"; "src"; "n"], [], bedrock_func_body:( + x = src-dst; + require x; + if x < x+n { + while n { + store1(dst, load1(src)); + src = src + $1; + dst = dst + $1; + n = n - $1 + } + } else { + dst = dst + (n - $1); + src = src + (n - $1); + while n { + store1(dst, load1(src)); + src = src - $1; + dst = dst - $1; + n = n - $1 + } + } + ))). + + + Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals} + {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env} + {ext_spec_ok : ext_spec.ok ext_spec}. + + Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward. + Require Import coqutil.Word.Properties coqutil.Map.Properties. + + Local Ltac ZnWords := destruct width_cases; bedrock2.ZnWords.ZnWords. + Lemma memmove_ok : program_logic_goal_for_function! memmove. + Proof. + repeat straightline. + + case H as (ms&mRs&?&?&?), H0 as (md&mRd&?&?&?); + cbv [sepclause_of_map] in *; subst; clear dependent Rs. + + eapply WeakestPreconditionProperties.dexpr_expr. + repeat straightline. + letexists; split. + { subst l; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + letexists; split. + { subst l; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + repeat straightline. + + set (x := word.sub src dst) in *. + unfold1_cmd_goal; cbv beta match delta [cmd_body]. + eapply WeakestPreconditionProperties.dexpr_expr. + letexists; split. + { subst l0; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + repeat straightline. + + (* x = 0 *) + split; intros Hx; cycle 1. + { replace src with dst in * by ZnWords. + cbn; ssplit; eauto. + eexists _, _; ssplit; eauto. + eapply map.split_same_footprint; eauto. + intros k. + rewrite 2map.get_of_list_word_at, 2List.nth_error_None. + Morphisms.f_equiv. ZnWords. } + + unfold1_cmd_goal; cbv beta match delta [cmd_body]. + eapply WeakestPreconditionProperties.dexpr_expr. + letexists; split. + { subst l0; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + repeat straightline. + letexists; split. + { subst l0; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + letexists; split. + { subst l0 l; rewrite ?Properties.map.get_put_dec. exact eq_refl. } + repeat straightline. + + rewrite word.unsigned_ltu, word.unsigned_add; cbv [word.wrap]. + split; intros Hbr; + [apply word.if_nonzero in Hbr | apply word.if_zero in Hbr]; + autoforward with typeclass_instances in Hbr. + + { assert (x + n < 2^width) by ZnWords. + refine ((Loops.tailrec + (HList.polymorphic_list.cons _ + (HList.polymorphic_list.cons _ + (HList.polymorphic_list.cons _ + (HList.polymorphic_list.cons _ + HList.polymorphic_list.nil)))) + ["dst";"src";"n";"x"]) + (fun (v:nat) s mRs d mRd t m dst src n _x => PrimitivePair.pair.mk ( + x + n < 2^width /\ map.split m (s$@src) mRs /\ map.split m (d$@dst) mRd /\ + x = word.sub src dst /\ v=n :> Z /\ length s = n :> Z /\ length d = n :> Z + ) + (fun T M DST SRC N X => t = T /\ map.split M (s$@dst) mRd)) + lt + _ _ _ _ _ _ _ _ _); + (* TODO wrap this into a tactic with the previous refine *) + cbn [HList.hlist.foralls HList.tuple.foralls + HList.hlist.existss HList.tuple.existss + HList.hlist.apply HList.tuple.apply + HList.hlist + List.repeat Datatypes.length + HList.polymorphic_list.repeat HList.polymorphic_list.length + PrimitivePair.pair._1 PrimitivePair.pair._2] in *. + { cbv [Loops.enforce]; cbn. + subst l l0. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn); split. + { exact eq_refl. } + { eapply map.map_ext; intros k. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]). + repeat (destruct String.eqb; trivial). } } + { eapply Wf_nat.lt_wf. } + { cbn; ssplit; eauto. } + { intros ?v ?s ?mRs ?d ?mRd ?t ?m ?dst ?src ?n ?x. + repeat straightline. + cbn in localsmap. + eexists n0; split; cbv [expr expr_body localsmap get]. + { rewrite ?Properties.map.get_put_dec. exists n0; cbn. auto. } + split; cycle 1. + { intros Ht; rewrite Ht in *. + intuition idtac; destruct s0, d0; cbn in *; try discriminate; []. + eauto. } + repeat straightline. + eapply WeakestPreconditionProperties.dexpr_expr. + repeat straightline. + letexists; split. + { rewrite ?Properties.map.get_put_dec; exact eq_refl. } + eapply WeakestPreconditionProperties.dexpr_expr. + repeat straightline. + letexists; split. + { rewrite ?Properties.map.get_put_dec; cbn. exact eq_refl. } + repeat straightline. + + cbv [WeakestPrecondition.load load load_Z]; cbn. + destruct s0 as [|b s0], d0 as [|B d0]; try (cbn in *; congruence); []. + exists (word.of_Z (byte.unsigned b)). + pose proof map.get_split src0 _ _ _ H6. + rewrite map.get_of_list_word_at in H14. + progress replace (Z.to_nat (word.sub src0 src0)) with O in H14 by ZnWords; + cbn in H14; case H14 as [[? ?]|[? ?]]; try discriminate. + rewrite H14. split. { rewrite LittleEndianList.le_combine_1. trivial. } + + cbv [WeakestPrecondition.store load load_Z load_bytes store store_Z store_bytes unchecked_store_bytes LittleEndianList.le_split]; cbn. + pose proof map.get_split dst0 _ _ _ H8. + rewrite map.get_of_list_word_at in H16. + progress replace (Z.to_nat (word.sub dst0 dst0)) with O in H16 by ZnWords; + cbn in H16; case H16 as [[? ?]|[? ?]]; try discriminate. + eexists. rewrite H16. split. + { rewrite word.unsigned_of_Z, Scalars.wrap_byte_unsigned. + rewrite byte.of_Z_unsigned; trivial. } + + eapply map.split_remove_put in H6; [|eapply H14]. + eapply map.split_remove_put in H8; [|eapply H16]. + rewrite map.remove_head_of_list_word_at_cons in H6,H8 by (cbn in *; ZnWords). + assert (map.split (map.put m0 dst0 b) (s0$@(word.add src0 (word.of_Z 1))) (map.put (map.put mRs0 src0 b) dst0 b)). + { eapply map.split_put_None; trivial. + rewrite map.get_of_list_word_at, List.nth_error_None. + cbn in *; ZnWords. } + assert (map.split (map.put m0 dst0 b) (d0$@(word.add dst0 (word.of_Z 1))) (map.put mRd0 dst0 b)). + { rewrite <-map.put_put_same with (m:=mRd0) (v1 := B). + eapply map.split_put_Some; rewrite ?map.get_put_same; eauto. } + + cbv [get literal dlet.dlet]. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). + eexists. + eexists. + { eauto. } + eexists. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). + eexists. + { eauto. } + eexists. + eexists. + { eauto. } + eexists _, _, _, _. + split. + { cbv [Loops.enforce]; cbn. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn); split. + { exact eq_refl. } + { eapply map.map_ext; intros k. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]). + repeat (destruct String.eqb; trivial). } } + eexists _, _, _, _, (length s0); split; ssplit. + { ZnWords. } + { eassumption. } + { eassumption. } + { ZnWords. } + { cbn in *; ZnWords. } + { cbn in *; ZnWords. } + { cbn in *; ZnWords. } + split. + { cbn in *; ZnWords. } + intuition idtac; repeat straightline_cleanup. + eapply map.split_put_r2l in H22; trivial. + rewrite <-map.of_list_word_at_cons in H22. exact H22. } + { cbn. intuition idtac. eexists _, _; ssplit; eauto. } } + + { assert (n <= x) by ZnWords. + + unfold1_cmd_goal; cbv beta match delta [cmd_body]. + eapply WeakestPreconditionProperties.dexpr_expr. + repeat straightline. + letexists; split. + { subst l0 l; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + letexists; split. + { subst l0 l; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + repeat straightline. + + eapply WeakestPreconditionProperties.dexpr_expr. + repeat straightline. + letexists; split. + { subst l1 l0 l; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + letexists; split. + { subst l1 l0 l; rewrite ?Properties.map.get_put_dec; exact eq_refl. } + repeat straightline. + + refine ((Loops.tailrec + (HList.polymorphic_list.cons _ + (HList.polymorphic_list.cons _ + (HList.polymorphic_list.cons _ + (HList.polymorphic_list.cons _ + HList.polymorphic_list.nil)))) + ["dst";"src";"n";"x"]) + (fun (v:nat) s mRs d mRd t m dst src n _x => PrimitivePair.pair.mk ( + n <= x /\ map.split m (s$@(word.sub src (word.sub n (word.of_Z 1)))) mRs /\ + map.split m (d$@(word.sub dst (word.sub n (word.of_Z 1)))) mRd /\ + x = word.sub src dst /\ v=n :> Z /\ length s = n :> Z /\ length d = n :> Z + ) + (fun T M DST SRC N X => t = T /\ map.split M (s$@(word.sub dst (word.sub n (word.of_Z 1)))) mRd)) + lt + _ _ _ _ _ _ _ _ _); + (* TODO wrap this into a tactic with the previous refine *) + cbn [HList.hlist.foralls HList.tuple.foralls + HList.hlist.existss HList.tuple.existss + HList.hlist.apply HList.tuple.apply + HList.hlist + List.repeat Datatypes.length + HList.polymorphic_list.repeat HList.polymorphic_list.length + PrimitivePair.pair._1 PrimitivePair.pair._2] in *. + { cbv [Loops.enforce]; cbn. + subst l l0 l1 l2. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn); split. + { exact eq_refl. } + { eapply map.map_ext; intros k. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]). + repeat (destruct String.eqb; trivial). } } + { eapply Wf_nat.lt_wf. } + { cbn. subst v0 v. rewrite !word.word_sub_add_l_same_r. ssplit; eauto. ZnWords. } + { intros ?v ?s ?mRs ?d ?mRd ?t ?m ?dst ?src ?n ?x. + repeat straightline. + cbn in localsmap. + eexists n0; split; cbv [expr expr_body localsmap get]. + { rewrite ?Properties.map.get_put_dec. exists n0; cbn. auto. } + split; cycle 1. + { intros Ht; rewrite Ht in *. + intuition idtac; destruct s0, d0; cbn in *; try discriminate; []. + rewrite map.of_list_word_nil in *; trivial. } + repeat straightline. + eapply WeakestPreconditionProperties.dexpr_expr. + repeat straightline. + letexists; split. + { rewrite ?Properties.map.get_put_dec; exact eq_refl. } + eapply WeakestPreconditionProperties.dexpr_expr. + repeat straightline. + letexists; split. + { rewrite ?Properties.map.get_put_dec; cbn. exact eq_refl. } + repeat straightline. + + cbv [WeakestPrecondition.load load load_Z]; cbn. + destruct (@List.exists_last _ s0) as (s0'&b&H's) in *. + { intro. subst. cbn in *. ZnWords. } + destruct (@List.exists_last _ d0) as (d0'&B&H'd) in *. + { intro. subst. cbn in *. ZnWords. } + subst s0 d0; rename s0' into s0; rename d0' into d0; rewrite List.app_length in *; cbn [List.length] in *. + exists (word.of_Z (byte.unsigned b)). + pose proof map.get_split src0 _ _ _ H6. + rewrite !map.get_of_list_word_at, !List.nth_error_app2 in H14 by ZnWords. + match goal with H : context[List.nth_error [_] ?i = None] |- _ => + replace i with O in H by ZnWords; cbn [List.nth_error] in H end. + cbn in H14; case H14 as [[? ?]|[? ?]]; try discriminate. + rewrite H14. split. { rewrite LittleEndianList.le_combine_1. trivial. } + + cbv [WeakestPrecondition.store load load_Z load_bytes store store_Z store_bytes unchecked_store_bytes LittleEndianList.le_split]; cbn. + pose proof map.get_split dst0 _ _ _ H8. + rewrite !map.get_of_list_word_at, !List.nth_error_app2 in H16 by ZnWords. + match goal with H : context[List.nth_error [_] ?i = None] |- _ => + replace i with O in H by ZnWords; cbn [List.nth_error] in H end. + case H16 as [[? ?]|[? ?]]; try discriminate. + eexists. rewrite H16. split. + { rewrite word.unsigned_of_Z, Scalars.wrap_byte_unsigned. + rewrite byte.of_Z_unsigned; trivial. } + + eapply map.split_remove_put in H6; [|eapply H14]. + eapply map.split_remove_put in H8; [|eapply H16]. + rewrite !map.remove_last_of_list_word_at_snoc in H6,H8 by ZnWords. + assert (map.split (map.put m0 dst0 b) (s0$@(word.sub src0 (word.sub n0 (word.of_Z 1)))) (map.put (map.put mRs0 src0 b) dst0 b)). + { eapply map.split_put_None; trivial. + rewrite map.get_of_list_word_at, List.nth_error_None. + cbn in *; ZnWords. } + assert (map.split (map.put m0 dst0 b) (d0$@(word.sub dst0 (word.sub n0 (word.of_Z 1)))) (map.put mRd0 dst0 b)). + { rewrite <-map.put_put_same with (m:=mRd0) (v1 := B). + eapply map.split_put_Some; rewrite ?map.get_put_same; eauto. } + + cbv [get literal dlet.dlet]. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). + eexists. + eexists. + { eauto. } + eexists. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). + eexists. + { eauto. } + eexists. + eexists. + { eauto. } + eexists _, _, _, _. + split. + { cbv [Loops.enforce]; cbn. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn); split. + { exact eq_refl. } + { eapply map.map_ext; intros k. + repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]). + repeat (destruct String.eqb; trivial). } } + eexists _, _, _, _, (length s0); split; ssplit. + { ZnWords. } + { replace (word.sub (word.sub src0 (word.of_Z 1))(word.sub (word.sub n0 (word.of_Z 1)) (word.of_Z 1))) + with (word.sub src0 (word.sub n0 (word.of_Z 1))) by ZnWords. + eassumption. } + { replace (word.sub (word.sub dst0 (word.of_Z 1)) (word.sub (word.sub n0 (word.of_Z 1)) (word.of_Z 1))) + with (word.sub dst0 (word.sub n0 (word.of_Z 1))) by ZnWords. + eassumption. } + { ZnWords. } + { cbn in *; ZnWords. } + { cbn in *; ZnWords. } + { cbn in *; ZnWords. } + split. + { cbn in *; ZnWords. } + intuition idtac; repeat straightline_cleanup. + eapply map.split_put_r2l in H22; trivial. + rewrite map.of_list_word_at_snoc by ZnWords. + progress replace (word.add (word.sub dst0 (word.sub n0 (word.of_Z 1))) (word.of_Z (length s0))) with dst0 by ZnWords. + progress replace (word.sub (word.sub dst0 (word.of_Z 1)) (word.sub (word.sub n0 (word.of_Z 1)) (word.of_Z 1))) with (word.sub dst0 (word.sub n0 (word.of_Z 1))) in H22 by ZnWords. + exact H22. } + { cbn. intuition idtac. eexists _, _; ssplit; eauto. f_equal. ZnWords. } } + Qed. + + Require Import coqutil.Macros.symmetry. + Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a"). + Global Instance spec_of_memmove_array : spec_of "memmove" := + fnspec! "memmove" (dst src n : word) / (d s : list byte) (R Rs : mem -> Prop), + { requires t m := m =* s$@src * Rs /\ m =* d$@dst * R /\ + length s = n :> Z /\ length d = n :> Z /\ n <= 2^(width-1); + ensures t' m := m =* s$@dst * R /\ t=t' }. + + Lemma memmove_ok_array : program_logic_goal_for_function! memmove. + Proof. + cbv [program_logic_goal_for spec_of_memmove_array]; intros. + eapply WeakestPreconditionProperties.Proper_call; cycle 1; [eapply memmove_ok|]; + cbv [sepclause_of_map] in *. + { intuition idtac. + - seprewrite_in_by @ptsto_bytes.array1_iff_eq_of_list_word_at H0 ZnWords; eassumption. + - seprewrite_in_by @ptsto_bytes.array1_iff_eq_of_list_word_at H ZnWords; eassumption. + - trivial. + - trivial. } + { intros ? ? ? ?. intuition idtac. + seprewrite_in_by (symmetry! @ptsto_bytes.array1_iff_eq_of_list_word_at) H2 ZnWords; eassumption. } + Qed. End WithParameters. diff --git a/deps/coqutil b/deps/coqutil index 55ac16f58..0a3b94015 160000 --- a/deps/coqutil +++ b/deps/coqutil @@ -1 +1 @@ -Subproject commit 55ac16f58905ac54bc38b2ac5d96a81d92c9d572 +Subproject commit 0a3b94015852b001fa7206800ece3a043c9a265c