diff --git a/Makefile b/Makefile index 032453df5..cdf3f1310 100644 --- a/Makefile +++ b/Makefile @@ -158,7 +158,8 @@ clean_end2end: install_end2end: $(MAKE) -C $(ABS_ROOT_DIR)/end2end install -all: bedrock2_ex LiveVerif_ex LiveVerifEx64 compiler_ex processor end2end +# TODO re-enable end2end +all: bedrock2_ex LiveVerif_ex LiveVerifEx64 compiler_ex processor # end2end clean: clean_bedrock2 clean_LiveVerif clean_LiveVerifEx64 clean_compiler clean_processor clean_end2end diff --git a/bedrock2/src/bedrock2/MetricProgramLogic.v b/bedrock2/src/bedrock2/MetricProgramLogic.v index 813ad255f..3e93d5ada 100644 --- a/bedrock2/src/bedrock2/MetricProgramLogic.v +++ b/bedrock2/src/bedrock2/MetricProgramLogic.v @@ -240,8 +240,8 @@ Ltac straightline := let __ := match s with String.String _ _ => idtac | String.EmptyString => idtac end in ident_of_constr_string_cps s ltac:(fun x => ensure_free x; - (* NOTE: keep this consistent with the [exists _, _ /\ _] case far below *) - letexists _ as x; split; [solve [repeat straightline]|]) + (* NOTE: keep this consistent with the [exists _ _, _ /\ _] case far below *) + letexists _ as x; letexists; split; [solve [repeat straightline]|]) | |- cmd _ ?c _ _ _ _ ?post => let c := eval hnf in c in lazymatch c with @@ -250,7 +250,7 @@ Ltac straightline := | cmd.interact _ _ _ => fail | _ => unfold1_cmd_goal; cbv beta match delta [cmd_body] end - | |- @list_map _ _ (get _ _) _ _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body] + | |- @list_map _ _ (get _) _ _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body] | |- @list_map _ _ (expr _ _) _ _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body] | |- @list_map _ _ _ nil _ _ => cbv beta match fix delta [list_map list_map_body] | |- expr _ _ _ _ _ => unfold1_expr_goal; cbv beta match delta [expr_body] @@ -310,15 +310,20 @@ Ltac straightline := split; [solve [repeat straightline]|] (* NOTE: metrics only case; maybe try to unify with non-metrics? *) | |- exists x y, ?P /\ ?Q => - eexists; eexists; split; [solve [repeat straightline]|] - (* eexists instead of letexists ensures unification of (?a,?b) = (const,const) - does not unfold the const aggressively (e.g. word to Naive) *) - | |- exists x, Markers.split (?P /\ ?Q) => - let x := fresh x in refine (let x := _ in ex_intro (fun x => P /\ Q) x _); - split; [solve [repeat straightline]|] - | |- Markers.unique (exists x, Markers.split (?P /\ ?Q)) => - let x := fresh x in refine (let x := _ in ex_intro (fun x => P /\ Q) x _); - split; [solve [repeat straightline]|] + let x := fresh x in let y := fresh y in + refine (let x := _ in let y := _ in + ex_intro (fun x => exists y, P /\ Q) x (ex_intro (fun y => P /\ Q) y _)); + split; [solve [repeat straightline]|] + | |- exists x y, Markers.split (?P /\ ?Q) => + let x := fresh x in let y := fresh y in + refine (let x := _ in let y := _ in + ex_intro (fun x => exists y, P /\ Q) x (ex_intro (fun y => P /\ Q) y _)); + split; [solve [repeat straightline]|] + | |- Markers.unique (exists x y, Markers.split (?P /\ ?Q)) => + let x := fresh x in let y := fresh y in + refine (let x := _ in let y := _ in + ex_intro (fun x => exists y, P /\ Q) x (ex_intro (fun y => P /\ Q) y _)); + split; [solve [repeat straightline]|] | |- Markers.unique (Markers.left ?G) => change G; unshelve (idtac; repeat match goal with @@ -343,12 +348,12 @@ Ltac straightline := (* TODO: once we can automatically prove some calls, include the success-only version of this in [straightline] *) Ltac straightline_call := lazymatch goal with - | |- MetricWeakestPrecondition.call ?functions ?callee _ _ _ _ => + | |- MetricWeakestPrecondition.call ?functions ?callee _ _ _ _ _ => let callee_spec := lazymatch constr:(_:spec_of callee) with ?s => s end in let Hcall := lazymatch goal with H: callee_spec functions |- _ => H end in eapply MetricWeakestPreconditionProperties.Proper_call; cycle -1; [ eapply Hcall | try eabstract (solve [Morphisms.solve_proper]) .. ]; - [ .. | intros ? ? ? ?] + [ .. | intros ? ? ? ? ?] end. Ltac current_trace_mem_locals := diff --git a/bedrock2/src/bedrock2Examples/SPI.v b/bedrock2/src/bedrock2Examples/SPI.v index 479c16286..df90470b3 100644 --- a/bedrock2/src/bedrock2Examples/SPI.v +++ b/bedrock2/src/bedrock2Examples/SPI.v @@ -231,6 +231,7 @@ Section WithParameters. end. Lemma spi_read_ok : program_logic_goal_for_function! spi_read. + Proof. repeat straightline. refine ((atleastonce ["b"; "busy"; "i"] (fun v T M B BUSY I => v = word.unsigned I /\ word.unsigned I <> 0 /\ M = m /\ diff --git a/bedrock2/src/bedrock2Examples/metric_LAN9250.v b/bedrock2/src/bedrock2Examples/metric_LAN9250.v new file mode 100644 index 000000000..85a79c694 --- /dev/null +++ b/bedrock2/src/bedrock2Examples/metric_LAN9250.v @@ -0,0 +1,939 @@ +Require Import bedrock2.Syntax bedrock2.NotationsCustomEntry. +Require Import bedrock2.MetricLogging bedrock2.MetricCosts. +Require Import coqutil.Z.prove_Zeq_bitwise. +Require Import bedrock2Examples.metric_SPI. + +From coqutil Require Import letexists. +Require Import bedrock2.AbsintWordToZ. +Require Import coqutil.Tactics.rdelta. +Require Import coqutil.Z.div_mod_to_equations. +Require Import coqutil.Z.Lia. + +Import BinInt String List.ListNotations. +Local Open Scope Z_scope. Local Open Scope string_scope. Local Open Scope list_scope. + +Local Notation MMIOWRITE := "MMIOWRITE". +Local Notation MMIOREAD := "MMIOREAD". + +Definition lan9250_readword := func! (addr) ~> (ret, err) { + SPI_CSMODE_ADDR = ($0x10024018); + io! ret = MMIOREAD(SPI_CSMODE_ADDR); + ret = (ret | $2); + output! MMIOWRITE(SPI_CSMODE_ADDR, ret); + + (* manually register-allocated, apologies for variable reuse *) + unpack! ret, err = spi_xchg($0x0b); require !err; (* FASTREAD *) + unpack! ret, err = spi_xchg(addr >> $8); require !err; + unpack! ret, err = spi_xchg(addr & $0xff); require !err; + unpack! ret, err = spi_xchg(err); require !err; (* dummy *) + + unpack! ret, err = spi_xchg(err); require !err; (* read *) + unpack! addr, err = spi_xchg(err); require !err; (* read *) + ret = (ret | (addr << $8)); + unpack! addr, err = spi_xchg(err); require !err; (* read *) + ret = (ret | (addr << $16)); + unpack! addr, err = spi_xchg(err); require !err; (* read *) + ret = (ret | (addr << $24)); + + io! addr = $MMIOREAD(SPI_CSMODE_ADDR); + addr = (addr & coq:(Z.lnot 2)); + output! $MMIOWRITE(SPI_CSMODE_ADDR, addr) + }. + +Definition lan9250_writeword := func! (addr, data) ~> err { + SPI_CSMODE_ADDR = $0x10024018; + io! ret = $MMIOREAD(SPI_CSMODE_ADDR); + ret = (ret | $2); + output! $MMIOWRITE(SPI_CSMODE_ADDR, ret); + + (* manually register-allocated, apologies for variable reuse *) + Oxff = $0xff; + eight = $8; + unpack! ret, err = spi_xchg($0x02); require !err; (* FASTREAD *) + unpack! ret, err = spi_xchg(addr >> eight); require !err; + unpack! ret, err = spi_xchg(addr & Oxff); require !err; + + unpack! ret, err = spi_xchg(data & Oxff); require !err; (* write *) + data = (data >> eight); + unpack! ret, err = spi_xchg(data & Oxff); require !err; (* write *) + data = (data >> eight); + unpack! ret, err = spi_xchg(data & Oxff); require !err; (* write *) + data = (data >> eight); + unpack! ret, err = spi_xchg(data); require !err; (* write *) + + io! addr = $MMIOREAD(SPI_CSMODE_ADDR); + addr = (addr & coq:(Z.lnot 2)); + output! $MMIOWRITE(SPI_CSMODE_ADDR, addr) + }. + +Definition MAC_CSR_DATA : Z := 0x0A8. +Definition MAC_CSR_CMD : Z := 0x0A4. +Definition BYTE_TEST : Z := 0x64. + +Definition lan9250_mac_write := func! (addr, data) ~> err { + unpack! err = lan9250_writeword($MAC_CSR_DATA, data); + require !err; +unpack! err = lan9250_writeword($MAC_CSR_CMD, coq:(Z.shiftl 1 31)|addr); + require !err; + unpack! data, err = lan9250_readword($BYTE_TEST) + (* while (lan9250_readword(0xA4) >> 31) { } // Wait until BUSY (= MAX_CSR_CMD >> 31) goes low *) + }. + +Definition lan9250_wait_for_boot := func! () ~> err { + err = ($0); + byteorder = ($0); + i = ($lightbulb_spec.patience); while (i) { i = (i - $1); + unpack! byteorder, err = lan9250_readword($0x64); + if err { i = (i^i) } + else if (byteorder == $0x87654321) { i = (i^i) } + else { err = ($-1) } + } +}. + +Definition lan9250_init := func! () ~> err { + unpack! err = lan9250_wait_for_boot(); + require !err; + unpack! hw_cfg, err = lan9250_readword($lightbulb_spec.HW_CFG); + require !err; + hw_cfg = (hw_cfg | coq:(Z.shiftl 1 20)); (* mustbeone *) + hw_cfg = (hw_cfg & coq:(Z.lnot (Z.shiftl 1 21))); (* mustbezero *) + unpack! err = lan9250_writeword($lightbulb_spec.HW_CFG, hw_cfg); + require !err; + + (* 20: full duplex; 18: promiscuous; 2, 3: TXEN/RXEN *) + unpack! err = lan9250_mac_write($1, coq:(Z.lor (Z.shiftl 1 20) (Z.lor (Z.shiftl 1 18) (Z.lor (Z.shiftl 1 3) (Z.shiftl 1 2))))); + require !err; + unpack! err = lan9250_writeword($0x070, coq:(Z.lor (Z.shiftl 1 2) (Z.shiftl 1 1))) + }. + +Local Definition TX_DATA_FIFO := 32. +Definition lan9250_tx := func! (p, l) ~> err { + (* A: first segment, last segment, length *) + unpack! err = lan9250_writeword($TX_DATA_FIFO, $(2^13)|$(2^12)|l); require !err; + (* B: length *) + unpack! err = lan9250_writeword($TX_DATA_FIFO, l); require !err; + while ($3 < l) { + unpack! err = lan9250_writeword($TX_DATA_FIFO, load4(p)); + if err { l = $0 } else { p = p + $4; l = l - $4 } } }. + +Require Import bedrock2.MetricProgramLogic. +Require Import bedrock2.FE310CSemantics. +Require Import coqutil.Word.Interface. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.TracePredicate. Import TracePredicateNotations. +Require bedrock2Examples.lightbulb_spec. +Require Import bedrock2.ZnWords. + +Import coqutil.Map.Interface. +Import lightbulb_spec. +Import MetricLoops. + +Section WithParameters. + Context {word: word.word 32} {mem: map.map word Byte.byte}. + Context {word_ok: word.ok word} {mem_ok: map.ok mem}. + + Import lightbulb_spec. + Local Notation mmio_trace_abstraction_relation := (@mmio_trace_abstraction_relation word). + Local Notation only_mmio_satisfying := (@only_mmio_satisfying word mem). + + Global Instance spec_of_lan9250_readword : MetricProgramLogic.spec_of "lan9250_readword" := fun functions => forall t m a mc, + (0x0 <= Word.Interface.word.unsigned a < 0x400) -> + MetricWeakestPrecondition.call functions "lan9250_readword" t m [a] mc (fun T M RETS MC => + M = m /\ + exists ret err, RETS = [ret; err] /\ + exists iol, T = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned err <> 0 /\ (any +++ lightbulb_spec.spi_timeout _) ioh) + (word.unsigned err = 0 /\ lightbulb_spec.lan9250_fastread4 _ a ret ioh /\ + (MC - mc <= 24 * mc_spi_xchg_const + Z.of_nat (length ioh) * mc_spi_mul)%metricsH)). + + Global Instance spec_of_lan9250_writeword : MetricProgramLogic.spec_of "lan9250_writeword" := fun functions => + forall t m a mc v, + (0x0 <= Word.Interface.word.unsigned a < 0x400) -> + (((MetricWeakestPrecondition.call functions "lan9250_writeword"))) t m [a; v] mc + (fun T M RETS MC => + M = m /\ + exists err, RETS = [err] /\ + exists iol, T = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned err <> 0 /\ (any +++ lightbulb_spec.spi_timeout _) ioh) + (word.unsigned err = 0 /\ lightbulb_spec.lan9250_write4 _ a v ioh /\ + (MC - mc <= 21 * mc_spi_xchg_const + Z.of_nat (length ioh) * mc_spi_mul)%metricsH)). + + Global Instance spec_of_lan9250_mac_write : MetricProgramLogic.spec_of "lan9250_mac_write" := fun functions => + forall t m a mc v, + (0 <= Word.Interface.word.unsigned a < 2^31) -> + (((MetricWeakestPrecondition.call functions "lan9250_mac_write"))) t m [a; v] mc + (fun T M RETS MC => + M = m /\ + exists err, RETS = [err] /\ + exists iol, T = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned err <> 0 /\ (any +++ lightbulb_spec.spi_timeout _) ioh) + (word.unsigned err = 0 /\ lan9250_mac_write_trace _ a v ioh /\ + (MC - mc <= 4*21 * mc_spi_xchg_const + Z.of_nat (length ioh) * mc_spi_mul)%metricsH)). + + Global Instance spec_of_lan9250_wait_for_boot : MetricProgramLogic.spec_of "lan9250_wait_for_boot" := fun functions => + forall t m mc, + (((MetricWeakestPrecondition.call functions "lan9250_wait_for_boot"))) t m [] mc + (fun T M RETS MC => + M = m /\ + exists err, RETS = [err] /\ + exists iol, T = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned err <> 0 /\ (any +++ lightbulb_spec.spi_timeout _) ioh \/ + (word.unsigned err <> 0 /\ lan9250_boot_timeout _ ioh)) + (word.unsigned err = 0 /\ lan9250_wait_for_boot_trace _ ioh)). + + Global Instance spec_of_lan9250_init : MetricProgramLogic.spec_of "lan9250_init" := fun functions => + forall t m mc, + (((MetricWeakestPrecondition.call functions "lan9250_init"))) t m [] mc + (fun T M RETS MC => + M = m /\ + exists err, RETS = [err] /\ + exists iol, T = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned err <> 0 /\ (any +++ lightbulb_spec.spi_timeout _) ioh \/ + (word.unsigned err <> 0 /\ lan9250_boot_timeout _ ioh)) + (word.unsigned err = 0 /\ lan9250_init_trace _ ioh)). + + Local Ltac split_if := + lazymatch goal with + |- MetricWeakestPrecondition.cmd _ ?c _ _ _ _ ?post => + let c := eval hnf in c in + lazymatch c with + | cmd.cond _ _ _ => letexists; letexists; split; [solve[repeat straightline]|split] + end + end. + + Ltac evl := (* COQBUG(has_variable) *) + repeat match goal with + | |- context G[string_dec ?x ?y] => + let e := eval cbv in (string_dec x y) in + let goal := context G [e] in + change goal + | |- context G[word.unsigned ?x] => + let x := rdelta x in + let x := lazymatch x with word.of_Z ?x => x end in + let x := rdelta x in + let x := rdelta x in + requireZcst x; + let x := eval cbv in x in + let goal := context G [x] in + change goal + | |- context G [app nil ?xs] => + let goal := context G [ xs ] in + change goal + end. + + Ltac trace_alignment := + repeat (eapply lightbulb_spec.align_trace_app + || eapply lightbulb_spec.align_trace_cons + || exact (eq_refl (app nil _))). + + Ltac mmio_trace_abstraction := + repeat match goal with + | |- mmio_trace_abstraction_relation _ _ => cbv [lightbulb_spec.mmio_trace_abstraction_relation] + | |- Forall2 lightbulb_spec.mmio_event_abstraction_relation _ _ => + eassumption || eapply Forall2_app || eapply Forall2_nil || eapply Forall2_cons + | |- lightbulb_spec.mmio_event_abstraction_relation _ _ => + (left + right); eexists _, _; split; exact eq_refl + end. + + Ltac metrics' := + repeat match goal with | H := _ : MetricLog |- _ => subst H end; + cost_unfold; + repeat match goal with + | H: context [?x] |- _ => is_const x; let t := type of x in constr_eq t constr:(MetricLog); + progress cbv beta delta [x] in * + | |- context [?x] => is_const x; let t := type of x in constr_eq t constr:(MetricLog); + progress cbv beta delta [x] in * + end; + cbn -[Z.add Z.mul Z.of_nat] in *; + rewrite ?List.app_length, ?List.length_cons, ?List.length_nil in *; + flatten_MetricLog; repeat unfold_MetricLog; repeat simpl_MetricLog; try blia. + Ltac metrics := solve [metrics']. + + Local Ltac slv := solve [ trivial | eauto 2 using TracePredicate.any_app_more | assumption | blia | trace_alignment | mmio_trace_abstraction ]. + + Ltac t := + match goal with + | _ => slv + | _ => progress evl + + | H : _ /\ _ \/ ?Y /\ _, G : not ?X |- _ => + constr_eq X Y; let Z := fresh in destruct H as [|[Z ?]]; [|case (G Z)] + | H : not ?Y /\ _ \/ _ /\ _, G : ?X |- _ => + constr_eq X Y; let Z := fresh in destruct H as [[Z ?]|]; [case (Z G)|] + | |- exists x, _ /\ _ => eexists; split; [repeat f_equal; slv|] + | |- ?A /\ _ \/ ?B /\ _ => + match goal with + | H: A |- _ => left | H: not B |- _ => left + | H: B |- _ => right | H: not A |- _ => right + end + + | |- _ /\ _ => split; [repeat t|] + + | _ => straightline + | _ => straightline_call; [ solve[repeat t].. | ] + | _ => split_if; [ solve[repeat t].. | ] + | |- MetricWeakestPrecondition.cmd _ (cmd.interact _ _ _) _ _ _ _ _ => eapply MetricWeakestPreconditionProperties.interact_nomem; [ solve[repeat t].. | ] + end. + + Import Word.Properties. + + Lemma lan9250_init_ok : program_logic_goal_for_function! lan9250_init. + Proof. + repeat t. + split_if; repeat t. + { rewrite ?app_nil_r; intuition idtac. } + straightline_call. + { clear -word_ok; rewrite word.unsigned_of_Z; cbv; split; congruence. } + repeat t. + split_if; repeat t. + { rewrite ?app_nil_r; intuition eauto using TracePredicate.any_app_more. } + straightline_call. + { clear -word_ok; rewrite word.unsigned_of_Z; cbv; split; congruence. } + repeat t. + split_if; repeat t. + { rewrite ?app_nil_r; intuition eauto using TracePredicate.any_app_more. } + straightline_call. + { clear -word_ok; rewrite word.unsigned_of_Z; cbv; split; congruence. } + repeat t. + split_if; repeat t. + { rewrite ?app_nil_r; intuition eauto using TracePredicate.any_app_more. } + straightline_call. + { clear -word_ok; rewrite word.unsigned_of_Z; cbv; split; congruence. } + repeat t. + rewrite ?app_nil_r; intuition eauto using TracePredicate.any_app_more. + + right. + split; trivial. + cbv [lan9250_init_trace]. + eexists. + repeat eapply concat_app; eauto. + Qed. + + Local Hint Mode map.map - - : typeclass_instances. (* COQBUG https://github.com/coq/coq/issues/14707 *) + + Lemma lan9250_readword_ok : program_logic_goal_for_function! lan9250_readword. + Proof. + Time repeat straightline. + + repeat match goal with + | H : _ /\ _ \/ ?Y /\ _, G : not ?X |- _ => + constr_eq X Y; let Z := fresh in destruct H as [|[Z ?]]; [|case (G Z)] + | H : not ?Y /\ _ \/ _ /\ _, G : ?X |- _ => + constr_eq X Y; let Z := fresh in destruct H as [[Z ?]|]; [case (Z G)|] + | _ => progress cbv [MMIOREAD MMIOWRITE] + | _ => progress cbv [SPI_CSMODE_ADDR] + | |- _ /\ _ => split + | |- context G[string_dec ?x ?x] => + let e := eval cbv in (string_dec x x) in + let goal := context G [e] in + change goal + | |- context G[string_dec ?x ?y] => + unshelve erewrite (_ : string_dec x y = right _); [ | exact eq_refl | ] + | _ => straightline_cleanup + | |- MetricWeakestPrecondition.cmd _ (cmd.interact _ _ _) _ _ _ _ _ => eapply MetricWeakestPreconditionProperties.interact_nomem + | |- ext_spec _ _ _ _ _ => + letexists; split; [exact eq_refl|]; split; [split; trivial|] + | |- ext_spec _ _ _ _ _ => + letexists; letexists; split; [exact eq_refl|]; split; [split; trivial|] + + | H: ?x = 0 |- _ => rewrite H + | |- ?F ?a ?b ?c => + match F with MetricWeakestPrecondition.get => idtac end; + let f := (eval cbv beta delta [MetricWeakestPrecondition.get] in F) in + change (f a b c); cbv beta + | _ => straightline + | _ => straightline_call + | _ => split_if + end. + all: try (eexists _, _; split; trivial). + all: try (exact eq_refl). + all: auto. + 1,2,3,4,16,17,18,19: + repeat match goal with x := _ |- _ => subst x end; + cbv [isMMIOAddr SPI_CSMODE_ADDR]; + rewrite !word.unsigned_of_Z; cbv [word.wrap]; + trivial; cbv -[Z.le Z.lt]; blia. + + all : try ( + repeat match goal with x := _ ++ _ |- _ => subst x end; + eexists; split; + [ repeat match goal with + |- context G [cons ?a ?b] => + assert_fails (idtac; match b with nil => idtac end); + let goal := context G [(app (cons a nil) b)] in + change goal + end; + rewrite !app_assoc; + repeat eapply (fun A => f_equal2 (@List.app A)); eauto |]). + + all : try ( + eexists; split; [ + repeat (eassumption || eapply Forall2_app || eapply Forall2_nil || eapply Forall2_cons) |]). + all : try ((left + right); eexists _, _; split; exact eq_refl). + + + all : try (left; split; [eassumption|]). + all : repeat rewrite <-app_assoc. + + all : eauto using TracePredicate.any_app_more. + { rewrite ?word.unsigned_of_Z; exact eq_refl. } + { rewrite Properties.word.unsigned_sru_nowrap; cycle 1. + { rewrite word.unsigned_of_Z; exact eq_refl. } + rewrite word.unsigned_of_Z; cbv [word.wrap]; rewrite Z.mod_small by (cbv; split; congruence). + rewrite Z.shiftr_div_pow2 by blia. + clear -H8. + change 0x400 with (4*256) in *. + Z.div_mod_to_equations. blia. } + { rewrite Properties.word.unsigned_and_nowrap. + rewrite word.unsigned_of_Z; cbv [word.wrap]; rewrite Z.mod_small by (cbv; split; congruence). + change 255 with (Z.ones 8). + rewrite Z.land_ones; + Z.div_mod_to_equations; blia. } + + right. + eexists; eauto. + split. + 2:metrics'. + eexists _, _, _, _, _, _. + + cbv [ + lightbulb_spec.lan9250_fastread4 + lightbulb_spec.spi_begin + lightbulb_spec.spi_xchg_mute + lightbulb_spec.spi_xchg_dummy + lightbulb_spec.spi_xchg_deaf + lightbulb_spec.spi_end + one + existsl + ]. + + cbv [concat]. + repeat match goal with + | |- _ /\ _ => eexists + | |- exists _, _ => eexists + | |- ?e = _ => is_evar e; exact eq_refl + | |- _ = ?e => is_evar e; exact eq_refl + end. + + 1 : rewrite <-app_assoc. + 1 : cbv [SPI_CSMODE_HOLD] ; rewrite word.unsigned_of_Z; exact eq_refl. + all : rewrite word.unsigned_of_Z in H12; try eassumption. + 1,2: + repeat match goal with + | _ => rewrite word.of_Z_unsigned + | _ => rewrite Byte.byte.unsigned_of_Z + | _ => cbv [Byte.byte.wrap]; rewrite Z.mod_small + | _ => solve [trivial] + end. + { rewrite Properties.word.unsigned_sru_nowrap by (rewrite word.unsigned_of_Z; exact eq_refl). + rewrite word.unsigned_of_Z; cbv [word.wrap]; rewrite Z.mod_small by (cbv; split; congruence). + rewrite Z.shiftr_div_pow2 by blia. + generalize dependent a; clear; intros. + change 0x400 with (4*256) in *. + Z.div_mod_to_equations. blia. } + { rewrite Properties.word.unsigned_and_nowrap. + rewrite word.unsigned_of_Z; cbv [word.wrap]; rewrite Z.mod_small by (cbv; split; congruence). + change 255 with (Z.ones 8); rewrite Z.land_ones by blia. + Z.div_mod_to_equations. blia. } + repeat match goal with x := _ |- _ => subst x end. + cbv [LittleEndianList.le_combine]. + + repeat rewrite ?Properties.word.unsigned_or_nowrap, <-?Z.lor_assoc by (rewrite ?word.unsigned_of_Z; exact eq_refl). + change (Z.shiftl 0 8) with 0 in *; rewrite Z.lor_0_r. + rewrite !Z.shiftl_lor, !Z.shiftl_shiftl in * by blia. + repeat f_equal. + + (* little-endian word conversion, automatable (bitwise Z and word) *) + all : try rewrite word.unsigned_slu by (rewrite ?word.unsigned_of_Z; exact eq_refl). + all : rewrite ?word.unsigned_of_Z. + all : cbv [word.wrap]. + all : repeat match goal with |- context G [?a mod ?b] => let goal := context G [a] in change goal end. + all : repeat match goal with |- context[Byte.byte.unsigned ?x] => is_var x; replace (Byte.byte.unsigned x) with (Byte.byte.wrap (Byte.byte.unsigned x)) by eapply Byte.byte.wrap_unsigned; set (Byte.byte.unsigned x) as X; clearbody X end. + all : change (8+8) with 16. + all : change (8+16) with 24. + all : cbv [Byte.byte.wrap]. + all : clear. + all : rewrite ?Z.shiftl_mul_pow2 by blia. + all : try (Z.div_mod_to_equations; blia). + Qed. + + Lemma lan9250_writeword_ok : program_logic_goal_for_function! lan9250_writeword. + Proof. + repeat t. + letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr. cbv [isMMIOAddr SPI_CSMODE_ADDR]. + rewrite !word.unsigned_of_Z; cbv [word.wrap]. + split; [|exact eq_refl]; clear. + cbv -[Z.le Z.lt]. blia. } + repeat straightline. + eapply MetricWeakestPreconditionProperties.interact_nomem; repeat straightline. + letexists; letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr. cbv [isMMIOAddr SPI_CSMODE_ADDR]. + rewrite !word.unsigned_of_Z; cbv [word.wrap]. + split; [|exact eq_refl]; clear. + cbv -[Z.le Z.lt]. blia. } + repeat straightline. + + straightline_call. + 1: { + match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end. + revert H7. + evl. + intros. + Z.div_mod_to_equations. blia. + } + repeat t. + straightline_call. + 1: { + match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end. + revert H7. + evl. + intros. + Z.div_mod_to_equations. blia. + } + repeat t. + straightline_call. + 1: { + match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end. + Z.div_mod_to_equations. blia. + } + repeat t. + straightline_call. + 1: { + match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end. + Z.div_mod_to_equations. blia. + } + repeat t. + straightline_call. + 1: { + match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end. + Z.div_mod_to_equations. blia. + } + repeat t. + + straightline_call. + 1: { + match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end. + Z.div_mod_to_equations. blia. + } + repeat t. + + straightline_call. + 1: { + match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end. + pose proof word.unsigned_range v. + repeat match goal with x := _ |- _ => subst x end. + Z.div_mod_to_equations. blia. + } + + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + t. + letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr. cbv [isMMIOAddr SPI_CSMODE_ADDR]. + rewrite !word.unsigned_of_Z; cbv [word.wrap]. + split; [|exact eq_refl]; clear. + cbv -[Z.le Z.lt]. blia. } + t. + t. + t. + t. + t. + t. + t. + t. + t. + letexists; letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr addr0. cbv [isMMIOAddr SPI_CSMODE_ADDR]. + rewrite !word.unsigned_of_Z; cbv [word.wrap]. + split; [|exact eq_refl]; clear. + cbv -[Z.le Z.lt]. blia. } + repeat t. + + 2: metrics. + + do 6 letexists. + cbv [spi_begin spi_xchg_deaf spi_end one]. + Local Arguments spi_xchg {_ _}. + + (* aligning regex and mmiotrace, not sure how to do it in a principled way *) + + cbv [concat existsl]. + + all : repeat match goal with + | |- _ /\ _ => split + | |- exists _, _ => eexists + | |- ?e = _ => (let e := rdelta e in is_evar e); try subst e; reflexivity + | |- _ = ?e => (let e := rdelta e in is_evar e); try subst e; reflexivity + end. + + all : repeat match goal with + |- context[?e] => is_evar e; set e + end. + + all: + repeat match goal with |- context[@cons ?T ?x ?y] => + match y with + | [] => fail 1 + | _=> change (@cons T x y) with (@app T (@cons T x nil) y) end end. + + 1: rewrite !app_assoc. + 1: repeat f_equal. + + all : repeat match goal with + |- context[?e] => (let v := rdelta e in is_evar v); subst e + end. + all : trivial. + all : eauto. + + all : try (rewrite Byte.byte.unsigned_of_Z; eapply Z.mod_small). + + all : pose proof word.unsigned_range a. + all : rewrite ?word.unsigned_and_nowrap, ?word.unsigned_sru_nowrap, ?word.unsigned_of_Z; rewrite ?word.unsigned_of_Z. + all : repeat match goal with |- context G[word.wrap ?x] => let g := context G [x] in change g end. + all : change 255 with (Z.ones 8). + all : rewrite ?Z.shiftr_div_pow2, ?Z.land_ones by blia. + all: try (Z.div_mod_to_equations; blia). + { subst addr. + cbv [SPI_CSMODE_HOLD]. + erewrite word.unsigned_of_Z. + change (word.wrap 2) with 2. + erewrite (word.of_Z_inj_mod _ (Z.lnot 2)); trivial. } + { instantiate (1:=x1); move H11 at bottom. + (* Local Arguments spi_xchg {_} _ _ _. *) + erewrite word.unsigned_of_Z in H11. + exact H11. } + + cbv [List.app]. + repeat match goal with x := _ |- _ => subst x end. + cbv [LittleEndianList.le_combine]. + repeat rewrite ?word.unsigned_of_Z, word.unsigned_sru_nowrap by (rewrite word.unsigned_of_Z; exact eq_refl). + + try erewrite ?word.unsigned_of_Z. + cbv [word.wrap]. + repeat match goal with |- context G [?a mod ?b] => let goal := context G [a] in change goal end. + rewrite ?Z.shiftl_mul_pow2 by (clear; blia). + + change 255 with (Z.ones 8). + rewrite <-!Z.shiftl_mul_pow2 by blia. + pose proof (@word.unsigned_range _ _ word_ok v). + set (@word.unsigned _ _ v) as X in *. + rewrite ?Byte.byte.unsigned_of_Z. + unfold Byte.byte.wrap. + rewrite <- ?Z.land_ones by blia. + prove_Zeq_bitwise. + Qed. + + Lemma lan9250_mac_write_ok : program_logic_goal_for_function! lan9250_mac_write. + Proof. + repeat match goal with + | _ => straightline + | _ => straightline_call + | _ => split_if + | _ => rewrite word.unsigned_of_Z + | |- context G [word.wrap ?a] => + requireZcst a; + let t := eval cbv in (word.wrap a) in + let g := context G [t] in + change g + | |- _ <= _ < _ => blia + | |- _ /\ _ => split + end. + + all : repeat t. + + intuition idtac; repeat t. + 2: metrics. + + eexists. + rewrite app_nil_r. + eauto using concat_app. + Qed. + + Lemma lan9250_wait_for_boot_ok : program_logic_goal_for_function! lan9250_wait_for_boot. + Proof. + repeat straightline. + refine ((atleastonce ["err"; "i"; "byteorder"] (fun v T M MC ERR I BUSY => + v = word.unsigned I /\ word.unsigned I <> 0 /\ M = m /\ + exists tl, T = tl++t /\ + exists th, mmio_trace_abstraction_relation th tl /\ + exists n, (multiple (lan9250_boot_attempt _) n) th /\ + Z.of_nat n + word.unsigned I = patience + )) + _ _ _ _ _); + cbn [reconstruct map.putmany_of_list HList.tuple.to_list + 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. + { exact (Z.lt_wf 0). } + { subst i; repeat t. + exists O; cbn; split; trivial. + rewrite word.unsigned_of_Z. exact eq_refl. } + { exfalso. subst i. ZnWords. } + { straightline_call. + { rewrite word.unsigned_of_Z. + repeat match goal with + | |- context G [word.wrap ?a] => + requireZcst a; + let t := eval cbv in (word.wrap a) in + let g := context G [t] in + change g + end. + clear; blia. } + repeat straightline. + split_if. + { + repeat (t; []); split. + { intro X. exfalso. eapply X. subst i. rewrite word.unsigned_xor. + rewrite Z.lxor_nilpotent. exact eq_refl. } + repeat t; eauto using TracePredicate.any_app_more. + } + repeat straightline. + split_if; repeat t. + { exfalso. subst i. rewrite word.unsigned_xor, Z.lxor_nilpotent in *. ZnWords. } + { right. + split; trivial. + cbv [lan9250_wait_for_boot_trace]. + rewrite app_nil_r. + eapply concat_app; eauto using kleene_multiple. + destruct (word.eqb_spec x5 (word.of_Z 2271560481)); subst. + 2: exfalso; ZnWords. + eassumption. } + { eexists. split. + 1: split; [exact eq_refl|]. + 2: { + pose proof word.unsigned_range i. + pose proof word.unsigned_range x0. + subst v. subst i. + rewrite word.unsigned_sub, word.unsigned_of_Z. + change (word.wrap 1) with 1. + cbv [word.wrap]; rewrite Z.mod_small; blia. } + repeat t. + rewrite app_nil_r. + eexists (S _). + split. + { eapply multiple_expand_right, concat_app; eauto. + destruct (word.eqb_spec x5 (word.of_Z 2271560481)); subst. + { exfalso; ZnWords. } + eexists. split; eauto. + ZnWords. } + ZnWords. } + { left. right. + split. { intro X. subst err. rewrite word.unsigned_of_Z in X. inversion X. } + rewrite app_nil_r. + cbv [lan9250_boot_timeout]. + rewrite <-H6. + replace (word.unsigned x0) with 1; cycle 1. + { subst i. ZnWords. } + rewrite Z.add_1_r. + rewrite Znat.Z2Nat.inj_succ by (clear; blia). + rewrite Znat.Nat2Z.id. + + eapply multiple_expand_right, concat_app; eauto. + eexists; split; eauto. + destruct (word.eqb_spec x5 (word.of_Z 2271560481)); ZnWords. } } + Qed. + + Import MetricWeakestPrecondition SeparationLogic Array Scalars MetricProgramLogic.Coercions. + Local Notation spi_timeout := (lightbulb_spec.spi_timeout word). + Local Notation lan9250_send := (lightbulb_spec.lan9250_send word). + Global Instance spec_of_lan9250_tx : MetricProgramLogic.spec_of "lan9250_tx" := + fnspec! "lan9250_tx" p l / bs R ~> err, + { requires t m mc := 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 MC := M = m /\ + exists iol, T = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned err <> 0 /\ (any +++ spi_timeout) ioh) + (word.unsigned err = 0 /\ lan9250_send bs ioh /\ + (MC - mc <= (50+6*l)* mc_spi_xchg_const + Z.of_nat (length ioh) * mc_spi_mul))%metricsH + }. + + Import symmetry autoforward. + + Local Ltac no_call := + lazymatch goal with + | |- Semantics.call _ _ _ _ _ _ => fail + | |- _ => idtac + end. + + Local Ltac original_esplit := esplit. + Local Ltac esplit := no_call; original_esplit. + + Lemma lan9250_tx_ok : program_logic_goal_for_function! lan9250_tx. + Proof. + + (* TODO clean this up *) + repeat (subst || straightline || straightline_call || ZnWords || intuition eauto). + { repeat (straightline || intuition eauto || esplit). } + esplit; esplit. + esplit. + { repeat straightline. } + unfold dlet.dlet. + intuition (esplit; esplit). + + esplit; repeat straightline. + + straightline_call; [ZnWords|]; repeat (intuition idtac; repeat straightline). + { eexists; eexists; split; repeat (straightline; intuition idtac; eauto). + subst a. rewrite app_assoc. + eexists; Tactics.ssplit; eauto. + eexists; Tactics.ssplit; try mmio_trace_abstraction; eauto using any_app_more. } + eexists; eexists; split; repeat (straightline; intuition eauto). + + refine (MetricLoops.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 mc => 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 /\ + err = 0 :> Z + ) + (fun T M P L ERR MC => + M = m /\ exists iol, T = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned ERR <> 0 /\ (any +++ spi_timeout) ioh) + (word.unsigned ERR = 0 /\ lightbulb_spec.lan9250_writepacket _ bs ioh /\ + (MC - mc <= (1+6*l) * mc_spi_xchg_const + Z.of_nat (length ioh) * mc_spi_mul)%metricsH) + ) + ) _ (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. + 2: { + eapply word.if_zero in H18. + rewrite word.unsigned_ltu in H18. + autoforward with typeclass_instances in H18. + destruct x5; cbn [List.length] in *; [|exfalso; ZnWords]. + Tactics.ssplit; trivial. repeat t; metrics. } + subst br. + rename l into l0. + rename x8 into l. + rewrite word.unsigned_ltu in H18. + destr.destr Z.ltb. + 2: { contradiction H18. rewrite word.unsigned_of_Z_0; trivial. } + pose proof word.unsigned_range l as Hl. rewrite H15 in Hl. + eapply (f_equal word.of_Z) in H15. rewrite word.of_Z_unsigned in H15. + 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 H17. + seprewrite_in @array_append H17. + seprewrite_in @scalar32_of_bytes H17. + { autoforward with typeclass_instances in E. + rewrite firstn_length. ZnWords. } + + eexists; eexists; split; repeat straightline. + straightline_call; repeat straightline. + { ZnWords. } + + seprewrite_in (symmetry! @scalar32_of_bytes) H17. + { autoforward with typeclass_instances in E. + rewrite firstn_length. ZnWords. } + + rename x5 into err. + eexists; eexists; split; repeat straightline; intuition idtac. + { seprewrite_in (symmetry! @array_append) H17. + rewrite (firstn_skipn 4 bs) in H17. + repeat straightline. + left; repeat t. + 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 H17 by ZnWords. + progress change (Z.of_nat 4) with 4%Z in H17. + eexists _, _, _; split; intuition eauto. + 3: ecancel_assumption. + 1: rewrite skipn_length; ZnWords. + 1 : ZnWords. + split; repeat t; [ ZnWords .. |]. + intuition idtac; repeat t. + 2: solve [metrics'; try ZnWords]. + do 4 (destruct bs as [|?b bs]; cbn [List.length] in *; try (exfalso; ZnWords)); + cbn [List.skipn lan9250_writepacket] in *; rewrite app_nil_r. + eauto using concat_app. } + + repeat t; intuition eauto; repeat t. + 2: metrics'. + rewrite app_nil_r. eapply concat_app; eauto. eapply concat_app; eauto. + Import Tactics.eplace. + all : match goal with |- ?f ?x _ => eplace x with _ ; try eassumption end. + all : f_equal; ZnWords. + Qed. + + Require Import Utf8. + Import Map.Separation. + Local Notation bytes := (array ptsto (word.of_Z 1)). + Implicit Type l : word. + Instance spec_of_lan9250_tx' : spec_of "lan9250_tx" := + fnspec! "lan9250_tx" p l / bs ~> err, + { requires t m mc := m =*> bytes p bs ∧ l = length bs :> Z ∧ l mod 4 = 0 :> Z; + ensures T M MC := M = m ∧ ∃ t', T = t' ++ t ∧ only_mmio_satisfying (fun h => + ((0 <> err ∧ (any+++spi_timeout) h) ∨ (0 = err ∧ lan9250_send bs h ∧ + MC - mc <= (50+6*l)*mc_spi_xchg_const + (length h)*mc_spi_mul))%metricsH) t' + }. + + Lemma lan9250_tx_ok' : program_logic_goal_for_function! lan9250_tx. + Proof. + epose proof lan9250_tx_ok. + cbv [program_logic_goal_for] in *; intros; eauto. + cbv [spec_of_lan9250_tx' spec_of_lan9250_tx] in *. + intros; eauto. + case H3 as ([]&?&?). + eapply MetricWeakestPreconditionProperties.Proper_call; [|eapply H]; intuition idtac; Tactics.ssplit; eauto. + repeat intro. + repeat match goal with + | H : exists _, _ |- _ => case H as [] + | H : _ /\ _ |- _ => case H as [] + end; subst. + repeat ((eexists; eauto; []) || (split; eauto; [])). + intuition congruence. + Qed. +End WithParameters. diff --git a/bedrock2/src/bedrock2Examples/metric_SPI.v b/bedrock2/src/bedrock2Examples/metric_SPI.v new file mode 100644 index 000000000..8fbaa9cf1 --- /dev/null +++ b/bedrock2/src/bedrock2Examples/metric_SPI.v @@ -0,0 +1,486 @@ +Require Import bedrock2.Syntax bedrock2.NotationsCustomEntry Coq.Strings.String. +Require Import coqutil.Z.div_mod_to_equations. +Require Import coqutil.Z.Lia. +Require Import coqutil.Word.Interface. +Require Import coqutil.Byte. + +Import BinInt String List.ListNotations ZArith. +Local Open Scope Z_scope. Local Open Scope string_scope. Local Open Scope list_scope. + +Require bedrock2Examples.lightbulb_spec. +Local Notation patience := lightbulb_spec.patience. + +Definition spi_write := func! (b) ~> busy { + busy = $-1; + i = $patience; while i { i = i - $1; + io! busy = MMIOREAD($0x10024048); + if !(busy >> $31) { i = i^i } + }; + if !(busy >> $31) { + output! MMIOWRITE($0x10024048, b); + busy = (busy ^ busy) + } + }. + +Definition spi_read := func! () ~> (b, busy) { + busy = $-1; + b = $0x5a; + i = $patience; while i { i = i - $1; + io! busy = MMIOREAD($0x1002404c); + if !(busy >> $31) { + b = busy & $0xff; + i = i^i; + busy = i + } + } + }. + +Definition spi_xchg := func! (b) ~> (b, busy) { + unpack! busy = spi_write(b); + require !busy; + unpack! b, busy = spi_read() + }. + +Require Import bedrock2.MetricLogging bedrock2.MetricCosts. +Require Import bedrock2.MetricProgramLogic. +Require Import bedrock2.MetricWeakestPreconditionProperties. +Require Import bedrock2.FE310CSemantics bedrock2.MetricSemantics. +Require Import Coq.Lists.List. Import ListNotations. +Require Import bedrock2.TracePredicate. Import TracePredicateNotations. +Require Import bedrock2.ZnWords. + +Import coqutil.Map.Interface. +Import ReversedListNotations. + +Section WithParameters. + Context {word: word.word 32} {mem: map.map word Byte.byte}. + Context {word_ok: word.ok word} {mem_ok: map.ok mem}. + + Definition mmio_event_abstraction_relation + (h : lightbulb_spec.OP word) + (l : mem * string * list word * (mem * list word)) := + Logic.or + (exists a v, h = ("st", a, v) /\ l = (map.empty, "MMIOWRITE", [a; v], (map.empty, []))) + (exists a v, h = ("ld", a, v) /\ l = (map.empty, "MMIOREAD", [a], (map.empty, [v]))). + Definition mmio_trace_abstraction_relation := + List.Forall2 mmio_event_abstraction_relation. + Definition only_mmio_satisfying P t := + exists mmios, mmio_trace_abstraction_relation mmios t /\ P mmios. + + Definition mc_spi_write_const := mkMetricLog 348 227 381 204. + Definition mc_spi_read_const := mkMetricLog 199 116 217 103. + Definition mc_spi_xchg_const := (mc_spi_write_const + mc_spi_read_const + mkMetricLog 410 402 414 401)%metricsH. + Definition mc_spi_mul := mkMetricLog 157 109 169 102. + Ltac mc_spi_write_unf := unfold mc_spi_write_const, mc_spi_mul in *. + Ltac mc_spi_read_unf := unfold mc_spi_read_const, mc_spi_mul in *. + Ltac mc_spi_xchg_unf := unfold mc_spi_xchg_const in *. + + Global Instance spec_of_spi_write : spec_of "spi_write" := fun functions => forall t m b mc, + word.unsigned b < 2 ^ 8 -> + MetricWeakestPrecondition.call functions "spi_write" t m [b] mc (fun T M RETS MC => + M = m /\ exists iol, T = t ;++ iol /\ exists ioh, mmio_trace_abstraction_relation ioh iol /\ exists err, RETS = [err] /\ Logic.or + (((word.unsigned err <> 0) /\ lightbulb_spec.spi_write_full _ ^* ioh /\ Z.of_nat (length ioh) = patience)) + (word.unsigned err = 0 /\ lightbulb_spec.spi_write word (byte.of_Z (word.unsigned b)) ioh) /\ + (MC - mc <= mc_spi_write_const + Z.of_nat (length ioh) * mc_spi_mul)%metricsH). + + Global Instance spec_of_spi_read : spec_of "spi_read" := fun functions => forall t m mc, + MetricWeakestPrecondition.call functions "spi_read" t m [] mc (fun T M RETS MC => + M = m /\ exists iol, T = t ;++ iol /\ exists ioh, mmio_trace_abstraction_relation ioh iol /\ exists (b: byte) (err : word), RETS = [word.of_Z (byte.unsigned b); err] /\ Logic.or + (word.unsigned err <> 0 /\ lightbulb_spec.spi_read_empty _ ^* ioh /\ Z.of_nat (length ioh) = patience) + (word.unsigned err = 0 /\ lightbulb_spec.spi_read word b ioh) /\ + (MC - mc <= mc_spi_read_const + Z.of_nat (length ioh) * mc_spi_mul)%metricsH). + + Lemma nonzero_because_high_bit_set (x : word) (H : word.unsigned (word.sru x (word.of_Z 31)) <> 0) + : word.unsigned x <> 0. + Proof. ZnWords. Qed. + + Add Ring wring : (Properties.word.ring_theory (word := word)) + (preprocess [autorewrite with rew_word_morphism], + morphism (Properties.word.ring_morph (word := word)), + constants [Properties.word_cst]). + + Ltac metrics := + repeat match goal with | H := _ : MetricLog |- _ => subst H end; + cost_unfold; + cbn in *; + solve_MetricLog. + + Ltac viewmetric := + repeat match goal with | H := _ : MetricLog |- _ => subst H end; + cost_unfold; + cbn in *; + repeat rewrite metriclit in *; + cbn in *. + + Import coqutil.Tactics.letexists. + Import MetricLoops. + Lemma spi_write_ok : program_logic_goal_for_function! spi_write. + Proof. + repeat straightline. + rename H into Hb. + + (* WHY do theese parentheses matter? *) + refine ((atleastonce ["b"; "busy"; "i"] (fun v T M MC B BUSY I => + b = B /\ v = word.unsigned I /\ word.unsigned I <> 0 /\ M = m /\ + exists tl, T = tl++t /\ + exists th, mmio_trace_abstraction_relation th tl /\ + lightbulb_spec.spi_write_full _ ^* th /\ + Z.of_nat (length th) + word.unsigned I = patience /\ + (MC - mc <= Z.of_nat (length th) * mc_spi_mul + mkMetricLog 27 5 30 0)%metricsH + )) _ _ _ _ _); + cbn [reconstruct map.putmany_of_list HList.tuple.to_list + 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. } + { eapply (Z.lt_wf 0). } + { eexists; eexists; split; repeat straightline. + { split; trivial; split; trivial. + eexists; split. + { rewrite app_nil_l; trivial. } + eexists; split. + { constructor. } + split. + { constructor. } + split; [|metrics]. + subst i. rewrite word.unsigned_of_Z. exact eq_refl. } + exfalso. ZnWords. } + repeat straightline. + eapply MetricWeakestPreconditionProperties.interact_nomem; repeat straightline. + letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { + cbv [isMMIOAddr addr]. + ZnWords. } + repeat straightline. + (* The hnf inside this letexists used to substitute + + c := cmd.cond (expr.op bopname.sru "busy" 31) cmd.skip + (cmd.set "i" (expr.op bopname.xor "i" "i")) : cmd.cmd + + and also unfolded WeakestPrecondition.cmd of c into + + WeakestPrecondition.dexpr m l0 cond letboundEvar /\ + ThenCorrectness /\ + ElseCorrectness + *) + letexists. letexists. split. + { repeat straightline. } + split; intros. + { (* CASE if-condition was true (word.unsigned v0 <> 0), i.e. NOP, loop exit depends on whether timeout *) + repeat straightline. (* <-- does split on a postcondition of the form + (word.unsigned br <> 0 -> loop invariant still holds) /\ + (word.unsigned br = 0 -> code after loop is fine) + which corresponds to case distinction over whether loop was exited *) + { (* SUBCASE loop condition was true (do loop again) *) + eexists; split. + { repeat (split; trivial; []). subst t0. + eexists (_ ;++ cons _ nil); split; [exact eq_refl|]. + eexists; split. + { refine (List.Forall2_app _ _); try eassumption. + econstructor; [|constructor]. + right; eexists _, _; repeat split. } + split. + { eapply kleene_app; eauto. + refine (kleene_step _ _ nil _ (kleene_empty _)). + repeat econstructor. + ZnWords. } + split; [|mc_spi_write_unf; metrics]. + { ZnWordsL. } } + { ZnWords. } } + { (* SUBCASE loop condition was false (exit loop because of timeout *) + letexists; letexists; split; [solve[repeat straightline]|split]; repeat straightline; try contradiction. + subst t0. + eexists (_ ;++ cons _ nil); split. + { rewrite <-app_assoc; cbn [app]; f_equal. } + eexists. split. + { eapply Forall2_app; eauto. + constructor; [|constructor]. + right; eauto. } + eexists. split; trivial. + split; [|mc_spi_write_unf; metrics]. + { left; repeat split; eauto using nonzero_because_high_bit_set. + { (* copied from above -- trace element for "fifo full" *) + eapply kleene_app; eauto. + refine (kleene_step _ _ nil _ (kleene_empty _)). + repeat econstructor. + ZnWords. } + { ZnWordsL. } } } + } + (* CASE if-condition was false (word.unsigned v0 = 0), i.e. we'll set i=i^i and exit loop *) + repeat straightline. + { subst i. + rewrite Properties.word.unsigned_xor_nowrap in *; rewrite Z.lxor_nilpotent in *; contradiction. } + (* evaluate condition then split if *) letexists; letexists; split; [solve[repeat straightline]|split]. + 1:contradiction. + repeat straightline. + eapply MetricWeakestPreconditionProperties.interact_nomem; repeat straightline. + letexists; letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { cbv [isMMIOAddr]. ZnWords. } + repeat straightline. + subst t0. + eexists (_ ;++ cons _ (cons _ nil)). split. + { rewrite <-app_assoc. cbn [app]. f_equal. } + eexists. split. + { eapply List.Forall2_app; eauto. + { constructor. + { left. eexists _, _; repeat split. } + { right; [|constructor]. + right; eexists _, _; repeat split. } } } + eexists; split; trivial. + split; [|mc_spi_write_unf; metrics]. + right. + subst busy. + split. + { f_equal. rewrite Properties.word.unsigned_xor_nowrap; rewrite Z.lxor_nilpotent; reflexivity. } + cbv [lightbulb_spec.spi_write]. + eexists _, _; split; eauto; []; split; eauto. + eexists (cons _ nil), (cons _ nil); split; cbn [app]; eauto. + split; repeat econstructor. + { ZnWords. } + { cbv [lightbulb_spec.spi_write_enqueue one]. + repeat f_equal. + eapply Properties.word.unsigned_inj. + rewrite byte.unsigned_of_Z; cbv [byte.wrap]; rewrite Z.mod_small; ZnWords. } + Qed. + + Local Ltac split_if := + lazymatch goal with + |- MetricWeakestPrecondition.cmd _ ?c _ _ _ _ ?post => + let c := eval hnf in c in + lazymatch c with + | cmd.cond _ _ _ => letexists; letexists; split; [solve[repeat straightline]|split] + end + end. + + Lemma spi_read_ok : program_logic_goal_for_function! spi_read. + Proof. + repeat straightline. + refine ((atleastonce ["b"; "busy"; "i"] (fun v T M MC B BUSY I => + v = word.unsigned I /\ word.unsigned I <> 0 /\ M = m /\ + B = word.of_Z (byte.unsigned (byte.of_Z (word.unsigned B))) /\ + exists tl, T = tl++t /\ + exists th, mmio_trace_abstraction_relation th tl /\ + lightbulb_spec.spi_read_empty _ ^* th /\ + Z.of_nat (length th) + word.unsigned I = patience /\ + (MC - mc <= Z.of_nat (length th) * mkMetricLog 157 109 169 102 + mkMetricLog 39 7 43 0)%metricsH + )) + _ _ _ _ _); + cbn [reconstruct map.putmany_of_list HList.tuple.to_list + 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. + { exact (Z.lt_wf 0). } + { split; trivial; split; trivial. + subst b; rewrite byte.unsigned_of_Z; cbv [byte.wrap]; + rewrite Z.mod_small; rewrite word.unsigned_of_Z. + 2: { cbv. split; congruence. } + split; trivial. + eexists nil; split; trivial. + subst i; rewrite word.unsigned_of_Z. + eexists nil; split; try split; try solve [constructor]. + split; [|metrics]. + constructor. + } + { exfalso. ZnWords. } + { eapply MetricWeakestPreconditionProperties.interact_nomem; repeat straightline. + letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { cbv [isMMIOAddr]. ZnWords. } + repeat ((split; trivial; []) || straightline || split_if). + { + letexists. split. + { subst v'. + split; trivial. + split; trivial. + split; trivial. + split; trivial. + eexists (x2 ;++ cons _ nil); split; cbn [app]; eauto. + eexists. split. + { econstructor; try eassumption; right; eauto. } + split. + { + refine (kleene_app _ (cons _ nil) _ x3 _); eauto. + refine (kleene_step _ (cons _ nil) nil _ (kleene_empty _)). + eexists; split. + { exact eq_refl. } + { ZnWords. } } + split; [|metrics]. + { ZnWordsL. } } + { ZnWords. } } + { eexists (x2 ;++ cons _ nil); split; cbn [app]; eauto. + eexists. split. + { econstructor; try eassumption; right; eauto. } + eexists (byte.of_Z (word.unsigned x)), _; split. + { f_equal. eassumption. } + split; [|mc_spi_read_unf; metrics]. + left; repeat split; eauto using nonzero_because_high_bit_set. + { refine (kleene_app _ (cons _ nil) _ x3 _); eauto. + refine (kleene_step _ (cons _ nil) nil _ (kleene_empty _)). + eexists; split. + { exact eq_refl. } + { ZnWords. } } + { ZnWordsL. } } + { repeat straightline. + repeat letexists; split. + 1: split. + { repeat straightline. } + 2: { + subst v'. + subst v. + subst i. + rewrite Properties.word.unsigned_xor_nowrap, Z.lxor_nilpotent. + ZnWords. } + repeat straightline. + repeat (split; trivial; []). + split. + { subst b. + (* automatable: multi-word bitwise *) + change (255) with (Z.ones 8). + pose proof Properties.word.unsigned_range v0. + eapply Properties.word.unsigned_inj. + repeat ( + cbv [byte.wrap word.wrap]; + rewrite ?byte.unsigned_of_Z, ?word.unsigned_of_Z, ?Properties.word.unsigned_and_nowrap, + ?Z.land_ones, ?Z.mod_mod, ?Z.mod_small + by blia; + change (Z.ones 8 mod 2 ^ 32) with (Z.ones 8)). + symmetry; eapply Z.mod_small. + pose proof Z.mod_pos_bound (word.unsigned v0) (2^8) eq_refl. + clear. Z.div_mod_to_equations. blia. } + { (* copy-paste from above, trace manipulation *) + eexists (x2 ;++ cons _ nil); split; cbn [app]; eauto. + eexists. split. + { econstructor; try eassumption; right; eauto. } + subst i. + rewrite Properties.word.unsigned_xor_nowrap, Z.lxor_nilpotent in H1; contradiction. } } + { (* copy-paste from above, trace manipulation *) + eexists (x2 ;++ cons _ nil); split; cbn [app]; eauto. + eexists. split. + { econstructor; try eassumption; right; eauto. } + eexists (byte.of_Z (word.unsigned b)), _; split. + { subst b; f_equal. + (* tag:bitwise *) + (* automatable: multi-word bitwise *) + change (255) with (Z.ones 8). + pose proof Properties.word.unsigned_range v0. + eapply Properties.word.unsigned_inj. + repeat ( + cbv [byte.wrap word.wrap]; + rewrite ?byte.unsigned_of_Z, ?word.unsigned_of_Z, ?Properties.word.unsigned_and_nowrap, + ?Z.land_ones, ?Z.mod_mod, ?Z.mod_small + by blia; + change (Z.ones 8 mod 2 ^ 32) with (Z.ones 8)). + symmetry; eapply Z.mod_small. + pose proof Z.mod_pos_bound (word.unsigned v0) (2^8) eq_refl. + clear. Z.div_mod_to_equations. blia. } + (* tag:symex *) + { split; [|mc_spi_read_unf; metrics]. + right; split. + { subst_words. rewrite Properties.word.unsigned_xor_nowrap, Z.lxor_nilpotent; exact eq_refl. } + eexists x3, (cons _ nil); split; cbn [app]; eauto. + split; eauto. + eexists; split; cbv [one]; trivial. + split. + (* tag:bitwise *) + { ZnWords. } + subst b. + (* automatable: multi-word bitwise *) + change (255) with (Z.ones 8). + pose proof Properties.word.unsigned_range v0. + eapply byte.unsigned_inj. + repeat ( + cbv [byte.wrap word.wrap]; + rewrite ?byte.unsigned_of_Z, ?word.unsigned_of_Z, ?Properties.word.unsigned_and_nowrap, + ?Z.land_ones, ?Z.mod_mod, ?Z.mod_small + by blia; + change (Z.ones 8 mod 2 ^ 32) with (Z.ones 8)). + trivial. } } } + Qed. + + Global Instance spec_of_spi_xchg : spec_of "spi_xchg" := fun functions => forall t m b_out mc, + word.unsigned b_out < 2 ^ 8 -> + MetricWeakestPrecondition.call functions "spi_xchg" t m [b_out] mc (fun T M RETS MC => + M = m /\ exists iol, T = t ;++ iol /\ exists ioh, mmio_trace_abstraction_relation ioh iol /\ exists (b_in:byte) (err : word), RETS = [word.of_Z (byte.unsigned b_in); err] /\ Logic.or + (word.unsigned err <> 0 /\ (any +++ lightbulb_spec.spi_timeout _) ioh) + (word.unsigned err = 0 /\ lightbulb_spec.spi_xchg word (byte.of_Z (word.unsigned b_out)) b_in ioh) /\ + (MC - mc <= mc_spi_xchg_const + Z.of_nat (length ioh) * mc_spi_mul)%metricsH). + + Lemma spi_xchg_ok : program_logic_goal_for_function! spi_xchg. + Proof. + (* avoid using information about read/write consts anywhere to ensure correct dependencies *) + assert (EmptyMetricLog <= mc_spi_read_const)%metricsH by (unfold EmptyMetricLog, mc_spi_read_const; solve_MetricLog). + assert (EmptyMetricLog <= mc_spi_write_const)%metricsH by (unfold EmptyMetricLog, mc_spi_write_const; solve_MetricLog). + + repeat ( + match goal with + | |- ?F ?a ?b ?c => + match F with MetricWeakestPrecondition.get => idtac end; + let f := (eval cbv beta delta [MetricWeakestPrecondition.get] in F) in + change (f a b c); cbv beta + | H : _ /\ _ \/ ?Y /\ _, G : not ?X |- _ => + constr_eq X Y; let Z := fresh in destruct H as [|[Z ?]]; [|case (G Z)] + | H : not ?Y /\ _ \/ _ /\ _, G : ?X |- _ => + constr_eq X Y; let Z := fresh in destruct H as [[Z ?]|]; [case (Z G)|] + end || + + straightline || straightline_call || split_if || refine (conj _ _) || eauto). + + { eexists. split. + { exact eq_refl. } + eexists. split. + { eauto. } + eexists. eexists. split. + { repeat f_equal. + instantiate (1 := byte.of_Z (word.unsigned b_out)). + (* automatable: multi-word bitwise *) + change (255) with (Z.ones 8). + pose proof Properties.word.unsigned_range b_out. + eapply Properties.word.unsigned_inj; + repeat ( + cbv [word.wrap byte.wrap]; + rewrite ?byte.unsigned_of_Z, ?word.unsigned_of_Z, ?Properties.word.unsigned_and_nowrap, ?Z.land_ones, ?Z.mod_mod, ?Z.mod_small by blia; + change (Z.ones 8 mod 2 ^ 32) with (Z.ones 8)); + rewrite ?Z.mod_small; rewrite ?Z.mod_small; trivial; blia. } + split; [|mc_spi_xchg_unf; metrics]. + left; split; eauto. + eexists nil, x0; repeat split; cbv [any choice lightbulb_spec.spi_timeout]; eauto. + rewrite app_nil_r; trivial. } + + { destruct H13; intuition eauto. + { eexists. split. + { subst a0. subst a. + rewrite List.app_assoc; trivial. } + eexists. split. + { eapply Forall2_app; eauto. } + eexists _, _; split. + { subst v; trivial. } + split; [|rewrite app_length; mc_spi_xchg_unf; metrics]. + left; split; eauto. + eapply concat_app; cbv [any choice lightbulb_spec.spi_timeout]; eauto. } + eexists. + subst a0. + subst a. + split. + { rewrite List.app_assoc; trivial. } + eexists. + split. + { eapply Forall2_app; eauto. } + eexists _, _; split. + { subst v. eauto. } + split; [|rewrite app_length; mc_spi_xchg_unf; metrics]. + right. split; eauto. + cbv [lightbulb_spec.spi_xchg]. + + assert (Trace__concat_app : forall T (P Q:list T->Prop) x y, P x -> Q y -> (P +++ Q) (y ++ x)). { + cbv [concat]; eauto. } + + eauto using Trace__concat_app. } + Qed. +End WithParameters. diff --git a/bedrock2/src/bedrock2Examples/metric_lightbulb.v b/bedrock2/src/bedrock2Examples/metric_lightbulb.v new file mode 100644 index 000000000..33f1168fb --- /dev/null +++ b/bedrock2/src/bedrock2Examples/metric_lightbulb.v @@ -0,0 +1,673 @@ +Require Import coqutil.Z.Lia. +Require Import bedrock2.Syntax. +Require Import bedrock2.NotationsCustomEntry coqutil.Macros.WithBaseName. +Require Import bedrock2.FE310CSemantics. +Require Import coqutil.Macros.symmetry. +Require Import coqutil.Byte. +Require Import bedrock2Examples.metric_SPI. +Require Import bedrock2Examples.metric_LAN9250. +From coqutil Require Import Z.div_mod_to_equations. +From coqutil Require Import Word.Interface Map.Interface. +From coqutil.Tactics Require Import letexists eabstract. +From bedrock2 Require Import FE310CSemantics MetricSemantics MetricWeakestPrecondition MetricProgramLogic Array Scalars. +From bedrock2.Map Require Import Separation SeparationLogic. +Require bedrock2.SepAutoArray bedrock2.SepCalls. +Import ZArith. +Local Open Scope Z_scope. + +Section WithParameters. + Import Syntax BinInt String List.ListNotations ZArith. + Context {word: word.word 32} {mem: map.map word Byte.byte}. + Context {word_ok: word.ok word} {mem_ok: map.ok mem}. + Local Open Scope string_scope. Local Open Scope Z_scope. Local Open Scope list_scope. + + Definition lightbulb_loop := func! (p_addr) ~> err { + unpack! bytesWritten, err = recvEthernet(p_addr); + if !err { (* success, packet *) + unpack! err = lightbulb_handle(p_addr, bytesWritten); + err = $0 (* bad packet continue anyway *) + } else if !(err ^ $1) { (* success, no packet *) + err = $0 + } + }. + + Definition recvEthernet := func! (buf) ~> (num_bytes, err) { + num_bytes = $0; + unpack! read, err = lan9250_readword(coq:(0x7C)); (* RX_FIFO_INF *) + require !err else { err = $-1 }; + require (read & coq:((2^8-1)*2^16)) else { err = $1 }; (* nonempty *) + unpack! read, err = lan9250_readword($0x40); (* RX_STATUS_FIFO_PORT *) + require !err else { err = $-1 }; + + num_bytes = read >> $16 & coq:(2^14-1); + (* round up to next word *) + num_bytes = (num_bytes + coq:(4-1)) >> $2; + num_bytes = num_bytes + num_bytes; + num_bytes = num_bytes + num_bytes; + + require (num_bytes < coq:(1520 + 1)) else { err = $2 }; + + i = $0; while (i < num_bytes) { + unpack! read, err = lan9250_readword($0); + if err { err = $-1; i = num_bytes } + else { store4(buf + i, read); i = i + $4 } + } + }. + + Definition lightbulb_handle := func! (packet, len) ~> r { + r = $42; + require (r < len) else { r = $-1 }; + + Oxff = $0xff; + ethertype = (((load1(packet + $12))&Oxff) << $8) | ((load1(packet + $13))&Oxff); + r = coq:(1536 - 1); + require (r < ethertype) else { r = $-1 }; + + r = $23; + r = packet + r; + protocol = (load1(r))&Oxff; + r = $0x11; + require (protocol == r) else { r = $-1 }; + + r = $42; + r = packet + r; + command = (load1(r))&Oxff; + command = command&$1; + + r = $0x1001200c; + io! mmio_val = MMIOREAD(r); + mmio_val = mmio_val & coq:(Z.clearbit (2^32-1) 23); + output! MMIOWRITE(r, mmio_val | command << $23); + + r = $0 + }. + + Definition lightbulb_init := func! { + output! MMIOWRITE($0x10012038, coq:((Z.shiftl (0xf) 2))); + output! MMIOWRITE($0x10012008, coq:((Z.shiftl 1 23))); + unpack! err = lan9250_init() + }. + + Import Datatypes List. + Local Notation bytes := (array scalar8 (word.of_Z 1)). + Local Infix "*" := (sep). + Local Infix "*" := (sep) : type_scope. + + Import TracePredicate. Import TracePredicateNotations. + Import Word.Properties. + Import lightbulb_spec. + Import bedrock2.MetricLogging bedrock2.MetricCosts. + Import MetricProgramLogic.Coercions. + + Instance spec_of_recvEthernet : spec_of "recvEthernet" := fun functions => + forall p_addr (buf:list byte) R m t mc, + (array scalar8 (word.of_Z 1) p_addr buf * R) m -> + length buf = 1520%nat -> + MetricWeakestPrecondition.call functions "recvEthernet" t m [p_addr] mc (fun t' m' rets mc' => + exists bytes_written err, rets = [bytes_written; err] /\ + exists iol, t' = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (word.unsigned err = 0 /\ + exists recv buf, (bytes p_addr recv * bytes (word.add p_addr bytes_written) buf * R) m' /\ lan9250_recv _ recv ioh /\ + word.unsigned bytes_written + Z.of_nat (length buf) = 1520%Z /\ + Z.of_nat (length recv) = word.unsigned bytes_written /\ + ((mc' - mc <= (55+7*bytes_written)*mc_spi_xchg_const + (length ioh)*mc_spi_mul))%metricsH + ) + (word.unsigned err <> 0 /\ exists buf, (array scalar8 (word.of_Z 1) p_addr buf * R) m' /\ length buf = 1520%nat /\ ( + word.unsigned err = 1 /\ lan9250_recv_no_packet _ ioh /\ + ((mc' - mc <= (55 )*mc_spi_xchg_const + (length ioh)*mc_spi_mul))%metricsH + \/ + word.unsigned err = 2 /\ lan9250_recv_packet_too_long _ ioh \/ + word.unsigned err = 2^32-1 /\ TracePredicate.concat TracePredicate.any (spi_timeout word) ioh + )) + ). + + Definition lightbulb_handle_cost := mkMetricLog 552 274 639 203. + Instance spec_of_lightbulb : spec_of "lightbulb_handle" := fun functions => + forall p_addr (buf:list byte) (len:word) R m t mc, + (array scalar8 (word.of_Z 1) p_addr buf * R) m -> + word.unsigned len = Z.of_nat (List.length buf) -> + MetricWeakestPrecondition.call functions "lightbulb_handle" t m [p_addr; len] mc + (fun t' m' rets mc' => exists v, rets = [v] /\ m' = m /\ + exists iol, t' = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ Logic.or + (exists cmd, lightbulb_packet_rep _ cmd buf /\ gpio_set _ 23 cmd ioh /\ word.unsigned v = 0 /\ + (mc' <= lightbulb_handle_cost + mc)%metricsH) + (not (exists cmd, lightbulb_packet_rep _ cmd buf) /\ ioh = nil /\ word.unsigned v <> 0 /\ + (mc' <= addMetricInstructions 226 (addMetricStores 46 (addMetricLoads 283 (addMetricJumps 3 mc))))%metricsH) + ). + + Instance spec_of_lightbulb_loop : spec_of "lightbulb_loop" := fun functions => + forall p_addr buf R m t mc, + (bytes p_addr buf * R) m -> + Z.of_nat (length buf) = 1520 -> + MetricWeakestPrecondition.call functions "lightbulb_loop" t m [p_addr] mc + (fun t' m' rets mc' => exists v, rets = [v] /\ + (exists buf, (bytes p_addr buf * R) m' /\ + Z.of_nat (length buf) = 1520) /\ + exists iol, t' = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ ( + (exists packet cmd, (lan9250_recv _ packet +++ gpio_set _ 23 cmd) ioh /\ lightbulb_packet_rep _ cmd packet /\ word.unsigned v = 0 /\ + ((mc' - mc <= (60+7*length packet)*mc_spi_xchg_const + lightbulb_handle_cost + (length ioh)*mc_spi_mul))%metricsH + ) \/ + (exists packet, (lan9250_recv _ packet) ioh /\ not (exists cmd, lightbulb_packet_rep _ cmd packet) /\ word.unsigned v = 0 /\ + ((mc' - mc <= (60+7*length packet)*mc_spi_xchg_const + lightbulb_handle_cost + (length ioh)*mc_spi_mul))%metricsH + ) \/ + (lan9250_recv_no_packet _ ioh /\ word.unsigned v = 0 /\ + ((mc' - mc <= (60 )*mc_spi_xchg_const + (length ioh)*mc_spi_mul))%metricsH + ) \/ + (lan9250_recv_packet_too_long _ ioh /\ word.unsigned v <> 0) \/ + ((TracePredicate.any +++ (spi_timeout word)) ioh /\ word.unsigned v <> 0) + )). + + Instance spec_of_lightbulb_init : spec_of "lightbulb_init" := fun functions => + forall m t mc, + MetricWeakestPrecondition.call functions "lightbulb_init" t m nil mc + (fun t' m' rets mc' => rets = [] /\ m' = m /\ + exists iol, t' = iol ++ t /\ + exists ioh, mmio_trace_abstraction_relation ioh iol /\ + BootSeq _ ioh + ). + + Import bedrock2.AbsintWordToZ. + Import MetricWeakestPreconditionProperties. + + Local Ltac seplog_use_array_load1 H i := + let iNat := eval cbv in (Z.to_nat i) in + let H0 := fresh in pose proof H as H0; + unshelve SeparationLogic.seprewrite_in @array_index_nat_inbounds H0; + [exact iNat|exact Byte.x00|blia|]; + replace ((word.unsigned (word.of_Z 1) * Z.of_nat iNat)%Z) with i in * by (rewrite word.unsigned_of_Z; exact eq_refl). + Local Ltac trans_ltu := + match goal with + | H : word.unsigned ?v <> 0 |- _ => + let v := rdelta.rdelta v in + let __ := lazymatch v with if word.ltu _ _ then word.of_Z 1 else word.of_Z 0 => I end in + eapply Properties.word.if_nonzero in H; rewrite word.unsigned_ltu in H; eapply Z.ltb_lt in H + | H : word.unsigned ?v = 0 |- _ => + let v := rdelta.rdelta v in + let __ := lazymatch v with if word.ltu _ _ then word.of_Z 1 else word.of_Z 0 => I end in + eapply Word.Properties.word.if_zero in H; rewrite word.unsigned_ltu in H; eapply Z.ltb_nlt in H + end. + Local Ltac split_if := + lazymatch goal with + |- MetricWeakestPrecondition.cmd _ ?c _ _ _ _ ?post => + let c := eval hnf in c in + lazymatch c with + | cmd.cond _ _ _ => letexists; letexists; split; [solve[repeat straightline]|split] + end + end. + + Local Ltac metrics' := + repeat match goal with | H := _ : MetricLog |- _ => subst H end; + cost_unfold; + repeat match goal with + | H: context [?x] |- _ => is_const x; let t := type of x in constr_eq t constr:(MetricLog); + progress cbv beta delta [x] in * + | |- context [?x] => is_const x; let t := type of x in constr_eq t constr:(MetricLog); + progress cbv beta delta [x] in * + end; + cbn -[Z.add Z.mul Z.of_nat] in *; + rewrite ?List.app_length, ?List.length_cons, ?List.length_nil, ?List.firstn_length, ?LittleEndianList.length_le_split in *; + flatten_MetricLog; repeat unfold_MetricLog; repeat simpl_MetricLog; try blia. + + Local Hint Mode map.map - - : typeclass_instances. (* COQBUG https://github.com/coq/coq/issues/14707 *) + + Lemma lightbulb_init_ok : program_logic_goal_for_function! lightbulb_init. + Proof. + repeat straightline. + eapply MetricWeakestPreconditionProperties.interact_nomem; repeat straightline. + (* mmio *) + 1: letexists; letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr val; cbv [isMMIOAddr]; + rewrite !word.unsigned_of_Z; split; trivial. + cbv -[Z.le Z.lt]. blia. } + repeat straightline. + + repeat (eauto || straightline || split_if || eapply interact_nomem || trans_ltu). + + letexists; letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr0 val0; cbv [isMMIOAddr]; + rewrite !word.unsigned_of_Z; split; trivial. + cbv -[Z.le Z.lt]. blia. } + repeat straightline. + + repeat (eauto || straightline || split_if || eapply interact_nomem || trans_ltu). + + straightline_call; repeat straightline. + eexists; split; trivial. + + 1: repeat (eapply align_trace_cons || exact (eq_sym (List.app_nil_l _)) || eapply align_trace_app). + + eexists; split; cbv [mmio_trace_abstraction_relation]. + 1:repeat (eapply List.Forall2_cons || eapply List.Forall2_nil || eapply List.Forall2_app; eauto). + 1,2 : match goal with + |- mmio_event_abstraction_relation _ _ => + (left+right); eexists _, _; split; exact eq_refl + end. + + cbv [BootSeq]. + eapply concat_app. + { eapply (concat_app _ _ [_] [_]); exact eq_refl. } + + cbv [choice]; intuition idtac. + Qed. + + Lemma lightbulb_loop_ok : program_logic_goal_for_function! lightbulb_loop. + Proof. + repeat (match goal with H : or _ _ |- _ => destruct H; intuition idtac end + || straightline || straightline_call || split_if || ecancel_assumption || eauto || blia); cycle 2. + all : split; [shelve|]. + all : eexists; split. + all: repeat (eapply align_trace_cons || exact (eq_sym (List.app_nil_l _)) || eapply align_trace_app). + all : eexists; split. + all : try subst err; rewrite ?word.unsigned_of_Z. + all : repeat (eapply List.Forall2_cons || eapply List.Forall2_nil || eapply List.Forall2_app || eauto 15 using concat_app). + { subst v. rewrite word.unsigned_xor_nowrap, H10, word.unsigned_of_Z in H4. case (H4 eq_refl). } + { right; right; left; eauto. intuition eauto using concat_app; metrics'. } + { subst v. rewrite word.unsigned_xor_nowrap, H9, word.unsigned_of_Z in H4. inversion H4. } + { subst v. rewrite word.unsigned_xor_nowrap, H9, word.unsigned_of_Z in H4. inversion H4. } + { left; eauto. eexists _, _; intuition eauto using concat_app; metrics'. } + { right; left; eauto. eexists _; intuition eauto using concat_app; metrics'. } + + Unshelve. + all : eexists; split; [ eauto | ]. + all : try seprewrite_in @bytearray_index_merge H6; eauto. + all : try rewrite List.app_length. + all : try blia. + Qed. + + Local Ltac prove_ext_spec := + lazymatch goal with + | |- ext_spec _ _ _ _ _ => split; [shelve|]; split; [trivial|] + end. + + Local Ltac zify_unsigned := + repeat match goal with + | |- context[word.unsigned ?e] => let H := unsigned.zify_expr e in rewrite H; pose proof H + | G : context[word.unsigned ?e] |- _ => let H := unsigned.zify_expr e in rewrite H in G; pose proof H + end; + repeat match goal with H:absint_eq ?x ?x |- _ => clear H end; + repeat match goal with H:?A |- _ => clear H; match goal with G:A |- _ => idtac end end. + + Lemma byte_mask_byte (b : byte) : word.and (word.of_Z (byte.unsigned b)) (word.of_Z 255) = word.of_Z (byte.unsigned b) :> word. + Proof. + eapply word.unsigned_inj; rewrite word.unsigned_and_nowrap. + rewrite !word.unsigned_of_Z. + pose proof byte.unsigned_range b. + cbv [word.wrap]. + rewrite <-!(Z.land_ones _ 32) by (cbv; congruence). + rewrite <-byte.wrap_unsigned at 2. cbv [byte.wrap]. + change (Z.land 255 (Z.ones 32)) with (Z.ones 8). + rewrite <-Z.land_ones by blia. + Z.bitwise. Btauto.btauto. + Qed. + + Lemma lightbulb_handle_ok : program_logic_goal_for_function! lightbulb_handle. + Proof. + repeat (eauto || straightline || split_if || eapply interact_nomem || prove_ext_spec || trans_ltu). + all: subst r. + 1: replace (word.unsigned (word.of_Z 42)) with 42 in * by ZnWords.ZnWords. + 2: { + eexists nil; split; eauto. + eexists nil; split; cbv [mmio_trace_abstraction_relation]; eauto using List.Forall2_nil. + right; repeat split; eauto. + { intros (?&?&?). ZnWords.ZnWords. } + 2,3,4,5: solve [metrics']. + intros HX; rewrite ?word.unsigned_of_Z in HX; inversion HX. } + + seplog_use_array_load1 H 12. + seplog_use_array_load1 H 13. + seplog_use_array_load1 H 23. + seplog_use_array_load1 H 42. + unshelve (repeat (eauto || straightline || split_if || eapply interact_nomem || prove_ext_spec)). + + 1: letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr r; cbv [isMMIOAddr]; + rewrite !word.unsigned_of_Z; split; trivial. + cbv -[Z.le Z.lt]. blia. } + 1: repeat straightline. + 1: repeat straightline; eapply interact_nomem; repeat straightline. + 1: letexists; letexists; split; [exact eq_refl|]; split; [split; trivial|]. + { subst addr r; cbv [isMMIOAddr]; + rewrite !word.unsigned_of_Z; split; trivial. + cbv -[Z.le Z.lt]. blia. } + 1: repeat straightline. + + 1: repeat (eauto || straightline || split_if || eapply interact_nomem || prove_ext_spec || trans_ltu). + + all : eexists; split. + all: repeat (eapply align_trace_cons || exact (eq_sym (List.app_nil_l _))). + all : eexists; split. + + all : repeat (eapply List.Forall2_cons || eapply List.Forall2_nil). + all : + try match goal with + |- mmio_event_abstraction_relation _ _ => + (left+right); eexists _, _; split; exact eq_refl + end. + + all : repeat trans_ltu; + repeat match goal with + | H : word.unsigned ?v <> 0 |- _ => + let v := rdelta.rdelta v in + let __ := lazymatch v with if word.eqb _ _ then word.of_Z 1 else word.of_Z 0 => I end in + eapply Properties.word.if_nonzero in H; eapply word.eqb_true in H + | H : word.unsigned ?v = 0 |- _ => + let v := rdelta.rdelta v in + let __ := lazymatch v with if word.eqb _ _ then word.of_Z 1 else word.of_Z 0 => I end in + eapply Word.Properties.word.if_zero in H; eapply word.eqb_false in H + end; + repeat match goal with x := _ |- _ => subst x end; + repeat match goal with H : _ |- _ => rewrite !byte_mask_byte in H end. + all : repeat straightline. + + 1: { + left. + eexists; repeat split. + all : rewrite ?word.unsigned_of_Z in H6. + all : try eassumption. + 1: blia. + 2: eapply word.unsigned_of_Z. + 2,3,4,5: solve [intuition metrics']. + cbv [gpio_set one existsl concat]. + eexists _, ([_]), ([_]); repeat split; repeat f_equal. + eapply word.unsigned_inj. + rewrite ?byte_mask_byte. + rewrite ?word.unsigned_and_nowrap. + rewrite word.unsigned_of_Z_1. + change 1 with (Z.ones 1). + rewrite Z.land_ones, Z.bit0_mod by blia. + rewrite !word.unsigned_of_Z. + cbv [word.wrap]. + rewrite 2(Z.mod_small _ (2^32)); try exact eq_refl. + 1: match goal with |- 0 <= byte.unsigned ?x < _ => pose proof byte.unsigned_range x end; blia. + clear; Z.div_mod_to_equations; blia. } + + (* parse failures *) + all : right; repeat split; eauto; try solve [metrics']. + 2,4: rewrite word.unsigned_of_Z; intro X; inversion X. + all : intros (?&?&?&?&?). + { rewrite word.unsigned_of_Z in H6; contradiction. } + { apply H6. rewrite word.unsigned_of_Z. exact H8. } + + Unshelve. + all : intros; exact True. + Qed. + + Add Ring wring : (Properties.word.ring_theory (word := word)) + (preprocess [autorewrite with rew_word_morphism], + morphism (Properties.word.ring_morph (word := word)), + constants [Properties.word_cst]). + + Import bedrock2.ZnWords. + Import bedrock2.SepAutoArray bedrock2.SepCalls. + + Lemma recvEthernet_ok : program_logic_goal_for_function! recvEthernet. + Proof. + straightline. + rename H into Hcall; clear H0 H1. rename H2 into H. rename H3 into H0. + repeat (straightline || split_if || straightline_call || eauto 99 || prove_ext_spec || ZnWords). + + 3: { + + refine (MetricLoops.tailrec_earlyout + (HList.polymorphic_list.cons (list byte) (HList.polymorphic_list.cons (mem -> Prop) HList.polymorphic_list.nil)) + ["buf";"num_bytes";"i";"read";"err"] + (fun v scratch R t m buf num_bytes_loop i read err mc => PrimitivePair.pair.mk ( + word.unsigned err = 0 /\ word.unsigned i <= word.unsigned num_bytes /\ + v = word.unsigned i /\ (bytes (word.add buf i) scratch * R) m /\ + List.length scratch = Z.to_nat (word.unsigned (word.sub num_bytes i)) /\ + word.unsigned i mod 4 = word.unsigned num_bytes mod 4 /\ + num_bytes_loop = num_bytes) + (fun T M BUF NUM_BYTES I READ ERR MC => + NUM_BYTES = num_bytes_loop /\ + exists RECV, (bytes (word.add buf i) RECV * R) M /\ + List.length RECV = List.length scratch /\ + exists iol, T = iol ++ t /\ exists ioh, mmio_trace_abstraction_relation ioh iol /\ + (word.unsigned ERR = 0 /\ lan9250_readpacket _ RECV ioh /\ + ((MC - mc <= (5+7*length RECV)*mc_spi_xchg_const + (length ioh)*mc_spi_mul))%metricsH + \/ + word.unsigned ERR = 2^32-1 /\ TracePredicate.concat TracePredicate.any (spi_timeout _) ioh ) ) + ) + _ _ _ _ _ _ _ _); + (* 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 || split_if || eapply interact_nomem || eauto 99) .. | ]. + { exact (Z.gt_wf (word.unsigned num_bytes)). } + + { + repeat (split; [trivial||ZnWords|]). + replace (word.add p_addr i) with p_addr by (subst i; ring). + progress trans_ltu. + + scancel_asm. + Tactics.ssplit. + all : trivial; try listZnWords. + } + + { straightline_call; repeat straightline. + { rewrite word.unsigned_of_Z. cbv; clear. intuition congruence. } + split_if; do 6 straightline. + + (* SPI timeout, break loop *) + { straightline. + straightline. + straightline. + straightline. + (* [repeat straightline] hangs *) + do 5 eexists; split; [repeat straightline|]; []. + left. + repeat straightline. + { subst br0. rewrite word.unsigned_ltu, Z.ltb_irrefl, word.unsigned_of_Z; exact eq_refl. } + eexists; split; eauto. + split; eauto. + eexists; split. + { subst a; eauto. } + eexists; split; eauto. + right; split. + { subst err. rewrite word.unsigned_of_Z. exact eq_refl. } + intuition eauto. } + + (* store *) + do 4 straightline. + trans_ltu. + match goal with + | H: context[word.unsigned (word.sub ?a ?b)] |- _ => + pose proof Properties.word.unsigned_range a; + pose proof Properties.word.unsigned_range b; + let H := fresh in + pose proof word.unsigned_sub a b as H; + unfold word.wrap in H; + rewrite Z.mod_small in H by blia + end. + match goal with H10 : _ ?a0 |- store _ ?a0 _ _ _ => rewrite <- (List.firstn_skipn 4 _) in H10; + SeparationLogic.seprewrite_in (symmetry! @bytearray_index_merge) H10 end. + { instantiate (1:= word.of_Z 4). + rewrite word.unsigned_of_Z. + rewrite List.length_firstn_inbounds; [exact eq_refl|]. Z.div_mod_to_equations. blia. } + do 2 straightline. + match goal with H12:_|-_ => seprewrite_in @scalar32_of_bytes H12 end. + { eapply List.length_firstn_inbounds; Z.div_mod_to_equations; blia. } + straightline. + (* after store *) + do 3 straightline. + (* TODO straightline hangs in Loops.enforce *) + do 5 letexists. split. { repeat straightline. } + right. do 3 letexists. + repeat split; repeat straightline; repeat split. + { intuition idtac. } + { subst i. + rewrite word.unsigned_add; cbv [word.wrap]; rewrite Z.mod_small; + replace (word.unsigned (word.of_Z 4)) with 4. + 2,4: rewrite word.unsigned_of_Z; exact eq_refl. + 1,2: try (Z.div_mod_to_equations; blia). } + { replace (word.add x9 i) + with (word.add (word.add x9 x11) (word.of_Z 4)) by (subst i; ring). + ecancel_assumption. } + { match goal with x1 := _ |- _ => subst x1; rewrite List.length_skipn end. + ZnWords. } + { ZnWords. } + { ZnWords. } + { ZnWords. } + + { letexists; repeat split. + { repeat match goal with x := _ |- _ => is_var x; subst x end; subst. + cbv [scalar32 truncated_word truncate_word truncate_Z truncated_scalar littleendian ptsto_bytes.ptsto_bytes] in *. + progress replace (word.add x9 (word.add x11 (word.of_Z 4))) with + (word.add (word.add x9 x11) (word.of_Z 4)) in * by ring. + SeparationLogic.seprewrite_in (@bytearray_index_merge) H25. + { rewrite word.unsigned_of_Z; exact eq_refl. } { ecancel_assumption. } } + { subst RECV. rewrite List.app_length. + rewrite H26. subst x22. rewrite List.length_skipn. + unshelve erewrite (_ : length (HList.tuple.to_list _) = 4%nat); [exact eq_refl|]. + enough ((4 <= length x7)%nat) by blia. + Z.div_mod_to_equations; blia. } + cbv [truncate_word truncate_Z] in *. + repeat match goal with x := _ |- _ => is_var x; subst x end; subst. + eexists; split. + { rewrite List.app_assoc; eauto. } + eexists; split. + { eapply List.Forall2_app; eauto. } + rewrite HList.tuple.to_list_of_list. + destruct H29; [left|right]; repeat (straightline || split || eauto using TracePredicate.any_app_more). + 2,3,4,5: intuition metrics'. + eapply TracePredicate.concat_app; eauto. + unshelve erewrite (_ : LittleEndianList.le_combine _ = word.unsigned x10); rewrite ?word.of_Z_unsigned; try solve [intuition idtac]. + { + etransitivity. + 1: eapply (LittleEndianList.le_combine_split 4). + eapply Properties.word.wrap_unsigned. } } } + + { eexists; split; eauto. split; eauto. exists nil; split; eauto. + eexists; split; [constructor|]. + left. split; eauto. + split. 2:intuition metrics'. + enough (Hlen : length x7 = 0%nat) by (destruct x7; try solve[inversion Hlen]; exact eq_refl). + PreOmega.zify. + rewrite H13. + subst br. + rewrite word.unsigned_ltu in H11. + destruct (Z.ltb (word.unsigned x11) (word.unsigned num_bytes)) eqn:HJ. + { rewrite word.unsigned_of_Z in H11. inversion H11. } + eapply Z.ltb_nlt in HJ. + ZnWords. } + repeat straightline. + + subst i. + progress replace (Z.to_nat (word.unsigned (word.sub p_addr p_addr) / 1)) with O in * by ZnWords. + rewrite ?word.add_0_r, ?word.sub_0_r, ?Z.mul_1_l, ?Nat.add_0_l, ?Z2Nat.id, ?word.of_Z_unsigned in * by apply word.unsigned_range. + + eexists; split. + 1: { repeat match goal with |- context [?x] => match type of x with list _ => subst x end end. + repeat rewrite List.app_assoc. f_equal. } + eexists; split. + 1:repeat eapply List.Forall2_app; eauto. + destruct H14; [left|right]; repeat straightline; repeat split; eauto. + { progress trans_ltu. + cbn [List.firstn array] in *. + replace (word.unsigned (word.of_Z 1521)) with 1521 in * + by (rewrite word.unsigned_of_Z; exact eq_refl). + eexists _, _; Tactics.ssplit. + { cbn [seps] in *. SeparationLogic.ecancel_assumption. } + { generalize dependent x2. generalize dependent x6. intros. + destruct H5; repeat straightline; try contradiction. + destruct H9; repeat straightline; try contradiction. + eexists _, _; split. + { rewrite <-!List.app_assoc. eauto using TracePredicate.concat_app. } + split; [zify_unsigned; eauto|]. + { cbv beta delta [lan9250_decode_length]. + rewrite H11. rewrite List.firstn_length, Znat.Nat2Z.inj_min. + replace (word.sub num_bytes (word.of_Z 0)) with num_bytes by ring; cbn [List.skipn]. + rewrite ?Znat.Z2Nat.id by eapply word.unsigned_range. + transitivity (word.unsigned num_bytes); [ZnWords|exact eq_refl]. } } + { pose proof word.unsigned_range num_bytes. + rewrite List.length_skipn. blia. } + { rewrite H11, List.length_firstn_inbounds, ?Znat.Z2Nat.id; cbn [List.skipn]. + all: try ZnWords. } + { intuition metrics'; ZnWords. } } + { repeat match goal with H : _ |- _ => rewrite H; intro HX; solve[inversion HX] end. } + { progress trans_ltu; + progress replace (word.unsigned (word.of_Z 1521)) with 1521 in * by + (rewrite word.unsigned_of_Z; exact eq_refl). + all : cbn [seps array List.firstn List.skipn] in *. + eexists _; split; eauto; repeat split; try blia. + { SeparationLogic.seprewrite_in @bytearray_index_merge H10. + { rewrite H11, List.firstn_length. ZnWords. } + eassumption. } + { 1:rewrite List.app_length, List.length_skipn, H11, List.firstn_length. + replace (word.sub num_bytes (word.of_Z 0)) with num_bytes by ring. + enough (Z.to_nat (word.unsigned num_bytes) <= length buf)%nat by ZnWords. + rewrite ?Znat.Z2Nat.id by eapply word.unsigned_range; blia. } + right. right. split; eauto using TracePredicate.any_app_more. } } + + all: eexists; split; + [repeat match goal with |- context [?x] => match type of x with list _ => subst x end end; + rewrite ?List.app_assoc; eauto|]. + all: eexists; split; + [repeat eapply List.Forall2_app; eauto|]. + all: + right; subst err; + split; [intro HX; rewrite word.unsigned_of_Z in HX; inversion HX|]. + all : repeat ((eexists; split; [solve[eauto]|]) || (split; [solve[eauto]|])). + all : rewrite !word.unsigned_of_Z. + + (* two cases of SPI timeout *) + { left; split; [exact eq_refl|] || right. + left; split; [exact eq_refl|] || right. + split; [exact eq_refl|]. + intuition eauto using TracePredicate.any_app_more. } + { left; split; [exact eq_refl|] || right. + left; split; [exact eq_refl|] || right. + split; [exact eq_refl|]. + intuition eauto using TracePredicate.any_app_more. } + { left; split; [exact eq_refl|] || right. + left; split; [exact eq_refl|]. + eexists _, _; split. + 1:eapply TracePredicate.concat_app; try intuition eassumption. + subst v0. + rewrite word.unsigned_ltu in H6. + + destruct (Z.ltb (word.unsigned num_bytes) (word.unsigned (word.of_Z 1521))) eqn:?. + all : rewrite word.unsigned_of_Z in Heqb, H6; try inversion H6. + eapply Z.ltb_nlt in Heqb; revert Heqb. + repeat match goal with |- context [?x] => match type of x with _ => subst x end end. + cbv [lan9250_decode_length]. split. 2: cbn in *; blia. + subst v. rewrite word.unsigned_and_nowrap, word.unsigned_of_Z in H2. eapply H2. } + { left. + split; [exact eq_refl|]. + intuition idtac. { eexists. split; intuition eauto. } + metrics'. } + Defined. + + Import metric_SPI. + + Definition funcs := + &[,lightbulb_init; lan9250_init; lan9250_wait_for_boot; lan9250_mac_write; + lightbulb_loop; lightbulb_handle; recvEthernet; lan9250_writeword; lan9250_readword; + spi_xchg; spi_write; spi_read]. + + Local Ltac specapply s := eapply s; [reflexivity|..]. + + Lemma link_lightbulb_loop : spec_of_lightbulb_loop (map.of_list funcs). + Proof. + specapply lightbulb_loop_ok; + (specapply recvEthernet_ok || specapply lightbulb_handle_ok); + specapply lan9250_readword_ok; specapply spi_xchg_ok; + (specapply spi_write_ok || specapply spi_read_ok). + Qed. + Lemma link_lightbulb_init : spec_of_lightbulb_init (map.of_list funcs). + Proof. + specapply lightbulb_init_ok; specapply lan9250_init_ok; + try (specapply lan9250_wait_for_boot_ok || specapply lan9250_mac_write_ok); + (specapply lan9250_readword_ok || specapply lan9250_writeword_ok); + specapply spi_xchg_ok; + (specapply spi_write_ok || specapply spi_read_ok). + Qed. +End WithParameters. diff --git a/compiler/src/compiler/CompilerInvariant.v b/compiler/src/compiler/CompilerInvariant.v deleted file mode 100644 index 409847301..000000000 --- a/compiler/src/compiler/CompilerInvariant.v +++ /dev/null @@ -1,256 +0,0 @@ -Require Import coqutil.Tactics.rewr. -Require Import coqutil.Map.Interface coqutil.Map.Properties. -Require Import coqutil.Word.Interface coqutil.Word.Properties. -Require Import coqutil.Byte. -Require Import riscv.Utility.bverify. -Require Import bedrock2.Array. -Require Import bedrock2.Map.SeparationLogic. -Require Import compiler.SeparationLogic. -Require Import coqutil.Tactics.Simp. -Require Import compiler.FlatToRiscvCommon. -Require Import compiler.FlatToRiscvFunctions. -Require Import compiler.LowerPipeline. -Require Import compiler.Pipeline. -Require Import compiler.ExprImpEventLoopSpec. -Require Import compiler.ToplevelLoop. -Require Import coqutil.Semantics.OmniSmallstepCombinators. - -(* TODO decide if we want to replace runsTo by eventually everywhere, or move - this compatibility lemma to an appropriate place *) -Lemma runsTo_is_eventually[State: Type](step: State -> (State -> Prop) -> Prop): - forall initial P, runsToNonDet.runsTo step initial P <-> eventually step P initial. -Proof. intros. split; induction 1; try (econstructor; solve [eauto]). Qed. - -Global Existing Instance riscv.Spec.Machine.DefaultRiscvState. - -Open Scope Z_scope. - -Local Open Scope ilist_scope. - -Section Pipeline1. - Context {width: Z}. - Context {BW: Bitwidth width}. - Context {word: word.word width}. - Context {word_ok: word.ok word}. - Context {mem: map.map word byte}. - Context {Registers: map.map Z word}. - Context {string_keyed_map: forall T: Type, map.map string T}. (* abstract T for better reusability *) - Context {ext_spec: Semantics.ExtSpec}. - Context {M: Type -> Type}. - Context {MM: Monad M}. - Context {RVM: RiscvProgram M word}. - Context {PRParams: PrimitivesParams M MetricRiscvMachine}. - Context {word_riscv_ok: RiscvWordProperties.word.riscv_ok word}. - Context {string_keyed_map_ok: forall T, map.ok (string_keyed_map T)}. - Context {Registers_ok: map.ok Registers}. - Context {PR: MetricPrimitives PRParams}. - Context {iset: InstructionSet}. - Context {BWM: bitwidth_iset width iset}. - Context {mem_ok: map.ok mem}. - Context {ext_spec_ok: Semantics.ext_spec.ok ext_spec}. - Context (compile_ext_call : string_keyed_map Z -> Z -> Z -> FlatImp.stmt Z -> list Instruction). - Context (compile_ext_call_correct: forall resvars extcall argvars, - compiles_FlatToRiscv_correctly compile_ext_call compile_ext_call - (FlatImp.SInteract resvars extcall argvars)). - Context (compile_ext_call_length_ignores_positions: forall stackoffset posmap1 posmap2 c pos1 pos2, - List.length (compile_ext_call posmap1 pos1 stackoffset c) = - List.length (compile_ext_call posmap2 pos2 stackoffset c)). - - Add Ring wring : (word.ring_theory (word := word)) - (preprocess [autorewrite with rew_word_morphism], - morphism (word.ring_morph (word := word)), - constants [word_cst]). - - Local Hint Mode word.word - : typeclass_instances. - - Context (ml: MemoryLayout) - (mlOk: MemoryLayoutOk ml). - - Lemma instrencode_cons: forall instr instrs, - instrencode (instr :: instrs) = - HList.tuple.to_list (LittleEndian.split 4 (encode instr)) ++ instrencode instrs. - Proof. intros. reflexivity. Qed. - - Lemma instrencode_app: forall instrs1 instrs2, - instrencode (instrs1 ++ instrs2) = instrencode instrs1 ++ instrencode instrs2. - Proof. - induction instrs1; intros. - - reflexivity. - - change ((a :: instrs1) ++ instrs2) with (a :: instrs1 ++ instrs2). - rewrite !instrencode_cons. - rewrite <-!List.app_assoc. - f_equal. - apply IHinstrs1. - Qed. - - Definition imem(code_start code_pastend: word)(instrs: list Instruction): mem -> Prop := - (ptsto_bytes code_start (instrencode instrs) * - mem_available (word.add code_start (word.of_Z (Z.of_nat (List.length (instrencode instrs))))) - code_pastend)%sep. - - Lemma ptsto_bytes_to_program: forall instrs p_code, - word.unsigned p_code mod 4 = 0 -> - Forall (fun i => verify i iset \/ valid_InvalidInstruction i) instrs -> - iff1 (ptsto_bytes p_code (instrencode instrs)) - (program iset p_code instrs). - Proof. - induction instrs; intros. - - reflexivity. - - simp. unfold program in *. rewrite array_cons. - specialize (IHinstrs (word.add p_code (word.of_Z 4))). - unfold ptsto_instr at 1. - unfold truncated_scalar, littleendian, ptsto_bytes, ptsto_bytes.ptsto_bytes. - simpl. - simpl. - rewrite <- IHinstrs; [|DivisibleBy4.solve_divisibleBy4|assumption]. - wwcancel. - cbn [seps]. - rewrite sep_emp_emp. - match goal with - | |- iff1 (emp ?P) (emp ?Q) => apply (RunInstruction.iff1_emp P Q) - end. - split; intros _; try exact I. - auto. - Qed. - - Lemma ptsto_bytes_range: forall bs (start pastend : word) m a v, - ptsto_bytes start bs m -> - word.unsigned start + Z.of_nat (List.length bs) <= word.unsigned pastend -> - map.get m a = Some v -> - word.unsigned start <= word.unsigned a < word.unsigned pastend. - Proof. - induction bs; intros. - - simpl in *. unfold emp in *. simp. rewrite map.get_empty in H1. discriminate. - - simpl in *. - unfold sep in H. simp. - specialize IHbs with (1 := Hp2). - destr (Z.eqb (word.unsigned a0) (word.unsigned start)). 1: blia. - specialize (IHbs pastend a0 v). - destruct IHbs as [L R]. - + rewrite word.unsigned_add. unfold word.wrap. - eapply Z.le_trans. 2: eassumption. - eapply Z.le_trans - with (m := word.unsigned start + word.unsigned (word.of_Z 1) + Z.of_nat (Datatypes.length bs)). - * apply Z.add_le_mono_r. - apply Z.mod_le. - -- repeat match goal with - | |- context [word.unsigned ?w] => unique pose proof (word.unsigned_range w) - end. - blia. - -- destruct width_cases as [F|F]; simpl in *; rewrite F; reflexivity. - * rewrite word.unsigned_of_Z. - unfold word.wrap. - replace (1 mod 2 ^ width) with 1. 1: blia. - simpl. - destruct width_cases as [F|F]; simpl in *; rewrite F; reflexivity. - + unfold map.split in *. simp. - rewrite map.get_putmany_dec in H1. - destr (map.get mq a0). 1: congruence. - exfalso. - unfold ptsto in *. subst mp. - rewrite map.get_put_dec in H1. - destr (word.eqb start a0). - * apply E. congruence. - * rewrite map.get_empty in H1. discriminate. - + rewrite word.unsigned_add in L. unfold word.wrap in L. - split; try assumption. - eapply Z.le_trans. 2: eassumption. - repeat match goal with - | |- context [word.unsigned ?w] => unique pose proof (word.unsigned_range w) - end. - rewrite Z.mod_small. 1: blia. - split; [blia|]. - eapply Z.le_lt_trans. - 2: exact (proj2 (word.unsigned_range pastend)). - eapply Z.le_trans. 2: eassumption. - rewrite word.unsigned_of_Z. - unfold word.wrap. - replace (1 mod 2 ^ width) with 1. 1: blia. - simpl. - destruct width_cases as [F|F]; simpl in *; rewrite F; reflexivity. - Qed. - - Context (spec: ProgramSpec). - - Definition initial_conditions(initial: MetricRiscvMachine): Prop := - exists srcprog (instrs: list Instruction) positions required_stack_space, - ProgramSatisfiesSpec "init"%string "loop"%string srcprog spec /\ - spec.(datamem_start) = ml.(heap_start) /\ - spec.(datamem_pastend) = ml.(heap_pastend) /\ - compile_prog compile_ext_call ml srcprog = Success (instrs, positions, required_stack_space) /\ - required_stack_space <= word.unsigned (word.sub (stack_pastend ml) (stack_start ml)) / bytes_per_word /\ - word.unsigned ml.(code_start) + Z.of_nat (List.length (instrencode instrs)) <= - word.unsigned ml.(code_pastend) /\ - bvalidInstructions iset instrs = true /\ - (imem ml.(code_start) ml.(code_pastend) instrs * - mem_available ml.(heap_start) ml.(heap_pastend) * - mem_available ml.(stack_start) ml.(stack_pastend))%sep initial.(getMem) /\ - (forall a, word.unsigned ml.(code_start) <= word.unsigned a < word.unsigned ml.(code_pastend) -> - List.In a initial.(getXAddrs)) /\ - initial.(getPc) = ml.(code_start) /\ - initial.(getNextPc) = word.add initial.(getPc) (word.of_Z 4) /\ - regs_initialized.regs_initialized initial.(getRegs) /\ - initial.(getLog) = nil /\ - valid_machine initial. - - Lemma compiler_invariant_proofs: - (forall initial, initial_conditions initial -> ll_inv compile_ext_call ml spec initial) /\ - (forall st, ll_inv compile_ext_call ml spec st -> - GoFlatToRiscv.mcomp_sat (run1 iset) st (ll_inv compile_ext_call ml spec)) /\ - (forall st, ll_inv compile_ext_call ml spec st -> - exists suff, spec.(goodTrace) (suff ++ st.(getLog))). - Proof. - ssplit; intros. - - eapply (establish_ll_inv _ compile_ext_call_correct compile_ext_call_length_ignores_positions). - 1: assumption. - unfold initial_conditions, ToplevelLoop.initial_conditions in *. - simp. - eassert ((ptsto_bytes (code_start ml) (instrencode instrs) * _)%sep initial.(getMem)) as SplitImem by (unfold imem in *; ecancel_assumption). - destruct SplitImem as [i_mem [non_imem [SplitImem [Imem NonImem] ] ] ]. - do 5 eexists. - ssplit; try eassumption. - + unfold subset, footpr, footprint_underapprox, of_list, elem_of, program. - intros a M0. - match goal with - | H: _ |- _ => eapply H - end. - specialize (M0 i_mem). - destruct mlOk. - destruct M0 as [v M0]. - * apply ptsto_bytes_to_program; try assumption. - eapply bvalidInstructions_valid. assumption. - * unfold ptsto_bytes in Imem. - eapply ptsto_bytes_range; try eassumption. - + unfold imem in *. - wcancel_assumption. - unfold ptsto_bytes. - cancel_seps_at_indices 0%nat 0%nat. 2: reflexivity. - eapply iff1ToEq. - destruct mlOk. - eapply ptsto_bytes_to_program; try eassumption. - eapply bvalidInstructions_valid. assumption. - - eapply @ll_inv_is_invariant; eassumption. - - eapply ll_inv_implies_prefix_of_good. eassumption. - Qed. - - Definition good_trace(st: MetricRiscvMachine): Prop := spec.(goodTrace) st.(getLog). - Definition always: (MetricRiscvMachine -> Prop) -> MetricRiscvMachine -> Prop := - always (GoFlatToRiscv.mcomp_sat (run1 iset)). - Definition eventually: (MetricRiscvMachine -> Prop) -> MetricRiscvMachine -> Prop := - eventually (GoFlatToRiscv.mcomp_sat (run1 iset)). - - Lemma always_eventually_good_trace: forall initial, - initial_conditions initial -> - always (eventually good_trace) initial. - Proof. - intros * IC. unfold always, eventually, good_trace. - apply mk_always with (invariant := ll_inv compile_ext_call ml spec). - - apply (proj1 compiler_invariant_proofs _ IC). - - apply (proj1 (proj2 compiler_invariant_proofs)). - - intros st HInv. unfold ll_inv, RiscvEventLoop.runsToGood_Invariant, ll_good in HInv. - apply proj1 in HInv. apply runsTo_is_eventually in HInv. - eapply eventually_weaken. 1: exact HInv. - clear initial IC st HInv. cbv beta. intros. simp. assumption. - Qed. - -End Pipeline1. diff --git a/compiler/src/compiler/ExprImpEventLoopSpec.v b/compiler/src/compiler/ExprImpEventLoopSpec.v index 9fd056417..a074904fa 100644 --- a/compiler/src/compiler/ExprImpEventLoopSpec.v +++ b/compiler/src/compiler/ExprImpEventLoopSpec.v @@ -6,6 +6,7 @@ Require Import bedrock2.Semantics. Require Import compiler.SeparationLogic. Require Import compiler.LowerPipeline. Require Import compiler.Pipeline. +Require Import bedrock2.MetricLogging. Section Params1. Context {width} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}. @@ -19,15 +20,18 @@ Section Params1. datamem_pastend: word; (* trace invariant which holds at the beginning (and end) of each loop iteration, but might not hold in the middle of the loop because more needs to be appended *) - goodTrace: Semantics.trace -> Prop; + goodObservables : Semantics.trace -> MetricLog -> Prop; (* state invariant which holds at the beginning (and end) of each loop iteration *) isReady: Semantics.trace -> mem -> Prop; }. Definition hl_inv(spec: ProgramSpec)(t: Semantics.trace)(m: mem) - (l: locals)(mc: bedrock2.MetricLogging.MetricLog) + (l: locals)(mc: MetricLog) : Prop := (* Restriction: no locals can be shared between loop iterations *) - spec.(isReady) t m /\ spec.(goodTrace) t. + spec.(isReady) t m /\ spec.(goodObservables) t mc. + + + Definition eventLoopJumpMetrics mc := addMetricInstructions 1 (addMetricJumps 1 (addMetricLoads 1 mc)). Local Set Warnings "-cannot-define-projection". @@ -45,7 +49,7 @@ Section Params1. get_loop_body: map.get (map.of_list e : env) loop_f = Some (nil, nil, loop_body); loop_body_correct: forall t m l mc, hl_inv spec t m l mc -> - MetricSemantics.exec (map.of_list e) loop_body t m l mc (hl_inv spec); + MetricSemantics.exec (map.of_list e) loop_body t m l mc (fun t m l mc => hl_inv spec t m l (eventLoopJumpMetrics mc)); }. End Params1. diff --git a/compiler/src/compiler/ForeverSafe.v b/compiler/src/compiler/ForeverSafe.v index 7bf0e073f..b952f070c 100644 --- a/compiler/src/compiler/ForeverSafe.v +++ b/compiler/src/compiler/ForeverSafe.v @@ -32,12 +32,12 @@ Section ForeverSafe. Variable iset: Decode.InstructionSet. Lemma extend_runsTo_to_good_trace: - forall (safe: RiscvMachineL -> Prop) (good_trace: trace -> Prop), - (forall st, safe st -> good_trace st.(getLog)) -> + forall (safe: RiscvMachineL -> Prop) (good_observables: trace -> MetricLog -> Prop), + (forall st, safe st -> good_observables st.(getLog) st.(getMetrics)) -> forall (st : RiscvMachineL), valid_machine st -> runsTo (mcomp_sat (run1 iset)) st safe -> - exists rest : trace, good_trace (rest ++ getLog st). + exists rest mc, good_observables (rest ++ getLog st) mc. Proof. intros ? ? safe2good st V R. induction R. - exists nil. rewrite List.app_nil_l. eauto. diff --git a/compiler/src/compiler/RiscvEventLoop.v b/compiler/src/compiler/RiscvEventLoop.v index cd82e5bf3..decaec5e4 100644 --- a/compiler/src/compiler/RiscvEventLoop.v +++ b/compiler/src/compiler/RiscvEventLoop.v @@ -66,12 +66,14 @@ Section EventLoop. Hypothesis goodReadyState_checks_PC: forall done m, goodReadyState done m -> m.(getPc) = if done then pc_end else pc_start. + Definition eventLoopJumpMetrics mc := addMetricInstructions 1 (addMetricJumps 1 (addMetricLoads 1 mc)). + Hypothesis goodReadyState_preserved_by_jump_back: - forall (state: RiscvMachineL) newMetrics, + forall (state: RiscvMachineL), goodReadyState true state -> let state' := (withPc pc_start (withNextPc (word.add pc_start (word.of_Z 4)) - (withMetrics newMetrics state))) in + (withMetrics (eventLoopJumpMetrics state.(getMetrics)) state))) in valid_machine state' -> goodReadyState false state'. diff --git a/compiler/src/compiler/ToplevelLoop.v b/compiler/src/compiler/ToplevelLoop.v index 99a63f567..5e70b5c07 100644 --- a/compiler/src/compiler/ToplevelLoop.v +++ b/compiler/src/compiler/ToplevelLoop.v @@ -48,7 +48,11 @@ Require Import coqutil.Tactics.autoforward. Require Import compiler.FitsStack. Require Import compiler.Pipeline. Require Import compiler.LowerPipeline. -Require Import compiler.ExprImpEventLoopSpec. +Require Import coqutil.Semantics.OmniSmallstepCombinators. + +Lemma runsTo_is_eventually[State: Type](step: State -> (State -> Prop) -> Prop): + forall initial P, runsToNonDet.runsTo step initial P <-> eventually step P initial. +Proof. intros. split; induction 1; try (econstructor; solve [eauto]). Qed. Global Existing Instance riscv.Spec.Machine.DefaultRiscvState. @@ -93,14 +97,13 @@ Section Pipeline1. Context (compile_ext_call_length_ignores_positions: forall stackoffset posmap1 posmap2 c pos1 pos2, List.length (compile_ext_call posmap1 pos1 stackoffset c) = List.length (compile_ext_call posmap2 pos2 stackoffset c)). - Context (ml: MemoryLayout) - (mlOk: MemoryLayoutOk ml). - + Context (init_f : string). + Context (loop_f : string). + Context + (ml: MemoryLayout) + (prog : (list (string * (list string * list string * Syntax.cmd)))). Let init_sp := word.unsigned ml.(stack_pastend). - - Local Notation source_env := (list (string * (list string * list string * Syntax.cmd))). - - (* All riscv machine code, layed out from low to high addresses: *) + (* 1) Initialize stack pointer *) Let init_sp_insts := FlatToRiscvDef.compile_lit iset RegisterNames.sp init_sp. Let init_sp_pos := ml.(code_start). @@ -117,58 +120,61 @@ Section Pipeline1. (* 5) Code of the compiled functions *) Let functions_pos := word.add backjump_pos (word.of_Z 4). - Definition compile_prog(prog: source_env): result (list Instruction * list (string * Z) * Z) := + Definition compile_prog: result (list Instruction * list (string * Z) * Z) := '(functions_insts, positions, required_stack_space) <- compile compile_ext_call prog;; - 'init_fun_pos <- match map.get (map.of_list positions) "init" with + 'init_fun_pos <- match map.get (map.of_list positions) init_f with | Some p => Success p - | None => error:("No function named" "init" "found") + | None => error:("No function named" init_f "found") end;; - 'loop_fun_pos <- match map.get (map.of_list positions) "loop" with + 'loop_fun_pos <- match map.get (map.of_list positions) loop_f with | Some p => Success p - | None => error:("No function named" "loop" "found") + | None => error:("No function named" loop_f "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 := List.map (fun '(name, p) => (name, (adjust p))) positions in Success (to_prepend ++ functions_insts, positions, required_stack_space). - Context (spec: ProgramSpec). + Definition loop_overhead := MetricLogging.mkMetricLog 197 195 197 197. + Definition run1 st post := (mcomp_sat (run1 iset) st (fun _ => post)). + Local Notation always := (always run1). + Local Notation eventually := (eventually run1). + Local Notation successively := (successively run1). - (* Holds each time before executing the loop body *) - Definition ll_good(done: bool)(mach: MetricRiscvMachine): Prop := - exists (prog: source_env) - (functions_instrs: list Instruction) (positions: list (string * Z)) - (required_stack_space: Z) - (init_fun_pos loop_fun_pos: Z) (R: mem -> Prop), - compile compile_ext_call prog = Success (functions_instrs, positions, required_stack_space) /\ - required_stack_space <= word.unsigned (word.sub (stack_pastend ml) (stack_start ml)) / bytes_per_word /\ - ProgramSatisfiesSpec "init"%string "loop"%string prog spec /\ - map.get (map.of_list positions) "init"%string = Some init_fun_pos /\ - map.get (map.of_list positions) "loop"%string = Some loop_fun_pos /\ - exists mH, - isReady spec mach.(getLog) mH /\ goodTrace spec mach.(getLog) /\ - mach.(getPc) = word.add loop_pos (word.of_Z (if done then 4 else 0)) /\ - machine_ok functions_pos ml.(stack_start) ml.(stack_pastend) functions_instrs mH R - (program iset init_sp_pos (init_sp_insts ++ - init_insts init_fun_pos ++ - loop_insts loop_fun_pos ++ - backjump_insts)) - mach. - - Definition ll_inv: MetricRiscvMachine -> Prop := runsToGood_Invariant ll_good iset. + Context + (mlOk: MemoryLayoutOk ml) + (loop_progress : Semantics.trace -> Semantics.trace -> MetricLog -> Prop) + (* state invariant which holds at the beginning (and end) of each loop iteration *) + (bedrock2_invariant : Semantics.trace -> mem -> Prop) + (funs_valid: valid_src_funs prog = true) + (init_code: Syntax.cmd.cmd) + (get_init_code: map.get (map.of_list prog : Semantics.env) init_f = Some (nil, nil, init_code)) + (init_code_correct: forall m0 mc0, + mem_available (heap_start ml) (heap_pastend ml)m0 -> + MetricSemantics.exec (map.of_list prog) init_code nil m0 map.empty mc0 (fun t m l mc => bedrock2_invariant t m)) + (loop_body: Syntax.cmd.cmd) + (get_loop_body: map.get (map.of_list prog : Semantics.env) loop_f = Some (nil, nil, loop_body)) + (loop_body_correct: forall t m mc, + bedrock2_invariant t m -> + MetricSemantics.exec (map.of_list prog) loop_body t m map.empty mc (fun t' m l mc' => + (* match compiler correctness theorem:*) + exists retvals : list word, map.getmany_of_list l [] = Some retvals /\ + bedrock2_invariant t' m /\ + forall dmc, metricsLeq dmc (metricsSub (MetricsToRiscv.lowerMetrics (metricsAdd loop_overhead mc')) (MetricsToRiscv.lowerMetrics mc)) -> + loop_progress t t' dmc + (* + (*actual postcondition*) + exists dt, t' = dt ++ t /\ loop_trace dt /\ + (metricsLeq (MetricsToRiscv.lowerMetrics (MetricLogging.metricsSub mc)) (loop_cost dt))%metricsL + *) + )) + (instrs: list Instruction) + (positions : list (string * Z)) + (required_stack_space: Z) + (R: mem -> Prop). - Add Ring wring : (word.ring_theory (word := word)) - (preprocess [autorewrite with rew_word_morphism], - morphism (word.ring_morph (word := word)), - constants [word_cst]). - - Definition initial_conditions(initial: MetricRiscvMachine): Prop := - exists (srcprog: source_env) - (instrs: list Instruction) positions (required_stack_space: Z) (R: mem -> Prop), - ProgramSatisfiesSpec "init"%string "loop"%string srcprog spec /\ - spec.(datamem_start) = ml.(heap_start) /\ - spec.(datamem_pastend) = ml.(heap_pastend) /\ - compile_prog srcprog = Success (instrs, positions, required_stack_space) /\ + Definition initial_conditions (initial : MetricRiscvMachine) := + compile_prog = Success (instrs, positions, required_stack_space) /\ required_stack_space <= word.unsigned (word.sub (stack_pastend ml) (stack_start ml)) / bytes_per_word /\ word.unsigned ml.(code_start) + Z.of_nat (List.length (instrencode instrs)) <= word.unsigned ml.(code_pastend) /\ @@ -182,16 +188,10 @@ Section Pipeline1. initial.(getLog) = nil /\ valid_machine initial. - Lemma signed_of_Z_small: forall c, - - 2 ^ 31 <= c < 2 ^ 31 -> - word.signed (word.of_Z c) = c. - Proof. - clear -word_ok BW. - simpl. - intros. - eapply word.signed_of_Z_nowrap. - case width_cases as [E | E]; rewrite E; Lia.lia. - Qed. + Add Ring wring : (word.ring_theory (word := word)) + (preprocess [autorewrite with rew_word_morphism], + morphism (word.ring_morph (word := word)), + constants [word_cst]). Lemma mod_2width_mod_bytes_per_word: forall x, (x mod 2 ^ width) mod bytes_per_word = x mod bytes_per_word. @@ -223,21 +223,38 @@ Section Pipeline1. Local Arguments map.get : simpl never. - Lemma establish_ll_inv: forall (initial: MetricRiscvMachine), + (* Holds each time before executing the loop body *) + Definition riscv_loop_invariant (mach: MetricRiscvMachine): Prop := + exists (functions_instrs: list Instruction) (positions: list (string * Z)) + (init_fun_pos loop_fun_pos: Z), + compile compile_ext_call prog = Success (functions_instrs, positions, required_stack_space) /\ + required_stack_space <= word.unsigned (word.sub (stack_pastend ml) (stack_start ml)) / bytes_per_word /\ + map.get (map.of_list positions) init_f = Some init_fun_pos /\ + map.get (map.of_list positions) loop_f = Some loop_fun_pos /\ + exists mH, + bedrock2_invariant mach.(getLog) mH /\ + mach.(getPc) = loop_pos /\ + machine_ok functions_pos ml.(stack_start) ml.(stack_pastend) functions_instrs mH R + (program iset init_sp_pos (init_sp_insts ++ + init_insts init_fun_pos ++ + loop_insts loop_fun_pos ++ + backjump_insts)) + mach. + + Lemma successively_execute_bedrock2_loop : forall initial, initial_conditions initial -> - ll_inv initial. + eventually (successively (fun s s' => + loop_progress s.(getLog) s'.(getLog) (metricsSub s'.(getMetrics) s.(getMetrics)) + )) initial. Proof. - unfold initial_conditions. - intros. fwd. - unfold ll_inv, runsToGood_Invariant. split; [|assumption]. + intros * IC. + eapply eventually_trans. { instantiate (1:=riscv_loop_invariant ). + unfold initial_conditions in *. + fwd. + eapply runsTo_is_eventually. destruct_RiscvMachine initial. match goal with - | H: context[ProgramSatisfiesSpec] |- _ => rename H into sat - end. - pose proof sat. - destruct sat. - match goal with - | H: compile_prog srcprog = Success _ |- _ => + | H: compile_prog = Success _ |- _ => pose proof H as CP; unfold compile_prog, compile in H end. remember instrs as instrs0. @@ -265,7 +282,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_f = Some ?pos |- _ => rename H into GetPos, pos into f_entry_rel_pos end. subst. @@ -297,21 +314,20 @@ Section Pipeline1. compile_ext_call_length_ignores_positions as P. unfold runsTo in P. specialize P with (argvals := []) - (post := fun t' m' retvals mc' => isReady spec t' m' /\ goodTrace spec t') - (fname := "init"%string). + (post := fun t' m' retvals mc' => bedrock2_invariant t' m') + (fname := init_f). + match goal with |- runsToNonDet.runsTo run1 (mkMetricRiscvMachine _ ?mc_now) _ => + specialize P with (mc:=MetricsToRiscv.raiseMetrics mc_now) end. edestruct P as (init_rel_pos & G & P'); clear P; cycle -1. 1: eapply P' with (p_funcs := word.add loop_pos (word.of_Z 8)) (Rdata := R). all: simpl_MetricRiscvMachine_get_set. 12: { - unfold hl_inv in init_code_correct. move init_code_correct at bottom. do 4 eexists. split. 1: eassumption. split. 1: reflexivity. eapply ExprImp.weaken_exec. - refine (init_code_correct _ _ _). - replace (datamem_start spec) with (heap_start ml) by congruence. - replace (datamem_pastend spec) with (heap_pastend ml) by congruence. exact HMem. - - cbv beta. intros * _ HP. exists []. split. 1: reflexivity. exact HP. + - cbv beta. intros * HP. exists []. split. 1: reflexivity. trivial. } 11: { unfold compile. rewrite_match. reflexivity. } all: try eassumption. @@ -381,9 +397,9 @@ Section Pipeline1. + do 2 rapply regs_initialized_put. eassumption. + rewrite map.get_put_diff by (cbv; discriminate). rewrite map.get_put_same. unfold init_sp. rewrite word.of_Z_unsigned. reflexivity. - - cbv beta. unfold ll_good. intros. fwd. + - cbv beta. unfold riscv_loop_invariant . intros. fwd. match goal with - | _: map.get ?positions "loop"%string = Some ?z |- _ => rename z into f_loop_rel_pos + | _: map.get ?positions loop_f = Some ?z |- _ => rename z into f_loop_rel_pos end. unfold compile_prog, compile in CP. fwd. repeat match goal with @@ -409,74 +425,24 @@ Section Pipeline1. * eapply iff1ToEq. unfold init_sp_insts, init_insts, loop_insts, backjump_insts. wwcancel. - Unshelve. exact MetricLogging.EmptyMetricLog. - Qed. - - Lemma ll_inv_is_invariant: forall (st: MetricRiscvMachine), - ll_inv st -> GoFlatToRiscv.mcomp_sat (run1 iset) st ll_inv. - Proof. - intros st. unfold ll_inv. - eapply runsToGood_is_Invariant with (jump := - 4) (pc_start := loop_pos) - (pc_end := word.add loop_pos (word.of_Z 4)). - - intro D. - apply (f_equal word.unsigned) in D. - rewrite word.unsigned_add in D. - rewrite word.unsigned_of_Z in D. - unfold word.wrap in D. - rewrite (Z.mod_small 4) in D; cycle 1. { - simpl. pose proof four_fits. blia. - } - rewrite Z.mod_eq in D by apply pow2width_nonzero. - let ww := lazymatch type of D with context [(2 ^ ?ww)] => ww end in set (w := ww) in *. - progress replace w with (w - 2 + 2) in D at 3 by blia. - rewrite Z.pow_add_r in D by (subst w; destruct width_cases as [E | E]; simpl in *; blia). - change (2 ^ 2) with 4 in D. - match type of D with - | ?x = ?x + 4 - ?A * 4 * ?B => assert (A * B = 1) as C by blia - end. - apply Z.eq_mul_1 in C. - destruct C as [C | C]; - subst w; destruct width_cases as [E | E]; simpl in *; rewrite E in C; cbv in C; discriminate C. - - intros. - unfold ll_good, machine_ok in *. - fwd. - etransitivity. 1: eassumption. - destruct done; solve_word_eq word_ok. - - (* Show that ll_ready (almost) ignores pc, nextPc, and metrics *) - intros. - unfold ll_good, machine_ok in *. - fwd. - destr_RiscvMachine state. - repeat match goal with - | |- exists _, _ => eexists - | |- _ /\ _ => split - | |- _ => progress cbv beta iota - | |- _ => eassumption - | |- _ => reflexivity - end. - + cbn. solve_word_eq word_ok. - + cbn. destruct mlOk. subst. simpl in *. subst loop_pos init_pos. solve_divisibleBy4. - - unfold ll_good, machine_ok. - intros. fwd. assumption. - - cbv. intuition discriminate. - - solve_word_eq word_ok. - - unfold ll_good, machine_ok. - intros. fwd. split. - + eexists. subst loop_pos init_sp_pos init_sp_insts init_pos backjump_pos backjump_insts. - wcancel_assumption. - + eapply shrink_footpr_subset. 1: eassumption. - subst loop_pos init_sp_pos init_sp_insts init_pos backjump_pos backjump_insts. - wwcancel. - - intros. destruct_RiscvMachine initial. unfold ll_good, machine_ok in H. cbn in *. fwd. + } { + clear dependent initial. + intros initial; intros. + eapply eventually_done, mk_successively with (invariant:=riscv_loop_invariant); trivial. + clear dependent initial. + intros initial; intros. + eapply runsTo_is_eventually. + - intros. destruct_RiscvMachine initial. unfold riscv_loop_invariant, machine_ok in H. cbn in *. fwd. (* call loop function (execute the Jal that jumps there) *) - eapply runsToStep. { + eapply runsToStep. + { eapply RunInstruction.run_Jal; cbn. 3: reflexivity. 3: eassumption. 3: { subst loop_pos init_pos init_sp_pos init_sp_insts. wwcancel. } { unfold compile, composed_compile, compose_phases, riscvPhase in *. fwd. match goal with - | H: map.get _ "loop"%string = Some _ |- _ => rename H into GetPos + | H: map.get _ loop_f = Some _ |- _ => rename H into GetPos end. rewrite map.of_list_tuples in GetPos. eapply fun_pos_div4 in GetPos. solve_divisibleBy4. } @@ -486,53 +452,34 @@ Section Pipeline1. { assumption. } } cbn. - intros. destruct_RiscvMachine mid. fwd. + intros mid; intros. destruct_RiscvMachine mid. fwd. (* use compiler correctness for loop body *) - unfold ll_good in *. fwd. - match goal with - | H: ProgramSatisfiesSpec _ _ _ _ |- _ => pose proof H as sat; destruct H - end. - unfold hl_inv in loop_body_correct. - specialize loop_body_correct with (l := map.empty). - lazymatch goal with - | H: context[@word.add ?w ?wo ?x (word.of_Z 0)] |- _ => - replace (@word.add w wo x (word.of_Z 0)) with x in H - end. - 2: solve_word_eq word_ok. + unfold riscv_loop_invariant in *. fwd. subst. + eapply runsTo_trans_cps. { eapply runsTo_weaken. + pose proof compiler_correct compile_ext_call compile_ext_call_correct compile_ext_call_length_ignores_positions as P. - unfold runsTo in P. - specialize P with (argvals := []) - (fname := "loop"%string) - (post := fun t' m' retvals mc' => isReady spec t' m' /\ goodTrace spec t'). - edestruct P as (loop_rel_pos & G & P'); clear P; cycle -1. - 1: eapply P' with (p_funcs := word.add loop_pos (word.of_Z 8)) (Rdata := R) - (ret_addr := word.add loop_pos (word.of_Z 4)). - 12: { - move loop_body_correct at bottom. - do 4 eexists. split. 1: eassumption. split. 1: reflexivity. - eapply ExprImp.weaken_exec. - - eapply loop_body_correct; eauto. - - cbv beta. intros * _ HP. exists []. split. 1: reflexivity. exact HP. - } + specialize P with (fname := loop_f) (argvals := []) . + match goal with |- runsToNonDet.runsTo run1 (mkMetricRiscvMachine _ ?mc_now) _ => + specialize P with (mc:=MetricsToRiscv.raiseMetrics mc_now) end. + + edestruct P as (loop_rel_pos & G & P'); clear P; cycle -2. + 2: eapply P' with (p_funcs := word.add loop_pos (word.of_Z 8)) (Rdata := R) + (ret_addr := word.add loop_pos (word.of_Z 4)); cycle 1. all: try eassumption. all: simpl_MetricRiscvMachine_get_set. + { do 4 eexists. split. 1: eassumption. split. 1: reflexivity. eapply loop_body_correct. eauto. } { apply stack_length_divisible. } { replace loop_rel_pos with loop_fun_pos by congruence. solve_word_eq word_ok. } - { cbn. rewrite map.get_put_same. f_equal. solve_word_eq word_ok. } + { cbn. rewrite map.get_put_same. trivial. } { subst loop_pos init_pos. destruct mlOk. solve_divisibleBy4. } { reflexivity. } { reflexivity. } { reflexivity. } - unfold loop_pos, init_pos. unfold machine_ok. unfold_RiscvMachine_get_set. - repeat match goal with - | x := _ |- _ => subst x - end. repeat match goal with | |- exists _, _ => eexists | |- _ /\ _ => split @@ -540,18 +487,21 @@ Section Pipeline1. | |- _ => eassumption | |- _ => reflexivity end. - * wcancel_assumption. - * eapply rearrange_footpr_subset. 1: eassumption. + * repeat match goal with x := _ |- _ => subst x end. + wcancel_assumption. + * repeat match goal with x := _ |- _ => subst x end. + eapply rearrange_footpr_subset. 1: eassumption. wwcancel. - * match goal with - | H: map.get _ "loop"%string = Some _ |- _ => rename H into GetPos + * repeat match goal with x := _ |- _ => subst x end. + match goal with + | H: map.get _ loop_f = Some _ |- _ => rename H into GetPos end. unfold compile, composed_compile, compose_phases, riscvPhase in *. fwd. repeat match goal with | H: _ |- _ => rewrite map.of_list_tuples in H; move H at bottom end. apply_in_hyps (fun_pos_div4 (iset := iset)). - remember (word.add + progress remember ( (word.add (word.add (code_start ml) (word.of_Z @@ -560,45 +510,63 @@ Section Pipeline1. (Datatypes.length (FlatToRiscvDef.compile_lit iset RegisterNames.sp (word.unsigned (stack_pastend ml))))))) - (word.of_Z 4)) (word.of_Z 0)) as X. + (word.of_Z 4))) as X. solve_divisibleBy4. * eapply regs_initialized_put. eassumption. * rewrite map.get_put_diff by (cbv; discriminate). assumption. - * match goal with - | H: valid_machine {| getMetrics := ?M |} |- valid_machine {| getMetrics := ?M |} => - eqexact.eqexact H; f_equal; f_equal - end. - { f_equal. solve_word_eq word_ok. } - { solve_word_eq word_ok. } - { solve_word_eq word_ok. } + cbv beta. intros. destruct_RiscvMachine final. - repeat match goal with - | x := _ |- _ => subst x - end. - unfold machine_ok in *. simpl_MetricRiscvMachine_get_set. fwd. + unfold machine_ok in *. simpl_MetricRiscvMachine_get_set. - repeat match goal with - | |- exists _, _ => eexists - | |- _ /\ _ => split - | |- _ => progress cbv beta iota - | |- _ => eassumption - | |- _ => reflexivity - end. - * wcancel_assumption. - * eapply rearrange_footpr_subset. 1: eassumption. - wwcancel. - Unshelve. exact MetricLogging.EmptyMetricLog. - Qed. + fwd. + simpl_MetricRiscvMachine_get_set. + eapply runsToStep. { + eapply RunInstruction.run_Jal0 with (jimm20:=-4); simpl_MetricRiscvMachine_get_set; trivial; try reflexivity. - Lemma ll_inv_implies_prefix_of_good: forall st, - ll_inv st -> exists suff, spec.(goodTrace) (suff ++ st.(getLog)). - Proof. - unfold ll_inv, runsToGood_Invariant. intros. fwd. - eapply extend_runsTo_to_good_trace. 2,3: eassumption. - simpl. unfold ll_good, hl_inv, FlatToRiscvCommon.goodMachine. - intros. fwd. eassumption. - Qed. + { eapply rearrange_footpr_subset. 1: eassumption. + subst loop_pos init_sp_pos init_sp_insts init_pos backjump_pos backjump_insts. + set (Datatypes.length _). + wwcancel. } + { subst loop_pos init_sp_pos init_sp_insts init_pos backjump_pos backjump_insts. + use_sep_assumption. + set (Datatypes.length _). + wwcancel. } } + simpl. intros. Simp.simp. + destruct_RiscvMachine mid. + subst. + apply runsToDone. + ssplit; try assumption; cbn; + repeat match goal with + |- context [ {| getPc := ?pc |} ] => progress ring_simplify pc + | |- exists _, _ => eexists + | |- _ /\ _ => split + | |- _ => progress cbv beta iota + | |- _ => eassumption + | |- _ => reflexivity + end; cycle 1. + { subst loop_pos init_sp_pos init_sp_insts init_pos backjump_pos backjump_insts functions_pos. + wcancel_assumption. } + { subst loop_pos init_sp_pos init_sp_insts init_pos backjump_pos backjump_insts functions_pos. + eapply rearrange_footpr_subset. 1: eassumption. + wwcancel. } + { match goal with + | H: valid_machine ?m1 |- valid_machine ?m2 => replace m2 with m1; [exact H|] + end. + f_equal. f_equal; solve_word_eq word_ok. } + { eapply Hp5p2. + repeat match goal with H : MetricLogging.metricsLeq _ _ |- _ => revert H end. + repeat match goal with H : metricsLeq _ _ |- _ => revert H end. + pose I; intros. + repeat ( + cbv [MetricsToRiscv.raiseMetrics MetricsToRiscv.lowerMetrics] in *; + cbv [Spilling.cost_spill_spec cost_compile_spec loop_overhead ] in *; + MetricLogging.unfold_MetricLog; MetricLogging.simpl_MetricLog; + unfold_MetricLog; simpl_MetricLog); + intuition try blia. + } + } + } + Qed. End Pipeline1. diff --git a/compiler/src/compilerExamples/MetricLightbulbInvariant.v b/compiler/src/compilerExamples/MetricLightbulbInvariant.v new file mode 100644 index 000000000..07900565f --- /dev/null +++ b/compiler/src/compilerExamples/MetricLightbulbInvariant.v @@ -0,0 +1,492 @@ +Require Import String. +Require Import Coq.ZArith.ZArith. +Require Import coqutil.Z.Lia. +Require Import Coq.Lists.List. Import ListNotations. +Require Import Coq.Logic.FunctionalExtensionality. +Require Import coqutil.Word.LittleEndian. +Require Import coqutil.Word.Properties. +Require Import coqutil.Map.Interface. +Require Import coqutil.Tactics.Tactics. +Require Import coqutil.Datatypes.PropSet. +Require Import compiler.RunInstruction. +Require Import compiler.RiscvEventLoop. +Require Import compiler.ForeverSafe. +Require Import compiler.GoFlatToRiscv. +Require Import coqutil.Tactics.Simp. +Require Import bedrock2.Syntax bedrock2.Semantics. +Require Import compiler.Pipeline. +Require Import compilerExamples.MMIO. +Require Import compiler.FlatToRiscvDef. +Require Import bedrock2.WeakestPreconditionProperties. +Require Import compiler.SeparationLogic. +Require Import compiler.ToplevelLoop. +Require Import Coq.Classes.Morphisms. +Require Import coqutil.Macros.WithBaseName. +Require Import bedrock2Examples.metric_lightbulb. +Require Import bedrock2Examples.lightbulb_spec. +From Coq Require Import Derive. +From riscv Require Import bverify. +From coqutil Require Import SortedListWord. +From bedrock2 Require Import Syntax NotationsCustomEntry. Import Syntax.Coercions. +From compiler Require Import Symbols. +Local Open Scope Z_scope. + +From coqutil Require Import Word.Naive. +Require Import coqutil.Word.Bitwidth32. +Require Import compiler.NaiveRiscvWordProperties. +#[local] Existing Instance Naive.word. +#[local] Existing Instance Naive.word32_ok. +#[local] Existing Instance SortedListString.map. +#[local] Existing Instance SortedListString.ok. +#[local] Existing Instance SortedListWord.ok. +#[local] Existing Instance SortedListWord.map. +#[local] Instance : FlatToRiscvCommon.bitwidth_iset 32 Decode.RV32IM := eq_refl. + +Definition ml : MemoryLayout (width:=32) := {| + code_start := word.of_Z 0; + code_pastend := word.of_Z (2 ^ 12); + heap_start := word.of_Z (2 ^ 12); + heap_pastend := word.of_Z (2 ^ 12 + 2 ^ 11); + stack_start := word.of_Z (2 ^ 12 + 2 ^ 11); + stack_pastend := word.of_Z (2 ^ 13); +|}. +Definition buffer_addr: Z := word.unsigned ml.(heap_start). + +Lemma ml_ok : MemoryLayout.MemoryLayoutOk ml. Proof. split; cbv; trivial; inversion 1. Qed. + +Definition loop := func! { unpack! _err = lightbulb_loop($buffer_addr) } . +Definition funcs := &[,loop] ++ metric_lightbulb.funcs. +Import metric_LAN9250 metric_SPI. +Local Ltac specapply s := eapply s; [reflexivity|..]. +Lemma link_lightbulb_loop : spec_of_lightbulb_loop (map.of_list funcs). +Proof. + specapply lightbulb_loop_ok; + (specapply recvEthernet_ok || specapply lightbulb_handle_ok); + specapply lan9250_readword_ok; specapply spi_xchg_ok; + (specapply spi_write_ok || specapply spi_read_ok). +Qed. +Lemma link_lightbulb_init : spec_of_lightbulb_init (map.of_list funcs). +Proof. + specapply lightbulb_init_ok; specapply lan9250_init_ok; + try (specapply lan9250_wait_for_boot_ok || specapply lan9250_mac_write_ok); + (specapply lan9250_readword_ok || specapply lan9250_writeword_ok); + specapply spi_xchg_ok; + (specapply spi_write_ok || specapply spi_read_ok). +Qed. + +Derive out SuchThat (compile_prog compile_ext_call "lightbulb_init" "loop" ml funcs = Success (fst (fst out), snd (fst out), snd out)) As out_ok. +Proof. + erewrite <-!surjective_pairing. + match goal with x := _ |- _ => cbv delta [x]; clear x end. + vm_compute. + match goal with |- @Success ?A ?x = Success ?e => + exact (@eq_refl (result A) (@Success A x)) end. +Qed. Optimize Heap. + +Import TracePredicate TracePredicateNotations metric_SPI lightbulb_spec. +Import bedrock2.MetricLogging bedrock2.MetricCosts MetricProgramLogic.Coercions. + +Definition loop_progress t t' dmc := + exists dt, t' = dt ++ t /\ + exists ioh, metric_SPI.mmio_trace_abstraction_relation ioh dt /\ + let dmc := metricsSub (MetricsToRiscv.raiseMetrics dmc) (cost_call PreSpill (cost_lit (prefix "reg_") ""%string loop_overhead)) in + (* spec_of_lightbulb_loop postcondition without return value: *) + (exists packet cmd, (lan9250_recv _ packet +++ gpio_set _ 23 cmd) ioh /\ lightbulb_packet_rep _ cmd packet /\ + ((dmc <= (60+7*length packet)*mc_spi_xchg_const + lightbulb_handle_cost + (length ioh)*mc_spi_mul))%metricsH + ) \/ + (exists packet, (lan9250_recv _ packet) ioh /\ not (exists cmd, lightbulb_packet_rep _ cmd packet) /\ + ((dmc <= (60+7*length packet)*mc_spi_xchg_const + lightbulb_handle_cost + (length ioh)*mc_spi_mul))%metricsH + ) \/ + (lan9250_recv_no_packet _ ioh /\ + ((dmc <= (60 )*mc_spi_xchg_const + lightbulb_handle_cost + (length ioh)*mc_spi_mul))%metricsH) \/ + (lan9250_recv_packet_too_long _ ioh) \/ + ((TracePredicate.any +++ (spi_timeout _)) ioh). + +(* We want to prove a theorem that's purely about RISC-V execution, so we want + to express everything in terms of RISC-V metrics (metricL notation scope), + but that doesn't have all the operators yet *) +Notation RiscvMetrics := Platform.MetricLogging.MetricLog. + +Definition metricAdd(metric: RiscvMetrics -> Z) finalM initialM: Z := + Z.add (metric finalM) (metric initialM). +Definition metricsAdd := Platform.MetricLogging.metricsOp metricAdd. +Infix "+" := metricsAdd : MetricL_scope. + +Definition metricsMul (n : Z) (m : RiscvMetrics) := + riscv.Platform.MetricLogging.mkMetricLog + (n * riscv.Platform.MetricLogging.instructions m) + (n * riscv.Platform.MetricLogging.stores m) + (n * riscv.Platform.MetricLogging.loads m) + (n * riscv.Platform.MetricLogging.jumps m). +Infix "*" := metricsMul : MetricL_scope. + +Definition mc_spi_write_const := + riscv.Platform.MetricLogging.mkMetricLog 348 227 381 204. +Definition mc_spi_read_const := + riscv.Platform.MetricLogging.mkMetricLog 199 116 217 103. +Definition mc_spi_xchg_const := + (mc_spi_write_const + mc_spi_read_const + + riscv.Platform.MetricLogging.mkMetricLog 410 402 414 401)%metricsL. +Definition mc_spi_mul := riscv.Platform.MetricLogging.mkMetricLog 157 109 169 102. +Definition lightbulb_handle_cost := + riscv.Platform.MetricLogging.mkMetricLog 552 274 639 203. + +(* very silly duplication because riscv-coq and bedrock2 don't share any common metrics + library *) +Ltac raise_metrics_const c := + lazymatch c with + | mc_spi_write_const => bedrock2Examples.metric_SPI.mc_spi_write_const + | mc_spi_read_const => bedrock2Examples.metric_SPI.mc_spi_read_const + | mc_spi_xchg_const => bedrock2Examples.metric_SPI.mc_spi_xchg_const + | mc_spi_mul => bedrock2Examples.metric_SPI.mc_spi_mul + | lightbulb_handle_cost => bedrock2Examples.metric_lightbulb.lightbulb_handle_cost + end. + +Ltac raise_metrics_getter g := + lazymatch g with + | riscv.Platform.MetricLogging.instructions => bedrock2.MetricLogging.instructions + | riscv.Platform.MetricLogging.stores => bedrock2.MetricLogging.stores + | riscv.Platform.MetricLogging.loads => bedrock2.MetricLogging.loads + | riscv.Platform.MetricLogging.jumps => bedrock2.MetricLogging.jumps + end. + +Ltac raise_step := + match goal with + | |- context[?g ?c] => + let g' := raise_metrics_getter g in + let c' := raise_metrics_const c in + change (g c) with (g' c') + end. + +(* + let dmc := metricsSub (MetricsToRiscv.raiseMetrics dmc) (cost_call PreSpill (cost_lit (prefix "reg_") ""%string loop_overhead)) in + *) + +(* TODO fix implicit-ness status at definition site *) +Arguments OP {word}. +Arguments lan9250_recv {word}. +Arguments lightbulb_packet_rep {word}. +Arguments gpio_set {word}. +Arguments lan9250_recv_packet_too_long {word}. +Arguments spi_timeout {word}. +Arguments lan9250_recv_no_packet {word}. + +Definition loop_compilation_overhead := + MetricsToRiscv.lowerMetrics + (cost_call PreSpill (cost_lit (prefix "reg_") ""%string loop_overhead)). + +Definition loop_cost(packet_length trace_length: Z): RiscvMetrics := + (60 + 7 * packet_length) * mc_spi_xchg_const + + lightbulb_handle_cost + trace_length * mc_spi_mul + + loop_compilation_overhead. + +(*------desired code width for papers: max 88 columns---------------------------------*) + +Section WithMetricsScope. Open Scope metricsL. + +Definition handle_request_spec(t t': trace)(mc mc': RiscvMetrics) := + exists dt, t' = dt ++ t /\ + exists ioh, metric_SPI.mmio_trace_abstraction_relation ioh dt /\ ( + (* Case 1: Received packet with valid command: *) + (exists packet cmd, + (lan9250_recv packet +++ gpio_set 23 cmd) ioh /\ + lightbulb_packet_rep cmd packet /\ + (mc' - mc <= loop_cost (length packet) (length ioh))) \/ + (* Case 2: Received invalid packet: *) + (exists packet, + (lan9250_recv packet) ioh /\ + not (exists cmd, lightbulb_packet_rep cmd packet) /\ + (mc' - mc <= loop_cost (length packet) (length ioh))) \/ + (* Case 3: Polled, but no new packet was available: *) + (lan9250_recv_no_packet ioh /\ + (mc' - mc <= loop_cost 0 (length ioh))) \/ + (* Case 4: Received too long packet *) + (lan9250_recv_packet_too_long ioh) \/ + (* Case 5: SPI protocol timeout *) + ((TracePredicate.any +++ spi_timeout) ioh)). + +End WithMetricsScope. + +Compute (loop_cost 1520 0). +(* + = {| + Platform.MetricLogging.instructions := 10240858; + Platform.MetricLogging.stores := 7972170; + Platform.MetricLogging.loads := 10829445; + Platform.MetricLogging.jumps := 7576200 + |} + : RiscvMetrics + + (* 10M instructions, less than 0.85ss at 12MHz or less 32ms at 320MHz (plus I/O wait) *) + *) + +Local Notation run1 := (ToplevelLoop.run1 (iset:=Decode.RV32I)). + +Lemma mem_available_to_seplog: forall m0, + LowerPipeline.mem_available (heap_start ml) (heap_pastend ml) m0 -> + exists buf R, + (array ptsto (word.of_Z 1) (word.of_Z buffer_addr) buf * R)%sep m0 /\ + Datatypes.length buf = 1520 :> Z. +Proof. + intros. unfold LowerPipeline.mem_available, ex1 in *. + destruct H as (buf & mp & mq & Sp & P & Q). + unfold emp in P. destruct P as (E & P). subst mp. + eapply map.split_empty_l in Sp. subst mq. + change (Z.of_nat (Datatypes.length buf) = 2048) in P. + unfold LowerPipeline.ptsto_bytes, buffer_addr in *. + (* Set Printing Coercions. *) rewrite word.of_Z_unsigned. + rewrite <- (List.firstn_skipn 1520 buf) in Q. + eapply array_append in Q. + do 2 eexists. split. 1: exact Q. + rewrite List.firstn_length. Lia.lia. +Qed. + +Module riscv. + (* just implicit arguments, as inferred by Coq in previous version + that used Ltac... :P *) + Definition run1 := + (@ToplevelLoop.run1 (2 ^ Nat.log2 32) BW32 (Naive.word (2 ^ Nat.log2 32)) + (@map (2 ^ Nat.log2 32) (Naive.word (2 ^ Nat.log2 32)) word32_ok Init.Byte.byte) + (Z_keyed_SortedListMap.Zkeyed_map (Naive.word (2 ^ Nat.log2 32))) + (FreeMonad.free.free + (@MetricMaterializeRiscvProgram.action 32 BW32 (Naive.word (2 ^ Nat.log2 32))) + (@MetricMaterializeRiscvProgram.result 32 BW32 (Naive.word (2 ^ Nat.log2 32)))) + (@FreeMonad.free.Monad_free + (@MetricMaterializeRiscvProgram.action 32 BW32 (Naive.word (2 ^ Nat.log2 32))) + (@MetricMaterializeRiscvProgram.result 32 BW32 (Naive.word (2 ^ Nat.log2 32)))) + (@MetricMaterializeRiscvProgram.MetricMaterialize 32 BW32 + (Naive.word (2 ^ Nat.log2 32))) + (@MetricMinimalMMIO.MetricMinimalMMIOPrimitivesParams 32 BW32 + (Naive.word (2 ^ Nat.log2 32)) + (@map (2 ^ Nat.log2 32) (Naive.word (2 ^ Nat.log2 32)) word32_ok + Init.Byte.byte) + (Z_keyed_SortedListMap.Zkeyed_map (Naive.word (2 ^ Nat.log2 32))) + (@FE310ExtSpec.FE310_mmio 32 BW32 (Naive.word (2 ^ Nat.log2 32)) + (@map (2 ^ Nat.log2 32) (Naive.word (2 ^ Nat.log2 32)) word32_ok + Init.Byte.byte))) RV32IM). +End riscv. + +Import coqutil.Semantics.OmniSmallstepCombinators. + +Lemma eventually_weaken_step {State} f g P (s : State) : + eventually f P s -> (forall t Q, f t Q -> g t Q) -> eventually g P s. +Proof. induction 1; [econstructor 1 | econstructor 2]; eauto. Qed. + +Lemma always_weaken_step {State} f g P (s : State) : + always f P s -> (forall t Q, f t Q -> g t Q) -> always g P s. +Proof. intros [] ?; eapply mk_always; intuition eauto. Qed. + +Lemma successively_weaken {State} step Q R (s : State) : + successively step Q s -> (forall x y, Q x y -> R x y) -> successively step R s. +Proof. + intros; eapply always_weaken_step; eauto; cbv beta; intros. + eapply eventually_weaken; eauto; cbv beta. + intuition eauto. +Qed. + +Lemma successively_weaken_step {State} f g R (s : State) : + successively f R s -> (forall t Q, f t Q -> g t Q) -> + successively g R s. +Proof. intros; eapply always_weaken_step; eauto; cbv beta; eauto using eventually_weaken_step. Qed. + +Require Import coqutil.Tactics.fwd. + +Theorem metric_lightbulb_correct: forall (initial : MetricRiscvMachine) R, + valid_machine initial -> + getLog initial = [] -> + regs_initialized.regs_initialized (getRegs initial) -> + getNextPc initial = word.add (getPc initial) (word.of_Z 4) -> + getPc initial = code_start ml -> + (program RV32IM (code_start ml) (fst (fst out)) * R * + LowerPipeline.mem_available (heap_start ml) (heap_pastend ml) * + LowerPipeline.mem_available (stack_start ml) (stack_pastend ml))%sep + (getMem initial) -> + subset (footpr (program RV32IM (code_start ml) (fst (fst out)))) + (of_list (getXAddrs initial)) -> + eventually riscv.run1 + (successively riscv.run1 + (fun s s' : MetricRiscvMachine => + handle_request_spec (getLog s) (getLog s') + (getMetrics s) (getMetrics s'))) initial. +Proof. + +intros. + +eapply eventually_weaken. +1: refine ( +let bedrock2_invariant t m := exists buf R, + (Separation.sep (Array.array Scalars.scalar8 (word.of_Z 1) (word.of_Z buffer_addr) buf) R) m /\ + Z.of_nat (Datatypes.length buf) = 1520 in + +successively_execute_bedrock2_loop +(word_riscv_ok:=naive_word_riscv_ok (Nat.log2 32)) +compile_ext_call +ltac:(eapply @compile_ext_call_correct; try exact _) +ltac:(trivial) +"lightbulb_init" +"loop" +ml +funcs +ml_ok +loop_progress +bedrock2_invariant +_ +(snd lightbulb_init) +_ +_ +(snd loop) +_ +_ +_ +_ +_ +_ +_ +ltac:(unfold initial_conditions; Tactics.ssplit) +). + +1:vm_compute; reflexivity. +1:vm_compute; reflexivity. +all : cycle 1. +1:vm_compute; reflexivity. +all : cycle 1. +1:eassumption. +1:eassumption. +1:eassumption. +1:eassumption. +1:eassumption. +all : cycle 1. +all : cycle 1. +all : cycle 1. +all : cycle 1. +1:exact out_ok. +all : cycle -1. +all : cycle -1. +all : cycle -1. +all : cycle -1. +1:eassumption. +1:eassumption. +1:apply Z.lt_le_incl; vm_compute; reflexivity. +1:apply Z.lt_le_incl; vm_compute; reflexivity. +{ + unfold loop_progress, handle_request_spec. + intros. + lazymatch goal with + | H: successively _ _ _ |- _ => rename H into HS + end. + eapply successively_weaken; [exact HS | clear HS]. + cbv beta. + clear. + intros s s' H. + fwd. + eexists. split. 1: eauto. + eexists. split. 1: eauto. + +Ltac t := +cbn [Platform.MetricLogging.instructions Platform.MetricLogging.stores Platform.MetricLogging.loads Platform.MetricLogging.jumps] in *; + cbv [metricsAdd metricsMul] in *; + cbv [metricAdd] in *; + cbv [MetricsToRiscv.raiseMetrics MetricsToRiscv.lowerMetrics] in *; + cbv [Spilling.cost_spill_spec cost_call cost_lit loop_overhead ] in *; + change (isRegStr "") with false in *; + change (prefix ?x ?y) with false in *; + MetricLogging.unfold_MetricLog; MetricLogging.simpl_MetricLog; + unfold_MetricLog; simpl_MetricLog. + + unfold loop_cost, loop_compilation_overhead. + destruct Hp1p1 as [Case1 | [Case2 | [Case3 | [Case4 | Case5] ] ] ]; fwd. + - left. do 2 eexists. do 2 (split; eauto). + clear -Case1p2. forget (getMetrics s') as mc'. forget (getMetrics s) as mc. + destruct mc'. destruct mc. t. + riscv.Platform.MetricLogging.simpl_MetricLog. + repeat raise_step. + Lia.lia. + - right. left. eexists. do 2 (split; eauto). + clear -Case2p2. forget (getMetrics s') as mc'. forget (getMetrics s) as mc. + destruct mc'. destruct mc. t. + riscv.Platform.MetricLogging.simpl_MetricLog. + repeat raise_step. + Lia.lia. + - right. right. left. split; eauto. + clear -Case3p1. forget (getMetrics s') as mc'. forget (getMetrics s) as mc. + destruct mc'. destruct mc. t. + riscv.Platform.MetricLogging.simpl_MetricLog. + repeat raise_step. + Lia.lia. + - right. right. right. left. assumption. + - do 4 right. assumption. +} +{ + intros. + edestruct link_lightbulb_init as (?&?&?&D&?&E&X). + vm_compute in D; inversion D; subst; clear D. + apply map.of_list_zip_nil_values in E; case E as []; subst. + eapply MetricSemantics.exec.weaken; [exact X|]. + cbv beta; intros * ?; intros (?&?&?&?&?&?&?&?&?); subst. + cbv [bedrock2_invariant]. + eapply mem_available_to_seplog. assumption. } +{ cbv [bedrock2_invariant handle_request_spec]. + intros; eapply MetricWeakestPreconditionProperties.sound_cmd. + repeat MetricProgramLogic.straightline. + { eapply MetricSemantics.weaken_call; [eapply link_lightbulb_loop|cbv beta]; try eassumption. + intros * (?&?&?&?&?&?&?&?). + repeat MetricProgramLogic.straightline; exists []; split; [exact eq_refl|]. + split. { eexists _, _; split; eassumption. } + eexists; split; [exact eq_refl|]. + eexists; split; [eassumption|]. + intuition (Simp.simp; eauto). + 1: left; exists packet, cmd; intuition eauto. + 2: right; left; exists packet; intuition eauto. +all : + repeat ( + repeat match goal with | H := _ : MetricLog |- _ => subst H end; + repeat match goal with + | H: context [?x] |- _ => is_const x; let t := type of x in constr_eq t constr:(MetricLog); + progress cbv beta delta [x] in * + | |- context [?x] => is_const x; let t := type of x in constr_eq t constr:(MetricLog); + progress cbv beta delta [x] in * + end; + cbn [Platform.MetricLogging.instructions Platform.MetricLogging.stores Platform.MetricLogging.loads Platform.MetricLogging.jumps] in *; + cbv [MetricsToRiscv.raiseMetrics MetricsToRiscv.lowerMetrics] in *; + cbv [Spilling.cost_spill_spec cost_call cost_lit loop_overhead ] in *; + change (isRegStr "") with false in *; + change (prefix ?x ?y) with false in *; + MetricLogging.unfold_MetricLog; MetricLogging.simpl_MetricLog; + unfold_MetricLog; simpl_MetricLog); + intuition try blia. } } +Qed. + +Import OmniSmallstepCombinators. +Check metric_lightbulb_correct. + +(* +metric_lightbulb_correct + : forall (initial : MetricRiscvMachine) + (R : map (Naive.word (2 ^ Nat.log2 32)) Init.Byte.byte -> Prop), + valid_machine initial -> + getLog initial = [] -> + regs_initialized.regs_initialized (getRegs initial) -> + getNextPc initial = word.add (getPc initial) (word.of_Z 4) -> + getPc initial = code_start ml -> + (program RV32IM (code_start ml) (fst (fst out)) * R * + LowerPipeline.mem_available (heap_start ml) (heap_pastend ml) * + LowerPipeline.mem_available (stack_start ml) (stack_pastend ml))%sep + (getMem initial) -> + subset (footpr (program RV32IM (code_start ml) (fst (fst out)))) + (of_list (getXAddrs initial)) -> + eventually riscv.run1 + (successively riscv.run1 + (fun s s' : MetricRiscvMachine => + handle_request_spec (getLog s) (getLog s') (getMetrics s) (getMetrics s'))) + initial + *) + +Print Assumptions metric_lightbulb_correct. +(* +Axioms: +PropExtensionality.propositional_extensionality : + forall P Q : Prop, P <-> Q -> P = Q +functional_extensionality_dep : + forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), + (forall x : A, f x = g x) -> f = g +*) diff --git a/deps/coqutil b/deps/coqutil index 0833256bc..2a15b1c1a 160000 --- a/deps/coqutil +++ b/deps/coqutil @@ -1 +1 @@ -Subproject commit 0833256bce2a55642c2b0ca37be6bbd27e1af6e1 +Subproject commit 2a15b1c1a973aa2b6ca292b08f3f1710809b4c36 diff --git a/end2end/src/end2end/End2EndLightbulb.v b/end2end/src/end2end/End2EndLightbulb.v index e1437e21b..c81e32ff2 100644 --- a/end2end/src/end2end/End2EndLightbulb.v +++ b/end2end/src/end2end/End2EndLightbulb.v @@ -16,7 +16,7 @@ Require Import end2end.Bedrock2SemanticsForKami. (* TODO why is the ok instance Require riscv.Utility.InstructionNotations. Require bedrock2.Hexdump. Require Import coqutil.Map.Z_keyed_SortedListMap. -Require Import Ltac2.Ltac2. Set Default Proof Mode "Classic". +Set Default Proof Mode "Classic". Open Scope Z_scope. Open Scope string_scope. diff --git a/end2end/src/end2end/End2EndPipeline.v b/end2end/src/end2end/End2EndPipeline.v index dcb547d65..f5dfd5a50 100644 --- a/end2end/src/end2end/End2EndPipeline.v +++ b/end2end/src/end2end/End2EndPipeline.v @@ -188,12 +188,12 @@ Section Connect. Only holds at the beginning/end of each loop iteration, will be transformed into "exists suffix, ..." form later *) Definition goodTraceE(t: list Event): Prop := - exists bedrockTrace, traces_related t bedrockTrace /\ spec.(goodTrace) bedrockTrace. + exists bedrockTrace mc, traces_related t bedrockTrace /\ spec.(goodObservables) bedrockTrace mc. - Definition bedrock2Inv := (fun t m l => forall mc, hl_inv spec t m l mc). + Definition bedrock2Inv := (fun t m l => exists mc, hl_inv spec t m l mc). - Hypothesis goodTrace_implies_related_to_Events: forall (t: list LogItem), - spec.(goodTrace) t -> exists t': list Event, traces_related t' t. + Hypothesis goodTrace_implies_related_to_Events: forall t mc, + spec.(goodObservables) t mc -> exists t': list Event, traces_related t' t. Definition riscvMemInit_all_values: list byte := List.map (get_kamiMemInit memInit) (seq 0 (Z.to_nat (2 ^ memSizeLg))). @@ -364,12 +364,13 @@ Section Connect. end. eapply MetricSemantics.of_metrics_free. eapply WeakestPreconditionProperties.sound_cmd; eauto. - -- simpl. clear. intros. unfold bedrock2Inv in *. eauto. + -- cbv beta. clear. intros. unfold bedrock2Inv in *. eauto. * exact GetLoop. * intros. unfold bedrock2Inv in *. eapply ExprImp.weaken_exec. -- eapply MetricSemantics.of_metrics_free. eapply WeakestPreconditionProperties.sound_cmd; eauto. + eapply Preserve. -- simpl. clear. intros. eauto. + assumption. + assumption.