lightbulb demo runs on FE310 and kami/rv32im

WIP

WIP with bram (backpressure fail)

compiled spi_write ran in simulation

after mit-plv#82....

misaligned instruction on initial call

compile the right functions...

lan9250_readword got 0x87654321 on FE310

WIP

WIP

WIP

it toggles! (on FE310, bedrock2 compiler and gcc)

specify lan9250_writeword

system.v: ignore gpio direction (no freeze)

it toggles on the FPGA!

FE310-compatible workaround for kami lbu bug

prove workaround

bedrock2/src/Examples/LAN9250.v

@@ -42,6 +42,91 @@ Definition lan9250_readword : function :=
     output! MMIOWRITE(SPI_CSMODE_ADDR, addr)
   ))).
 
+Definition lan9250_writeword : function :=
+  let addr : varname := "addr" in
+  let data : varname := "data" in
+  let Oxff : varname := "Oxff" in
+  let eight : varname := "eight" in
+  let ret : varname := "ret" in
+  let err : varname := "err" in
+  let SPI_CSMODE_ADDR := "SPI_CSMODE_ADDR" in
+  ("lan9250_writeword", ((addr::data::nil), (err::nil), bedrock_func_body:(
+    SPI_CSMODE_ADDR = (constr:(Ox"10024018"));
+    io! ret = MMIOREAD(SPI_CSMODE_ADDR);
+    ret = (ret | constr:(2));
+    output! MMIOWRITE(SPI_CSMODE_ADDR, ret);
+
+    (* manually register-allocated, apologies for variable reuse *)
+    Oxff = (constr:(Ox"ff"));
+    eight = (constr:(8));
+    unpack! ret, err = spi_xchg(constr:(Ox"02")); 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 & constr:(Z.lnot 2));
+    output! MMIOWRITE(SPI_CSMODE_ADDR, addr)
+  ))).
+
+Definition MAC_CSR_DATA : Z := Ox"0A8".
+Definition MAC_CSR_CMD : Z := Ox"0A4".
+Definition BYTE_TEST : Z := Ox"64".
+
+Definition lan9250_mac_write : function :=
+  let addr : varname := "addr" in
+  let data : varname := "data" in
+  let err : varname := "err" in
+  ("lan9250_mac_write", ((addr::data::nil), (err::nil), bedrock_func_body:(
+    unpack! err = lan9250_writeword(MAC_CSR_DATA, data);
+    require !err;
+	  unpack! err = lan9250_writeword(MAC_CSR_CMD, constr:(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 HW_CFG : Z := Ox"074".
+
+Definition lan9250_wait_for_boot : function :=
+  let err : varname := "err" in
+  let i : varname := "i" in
+  let byteorder : varname := "byteorder" in
+  ("lan9250_wait_for_boot", (nil, (err::nil), bedrock_func_body:(
+  err = (constr:(0));
+  byteorder = (constr:(0));
+  i = (lightbulb_spec.patience); while (i) { i = (i - constr:(1));
+	  unpack! err, byteorder = lan9250_readword(constr:(Ox"64"));
+    if err { i = (i^i) };
+    if (byteorder == constr:(Ox"87654321")) { i = (i^i) }
+  }
+  ))).
+
+Definition lan9250_init : function :=
+  let hw_cfg : varname := "hw_cfg" in
+  let err : varname := "err" in
+  ("lan9250_init", (nil, (err::nil), bedrock_func_body:(
+	  lan9250_wait_for_boot();
+	  unpack! hw_cfg, err = lan9250_readword(HW_CFG);
+    require !err;
+    hw_cfg = (hw_cfg | constr:(Z.shiftl 1 20)); (* mustbeone *)
+    hw_cfg = (hw_cfg & constr:(Z.lnot (Z.shiftl 1 21))); (* mustbezero *)
+    unpack! err = lan9250_writeword(HW_CFG, hw_cfg);
+    require !err;
+
+    (* 20: full duplex; 18: promiscuous; 2, 3: TXEN/RXEN *)
+  	unpack! err = lan9250_mac_write(constr:(1), constr:(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(constr:(Ox"070"), constr:(Z.lor (Z.shiftl 1 2) (Z.shiftl 1 1)))
+  ))).
+
 Require Import bedrock2.ProgramLogic.
 Require Import bedrock2.FE310CSemantics.
 Require Import coqutil.Word.Interface.
@@ -80,6 +165,149 @@ Proof.
   eapply concat_app; eauto.
 Qed.
 
+Instance spec_of_lan9250_writeword : ProgramLogic.spec_of "lan9250_writeword" := fun functions =>
+  forall t m a v,
+    (Ox"0" <= Word.Interface.word.unsigned a < Ox"400") ->
+  (((WeakestPrecondition.call functions "lan9250_writeword"))) t m [a; v]
+    (fun T M RETS =>
+    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)).
+
+Require Import bedrock2.AbsintWordToZ.
+Require Import coqutil.Tactics.rdelta.
+Require Import coqutil.Z.Lia.
+
+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[Ox ?x] =>
+        let x := rdelta x in
+        let e := eval cbv in (Ox x) 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 := match x with Ox ?x => x | _ => x end 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 [mmio_trace_abstraction_relation]
+  | |- Forall2 mmio_event_abstraction_relation _ _ =>
+      eassumption || eapply Forall2_app || eapply Forall2_nil || eapply Forall2_cons
+  | |- mmio_event_abstraction_relation _ _ =>
+      (left + right); eexists _, _; split; exact eq_refl
+  end.
+
+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].. | ]
+  | |- WeakestPrecondition.cmd _ (cmd.interact _ _ _) _ _ _ _ => eapply WeakestPreconditionProperties.interact_nomem; [  solve[repeat t].. | ]
+  | |- Semantics.ext_spec _ _ _ _ _ => progress cbn [parameters Semantics.ext_spec]
+  end.
+
+From coqutil Require Import Z.div_mod_to_equations.
+Require Import bedrock2.AbsintWordToZ.
+Import Word.Properties.
+
+Lemma lan9250_writeword_ok : program_logic_goal_for_function! lan9250_writeword.
+Proof.
+  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.
+    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: {
+    subst data.
+    subst data1.
+    subst data0.
+    match goal with |- word.unsigned ?x < _ => let H := unsigned.zify_expr x in rewrite H end.
+    pose proof word.unsigned_range v.
+    change (2^Semantics.width) with (2^32) in *.
+    Z.div_mod_to_equations. blia.
+  }
+  repeat t.
+
+  (* aligning regex and mmiotrace, not sure how to do it in a principled way *)
+
+Abort.
+
+
 From coqutil Require Import Z.div_mod_to_equations.
 Lemma lan9250_readword_ok : program_logic_goal_for_function! lan9250_readword.
 Proof.

bedrock2/src/Examples/lightbulb.v

@@ -113,6 +113,7 @@ Definition lightbulb :=
     let port : varname := "port" in
     let mmio_val : varname := "mmio_val" in
     let command : varname := "command" in
+    let Oxff : varname := "Oxff" in
     let MMIOREAD : varname := "MMIOREAD" in
     let MMIOWRITE : varname := "MMIOWRITE" in
     let r : varname := "r" in
@@ -121,19 +122,20 @@ Definition lightbulb :=
     r = (constr:(42));
     require (r < len) else { r = (constr:(-1)) };
 
-    ethertype = ((load1(packet + constr:(12)) << constr:(8)) | (load1(packet + constr:(13))));
+    Oxff = (constr:(Ox"ff"));
+    ethertype = ((((load1(packet + constr:(12)))&Oxff) << constr:(8)) | ((load1(packet + constr:(13)))&Oxff));
     r = (constr:(1536 - 1));
     require (r < ethertype) else { r = (constr:(-1)) };
 
     r = (constr:(23));
     r = (packet + r);
-    protocol = (load1(r));
+    protocol = ((load1(r))&Oxff);
     r = (constr:(Ox"11"));
     require (protocol == r) else { r = (constr:(-1)) };
 
     r = (constr:(42));
     r = (packet + r);
-    command = (load1(r));
+    command = ((load1(r))&Oxff);
     command = (command&constr:(1));
 
     (* pin output enable -- TODO do this in init
@@ -214,11 +216,6 @@ Instance spec_of_iot : spec_of "iot" := fun functions =>
 Require Import bedrock2.AbsintWordToZ.
 Import WeakestPreconditionProperties.
 
-Lemma align_trace_cons {T} x xs cont t (H : xs = cont ++ t) : @cons T x xs = (cons x cont) ++ t.
-Proof. intros. cbn. congruence. Qed.
-Lemma align_trace_app {T} x xs cont t (H : xs = cont ++ t) : @app T x xs = (app x cont) ++ t.
-Proof. intros. cbn. subst. rewrite List.app_assoc; trivial. Qed.
-
 Lemma iot_ok : program_logic_goal_for_function! iot.
 Proof.
   repeat (match goal with H : or _ _ |- _ => destruct H; intuition idtac end
@@ -247,6 +244,20 @@ Local Ltac zify_unsigned :=
   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 : Semantics.byte) : word.and (word.of_Z (word.unsigned b)) (word.of_Z 255) = word.of_Z (word.unsigned b) :> Semantics.word.
+Proof.
+  eapply word.unsigned_inj; rewrite word.unsigned_and_nowrap.
+  rewrite !word.unsigned_of_Z.
+  pose proof word.unsigned_range b.
+  cbv [word.wrap].
+  rewrite <-!(Z.land_ones _ width) by (cbv; congruence).
+  rewrite <-word.wrap_unsigned at 2.
+  change (Z.land 255 (Z.ones width)) with (Z.ones 8).
+  change (Z.ones width) with (Z.ones 32).
+  rewrite <-Z.land_ones by blia.
+  Z.bitwise. Btauto.btauto.
+Qed.
+
 Lemma lightbulb_ok : program_logic_goal_for_function! lightbulb.
 Proof.
   repeat (eauto || straightline || split_if || eapply interact_nomem || prove_ext_spec || trans_ltu).
@@ -290,7 +301,9 @@ Proof.
       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 := word.of_Z _ |- _ => subst x 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.
@@ -299,16 +312,16 @@ Proof.
     1: blia.
     cbv [gpio_set one existsl concat].
     eexists _, ([_]), ([_]); repeat split; repeat f_equal.
-    subst command.
     eapply word.unsigned_inj.
+    rewrite ?byte_mask_byte.
     rewrite ?word.unsigned_and_nowrap.
     change (word.unsigned (word.of_Z 1)) with (Z.ones 1).
     rewrite Z.land_ones, Z.bit0_mod by blia.
     rewrite !word.unsigned_of_Z.
     cbv [word.wrap]; change width with 32 in *.
     rewrite 2(Z.mod_small _ (2^32)); try exact eq_refl.
     1: match goal with |- 0 <= word.unsigned ?x < _ => pose proof word.unsigned_range x end; blia.
-    1: clear; Z.div_mod_to_equations; blia. }
+    clear; Z.div_mod_to_equations; blia. }
 
   (* parse failures *)
   all : right; repeat split; eauto; try solve[intros HX; inversion HX]; intros (?&?&?&?&?).
@@ -596,18 +609,20 @@ Proof.
   exact _.
 Defined.
 
-(*
-Definition x := (iot_ok , lightbulb_ok , recvEthernet_ok , lan9250_readword_ok , spi_read_ok , spi_write_ok).
-Print Assumptions x.
-Axioms:, SortedListString.string_strict_order, TailRecursion.putmany_gather, parameters_ok FE310CSemantics.parameters, SortedList.TODO
-*)
+Lemma link_lightbulb : spec_of_iot (iot::recvEthernet::lightbulb::lan9250_readword::SPI.spi_xchg::SPI.spi_read::SPI.spi_write::nil).
+Proof.
+  eapply iot_ok;
+  (eapply recvEthernet_ok || eapply lightbulb_ok);
+      eapply lan9250_readword_ok; eapply spi_xchg_ok;
+      (eapply spi_write_ok || eapply spi_read_ok).
+Qed.
+(* Print Assumptions link_lightbulb. *)
+(* parameters_ok FE310CSemantics.parameters, SortedList.TODO, TailRecursion.putmany_gather, SortedListString.string_strict_order *)
 
-(*
 From bedrock2 Require Import ToCString Byte Bytedump.
 Local Open Scope bytedump_scope.
+Set Printing Width 999999.
 Goal True.
-(* FIXME: name clashes between this file and lan9250_spec *)
-  let c_code := eval cbv in (of_string (@c_module BasicCSyntax.to_c_parameters [iot; lightbulb; recvEthernet; lan9250_readword; spi_read; spi_write])) in
-  idtac (* c_code *).
+  let c_code := eval cbv in (of_string (@c_module BasicCSyntax.to_c_parameters [lan9250_init; lan9250_wait_for_boot; iot; lightbulb; recvEthernet; lan9250_mac_write; lan9250_writeword; lan9250_readword; SPI.spi_xchg; SPI.spi_read; SPI.spi_write])) in
+  idtac c_code.
 Abort.
-*)