diff --git a/bedrock2/src/Examples/LAN9250.v b/bedrock2/src/Examples/LAN9250.v
index c7dfebf88..30f62c906 100644
--- a/bedrock2/src/Examples/LAN9250.v
+++ b/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.
diff --git a/bedrock2/src/Examples/lightbulb.v b/bedrock2/src/Examples/lightbulb.v
index ebe5b4573..2e2a8f444 100644
--- a/bedrock2/src/Examples/lightbulb.v
+++ b/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,8 +312,8 @@ 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.
@@ -308,7 +321,7 @@ Proof.
     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.
-*)
diff --git a/bedrock2/src/Examples/lightbulb_spec.v b/bedrock2/src/Examples/lightbulb_spec.v
index 0816f3baa..ef223d85b 100644
--- a/bedrock2/src/Examples/lightbulb_spec.v
+++ b/bedrock2/src/Examples/lightbulb_spec.v
@@ -63,7 +63,7 @@ Section LightbulbSpec.
   
   (** LAN9250 *)
   Definition LAN9250_FASTREAD : byte := word.of_Z (Ox"b").
-  (* TODO: byte order? *)
+
   Definition lan9250_fastread4 (a v : word) t := 
     exists a0 a1 v0 v1 v2 v3, (
     spi_begin +++
@@ -80,6 +80,23 @@ Section LightbulbSpec.
     word.unsigned a0 = word.unsigned (word.and a (word.of_Z 255)) /\
     word.unsigned v = LittleEndian.combine 4 ltac:(repeat split; [exact v0|exact v1|exact v2|exact v3]).
 
+  Definition LAN9250_WRITE : byte := word.of_Z (Ox"2").
+
+  Definition lan9250_write4 (a v : word) t := 
+    exists a0 a1 v0 v1 v2 v3, (
+    spi_begin +++
+    spi_xchg_deaf LAN9250_WRITE +++
+    spi_xchg_deaf a1 +++
+    spi_xchg_deaf a0 +++
+    spi_xchg_deaf v0 +++
+    spi_xchg_deaf v1 +++
+    spi_xchg_deaf v2 +++
+    spi_xchg_deaf v3 +++
+    spi_end) t /\
+    word.unsigned a1 = word.unsigned (word.sru a (word.of_Z 8)) /\
+    word.unsigned a0 = word.unsigned (word.and a (word.of_Z 255)) /\
+    word.unsigned v = LittleEndian.combine 4 ltac:(repeat split; [exact v0|exact v1|exact v2|exact v3]).
+
   (* NOTE: we could do this without rounding up to the nearest word, and this
   * might be necessary for other stacks than IP-TCP and IP-UDP *)
   Definition lan9250_decode_length  (status : word) : word :=
@@ -129,3 +146,8 @@ Section LightbulbSpec.
     lightbulb_init +++ lightbulb_step^*.
   *)
 End LightbulbSpec.
+
+Lemma align_trace_cons {T} x xs cont t (H : xs = app cont t) : @cons T x xs = app (cons x cont) t.
+Proof. intros. cbn. congruence. Qed.
+Lemma align_trace_app {T} x xs cont t (H : xs = app cont t) : @app T x xs = app (app x cont) t.
+Proof. intros. cbn. subst. rewrite List.app_assoc; trivial. Qed.
diff --git a/compiler/src/FlatToRiscvDef.v b/compiler/src/FlatToRiscvDef.v
index 3322fb47d..7f1a6777e 100644
--- a/compiler/src/FlatToRiscvDef.v
+++ b/compiler/src/FlatToRiscvDef.v
@@ -237,7 +237,7 @@ Section FlatToRiscv1.
           bElse'
       | SLoop body1 cond body2 =>
           let body1' := compile_stmt mypos body1 in
-          let body2' := compile_stmt (mypos + Z.of_nat (length body1') + 4) body2 in
+          let body2' := compile_stmt (mypos + (Z.of_nat (length body1') + 1) * 4) body2 in
           (* only works if branch lengths are < 2^12 *)
           body1' ++
           [[compile_bcond_by_inverting cond ((Z.of_nat (length body2') + 2) * 4)]] ++
diff --git a/compiler/src/examples/integration.v b/compiler/src/examples/integration.v
index 3c5032fd5..68c703de0 100644
--- a/compiler/src/examples/integration.v
+++ b/compiler/src/examples/integration.v
@@ -23,7 +23,6 @@ Require Import riscv.Platform.MetricRiscvMachine.
 Require Import bedrock2.Byte.
 Require bedrock2.Hexdump.
 Require Import bedrock2.Examples.swap.
-Require Import bedrock2.Examples.SPI.
 
 Open Scope Z_scope.
 Open Scope string_scope.
@@ -35,7 +34,7 @@ Local Existing Instance DefaultRiscvState.
 Local Existing Instance coqutil.Map.SortedListString.map.
 Local Existing Instance coqutil.Map.SortedListString.ok.
 Instance flatToRiscvDef_params: FlatToRiscvDef.FlatToRiscvDef.parameters := {
-  FlatToRiscvDef.FlatToRiscvDef.compile_ext_call argnames fname retnames :=
+  FlatToRiscvDef.FlatToRiscvDef.compile_ext_call retnames fname argnames :=
     if string_dec fname "nop" then [[Addi Register0 Register0 0]]
     else if string_dec fname "MMIOREAD" then
            match retnames, argnames with
@@ -51,25 +50,28 @@ Instance flatToRiscvDef_params: FlatToRiscvDef.FlatToRiscvDef.parameters := {
   FlatToRiscvDef.FlatToRiscvDef.compile_ext_call_length _ := TODO;
   FlatToRiscvDef.FlatToRiscvDef.compile_ext_call_emits_valid _ _ := TODO;
 }.
-
 Notation RiscvMachine := MetricRiscvMachine.
+
+
+Instance mapops: RegAlloc.map.ops (SortedListString.map Z). refine (
+  {| RegAlloc.map.intersect (s1 s2 : SortedListString.map Z) :=
+    {| value := ListLib.list_intersect (fun '(k,v) '(k',v') => andb (_ k k') (_ v v')) (value s1) (value s2); _value_ok := TODO |};
+     RegAlloc.map.default_value := 666;
+  |}).
+- exact String.eqb.
+- exact Z.eqb.
+Defined.
+
 Definition params : Pipeline.parameters. simple refine {|
   Pipeline.locals := _;
   Pipeline.Registers := _;
   Pipeline.ext_spec _ _ := TODO;
   Pipeline.ext_guarantee _ := False;
   Pipeline.PRParams := TODO;
+  Pipeline.src2imp_ops := mapops;
 |}; unshelve (try exact _); apply TODO. Defined.
 Definition flatparams := (FlattenExpr.mk_Syntax_params (@Pipeline.FlattenExpr_parameters params)).
 Instance pipeline_assumptions: @Pipeline.assumptions params. Admitted.
-Instance mapops: RegAlloc.map.ops (SortedListString.map Z). refine (
-  {| RegAlloc.map.intersect (s1 s2 : SortedListString.map Z) :=
-    {| value := ListLib.list_intersect (fun '(k,v) '(k',v') => andb (_ k k') (_ v v')) (value s1) (value s2); _value_ok := TODO |};
-     RegAlloc.map.default_value := 666;
-  |}).
-- exact String.eqb.
-- exact Z.eqb.
-Defined.
 
 (* stack grows from high addreses to low addresses, first stack word will be written to
    (stack_pastend-4), next stack word to (stack_pastend-8) etc *)
@@ -87,10 +89,10 @@ Definition instrencode p : list byte :=
   let word8s := List.flat_map (fun inst => HList.tuple.to_list (LittleEndian.split 4 (encode inst))) p in
   List.map (fun w => Byte.of_Z (word.unsigned w)) word8s.
 
-Definition i : @varname flatparams := "i".
 Require Import coqutil.Z.HexNotation.
+Definition i : @varname flatparams := "i".
 Definition prog := (
-  [swap; swap_swap], (* TODO: spi_read here *)
+  [swap; swap_swap],
   @cmd.call flatparams [] "swap_swap" [expr.literal (2^9); expr.literal (2^9+4)],
   cmd.seq (cmd.set i (expr.load access_size.word (expr.literal (2^9-2))))
   (cmd.seq (cmd.store access_size.word (expr.literal (Ox"1001200c")) (expr.var i))
@@ -109,6 +111,11 @@ Goal True.
                              Sw 0 7 (2^9+4)
                          ]] ++ compile prog)%list%Z) in
   pose r as asm.
+  Import bedrock2.NotationsCustomEntry.
+
+  (* searching for "addi    x2, x2, -" shows where the functions begin, and the first
+     thing they do is to save all used registers onto the stack, so we can look for the
+     max there to see how many registers a function needs *)
 
   let x := eval cbv in (instrencode asm) in
   idtac x.
diff --git a/compiler/src/examples/lightbulb.v b/compiler/src/examples/lightbulb.v
index 9a6a90be5..bb89a1895 100644
--- a/compiler/src/examples/lightbulb.v
+++ b/compiler/src/examples/lightbulb.v
@@ -35,11 +35,19 @@ Local Existing Instance DefaultRiscvState.
 Local Existing Instance coqutil.Map.SortedListString.map.
 Local Existing Instance coqutil.Map.SortedListString.ok.
 Instance flatToRiscvDef_params: FlatToRiscvDef.FlatToRiscvDef.parameters := {
-  FlatToRiscvDef.FlatToRiscvDef.compile_ext_call argnames fname retnames :=
-    if string_dec fname "nop" then
-      [[Addi Register0 Register0 0]]
-    else
-      nil;
+  FlatToRiscvDef.FlatToRiscvDef.compile_ext_call retnames fname argnames :=
+    if string_dec fname "nop" then [[Addi Register0 Register0 0]]
+    else if string_dec fname "MMIOREAD" then
+           match retnames, argnames with
+           | [res], [addr] => [[ Lw res addr 0 ]]
+           | _, _ => nil
+           end
+    else if string_dec fname "MMIOWRITE" then
+           match retnames, argnames with
+           | [], [addr; val] => [[ Sw addr val 0 ]]
+           | _, _ => nil
+           end
+    else  nil;
   FlatToRiscvDef.FlatToRiscvDef.compile_ext_call_length _ := TODO;
   FlatToRiscvDef.FlatToRiscvDef.compile_ext_call_emits_valid _ _ := TODO;
 }.
@@ -63,11 +71,12 @@ Definition params : Pipeline.parameters. simple refine {|
   Pipeline.src2imp_ops := mapops;
 |}; unshelve (try exact _); apply TODO. Defined.
 Definition flatparams := (FlattenExpr.mk_Syntax_params (@Pipeline.FlattenExpr_parameters params)).
+Definition b : @varname flatparams := "b".
 Instance pipeline_assumptions: @Pipeline.assumptions params. Admitted.
 
 (* stack grows from high addreses to low addresses, first stack word will be written to
    (stack_pastend-4), next stack word to (stack_pastend-8) etc *)
-Definition stack_pastend: Z := 1024.
+Definition stack_pastend: Z := 1024*16.
 Definition compile '(functions, initial, reactive) :=
   compile_prog (p:=params) stack_pastend
      (@Build_Program (FlattenExpr.mk_Semantics_params (@Pipeline.FlattenExpr_parameters params))
@@ -81,10 +90,19 @@ Definition instrencode p : list byte :=
   let word8s := List.flat_map (fun inst => HList.tuple.to_list (LittleEndian.split 4 (encode inst))) p in
   List.map (fun w => Byte.of_Z (word.unsigned w)) word8s.
 
+Require Import coqutil.Z.HexNotation.
 Definition prog := (
-  [iot; lightbulb; recvEthernet; lan9250_readword; spi_write; spi_read],
-  @cmd.skip flatparams,
-  @cmd.call flatparams [] "iot" []).
+  [lan9250_init; lan9250_wait_for_boot; lan9250_mac_write;
+  iot; lightbulb; recvEthernet;  lan9250_writeword; lan9250_readword;
+  spi_xchg; spi_write; spi_read],
+  cmd.seq (@cmd.store flatparams access_size.word (expr.literal (Ox"10012038")) (expr.literal (Z.shiftl (Ox"f") 2))) (
+  cmd.seq (@cmd.store flatparams access_size.word (expr.literal (Ox"10012008")) (expr.literal (Z.shiftl 1 23)))
+  (@cmd.call flatparams ["_"] "lan9250_init" [])),
+  (* @cmd.call flatparams ["_"] "iot" [expr.literal (Ox"80000000")] *)
+  @cmd.call flatparams ["_"] "iot" [expr.literal (1024*4)]
+  (* (@cmd.call flatparams ["a"; "b"] "lan9250_readword" [expr.literal (Ox"64")]) *)
+  (* @cmd.call flatparams ["_"] "spi_write" [expr.literal (Ox"a5")] *)
+).
 
 Import riscv.Utility.InstructionNotations.
 Import bedrock2.Hexdump.
@@ -93,11 +111,14 @@ Set Printing Width 108.
 
 
 Goal True.
-  Time
-  let r := eval vm_compute in (([[
+  pose (let '(functions, initial, reactive) := prog in
+    SortedList.value (snd (functions2Riscv (p:=params) (RegAlloc.map.putmany_of_tuples map.empty functions) (List.map fst functions)))) as symbols.
+  cbv in symbols.
+
+
+  let r := eval cbv in (([[
                          ]] ++ compile prog)%list%Z) in
   pose r as asm.
-  Compute (List.length asm).
   Import bedrock2.NotationsCustomEntry.
 
   (* searching for "addi    x2, x2, -" shows where the functions begin, and the first
diff --git a/deps/coqutil b/deps/coqutil
index 043f925db..1ccaccbc3 160000
--- a/deps/coqutil
+++ b/deps/coqutil
@@ -1 +1 @@
-Subproject commit 043f925db108041259771bc8f93d6117245225d2
+Subproject commit 1ccaccbc38663bb9148324028e1272275ca086a5
diff --git a/deps/kami b/deps/kami
index 48a594572..5d4c96a79 160000
--- a/deps/kami
+++ b/deps/kami
@@ -1 +1 @@
-Subproject commit 48a5945723b87c21ee263f167317f6459ae01fe6
+Subproject commit 5d4c96a792aa8d840da618155e3ed7b3c890fa26
diff --git a/processor/integration/Makefile b/processor/integration/Makefile
index 376a3456e..fbb075e98 100644
--- a/processor/integration/Makefile
+++ b/processor/integration/Makefile
@@ -4,13 +4,13 @@ system.vvp: system.v mkTop.v
 	iverilog -y ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/ -y. -o system.vvp system.v
 clean:
 	rm -f system.vvp system.vcd program0.hex program1.hex program2.hex program3.hex system.json system.out.config system.bit system.svf
-program.hex: ../../compiler/src/examples/integration.v
+program.hex: ../../compiler/src/examples/lightbulb.v
 	( cd ../../compiler && coqc -q \
 		-Q ../bedrock2/src bedrock2 \
 		-Q ../deps/coqutil/src coqutil \
 		-Q ../deps/riscv-coq/src riscv \
 		-Q lib lib -Q src compiler  \
-		../compiler/src/examples/integration.v ) > program.hex
+		../compiler/src/examples/lightbulb.v ) > program.hex
 program0.hex: program.hex
 	< $< tr ' ' '\n' | grep . | awk 'NR % 4 == 1' > $@
 program1.hex: program.hex
@@ -20,9 +20,9 @@ program2.hex: program.hex
 program3.hex: program.hex
 	< $< tr ' ' '\n' | grep . | awk 'NR % 4 == 0' > $@
 
-system.json: system.v mkTop.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/FIFO2.v
-	yosys -p "synth_ecp5 -json system.json" $^
+system.json: program0.hex program1.hex program2.hex program3.hex system.v mkTop.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/FIFO2.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/SizedFIFO.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/BRAM1.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/mkBramInst.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/RegFileLoad.v
+	yosys -p "synth_ecp5 -json system.json" system.v mkTop.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/FIFO2.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/SizedFIFO.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/BRAM1.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/mkBramInst.v ../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/RegFileLoad.v
 system.out.config: system.json
-	nextpnr-ecp5 --json system.json --textcfg system.out.config --um5g-85k --package CABGA381 --lpf ecp5evn.lpf --freq 50
+	nextpnr-ecp5 --json system.json --textcfg system.out.config --um5g-85k --package CABGA381 --lpf ecp5evn.lpf --freq 10
 system.bit system.svf: system.out.config
 	ecppack --svf system.svf system.out.config system.bit
diff --git a/processor/integration/ecp5evn.lpf b/processor/integration/ecp5evn.lpf
index 3796b4a72..1b8cdf6c8 100644
--- a/processor/integration/ecp5evn.lpf
+++ b/processor/integration/ecp5evn.lpf
@@ -1,6 +1,13 @@
 LOCATE COMP "clk" SITE "A10";
 IOBUF PORT "clk" IO_TYPE=LVCMOS33;
 
+LOCATE COMP "spi_clk" SITE "F1";
+LOCATE COMP "spi_mosi" SITE "G1";
+LOCATE COMP "spi_miso" SITE "J5";
+LOCATE COMP "spi_csn" SITE "K3";
+
+LOCATE COMP "lightbulb" SITE "K5";
+
 LOCATE COMP "led[0]" SITE "A13";
 LOCATE COMP "led[1]" SITE "A12";
 LOCATE COMP "led[2]" SITE "B19";
@@ -10,6 +17,13 @@ LOCATE COMP "led[5]" SITE "C17";
 LOCATE COMP "led[6]" SITE "A17";
 LOCATE COMP "led[7]" SITE "B17";
 
+IOBUF PORT "spi_clk" IO_TYPE=LVCMOS33;
+IOBUF PORT "spi_mosi" IO_TYPE=LVCMOS33;
+IOBUF PORT "spi_miso" IO_TYPE=LVCMOS33;
+IOBUF PORT "spi_csn" IO_TYPE=LVCMOS33;
+
+IOBUF PORT "lightbulb" IO_TYPE=LVCMOS33;
+
 IOBUF PORT "led[0]" IO_TYPE=LVCMOS33;
 IOBUF PORT "led[1]" IO_TYPE=LVCMOS33;
 IOBUF PORT "led[2]" IO_TYPE=LVCMOS33;
diff --git a/processor/integration/mkTop.v b/processor/integration/mkTop.v
index 6b3fc0080..0f80d6a58 120000
--- a/processor/integration/mkTop.v
+++ b/processor/integration/mkTop.v
@@ -1 +1 @@
-../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/mkTop7.v
\ No newline at end of file
+../../deps/kami/Kami/Ext/BluespecFrontEnd/verilog/mkTopB10.v
\ No newline at end of file
diff --git a/processor/integration/system.v b/processor/integration/system.v
index ff60bfedc..5a7318bd9 100644
--- a/processor/integration/system.v
+++ b/processor/integration/system.v
@@ -78,21 +78,23 @@ endmodule
 module system(
 `ifdef SYNTHESIS
   input wire clk,
+  input wire spi_miso,
 `endif
-  output reg [7:0] led = 8'hff
+  output reg [7:0] led = 8'hff,
+  output reg spi_clk = 0,
+  output wire spi_mosi,
+  output reg spi_csn = 1,
+  output reg lightbulb = 0
 );
-  reg spi_clk = 0;
-  reg spi_cs = 0;
-  wire spi_mosi;
-  wire spi_miso;
 
 `ifndef SYNTHESIS
   reg clk=0;
+  wire spi_miso; assign spi_miso = spi_mosi;
 `endif
 
   reg resetn = 1'b0; always @(posedge clk) begin resetn <= 1'b1; end
 
-  parameter integer LGSZW = 8;
+  parameter integer LGSZW = 12;
   wire [31:0] ram_read;
   wire [64:0] obtain_rq_get;
   wire rdy_obtain_rq_get;
@@ -126,19 +128,15 @@ module system(
     .write(mem_rq_data)
   );
 
-  assign instant_rs_en = en_obtain_rq_get && (mem_rq_addr == 32'h1001200c || mem_rq_addr == 32'h10024048 || mem_rq_addr == 32'h1002404c);
+  assign instant_rs_en = en_obtain_rq_get && (mem_rq_addr == 32'h10012008 || mem_rq_addr == 32'h1001200c || mem_rq_addr == 32'h10024018 || mem_rq_addr == 32'h10024048 || mem_rq_addr == 32'h1002404c || mem_rq_addr == 32'h10012038);
   assign instant_rs =
 	  (!instant_rs_en) ? 32'hxxxxxxxx
 	  : (mem_rq_addr == 32'h1001200c && !mem_rq_iswrite) ? {8'h00, led, 16'h0000}
 	  : (mem_rq_addr == 32'h10024048 && !mem_rq_iswrite) ? {(!spi_tx_rdy), 31'h0}
 	  : (mem_rq_addr == 32'h1002404c && !mem_rq_iswrite) ? {(!spi_tx_rdy), 23'h0, spi_rx_buf}
+    : mem_rq_addr == 32'h10012038 ? 0
 	  : 32'hxxxxxxxx;
-  always @(posedge clk) begin
-    if (en_obtain_rq_get && mem_rq_iswrite && mem_rq_addr == 32'h1001200c) begin
-      led <= mem_rq_data[23:16];
-    end
-  end
-  wire spi_tx_en = en_obtain_rq_get && mem_rq_iswrite && mem_rq_addr == 32'h1001200c;
+  wire spi_tx_en = en_obtain_rq_get && mem_rq_iswrite && mem_rq_addr == 32'h10024048;
   reg [3:0] spi_tx_remaining = 0;
   reg [7:0] spi_tx_buf;
   reg [7:0] spi_rx_buf;
@@ -150,21 +148,65 @@ module system(
       spi_tx_remaining <= 8;
     end else if (spi_tx_remaining && !spi_clk) begin
       spi_clk <= 1;
-      spi_rx_buf = {spi_rx_buf[6:0], spi_mosi};
+      spi_rx_buf = {spi_rx_buf[6:0], spi_miso};
     end else if (spi_clk) begin
       spi_clk <= 0;
       spi_tx_buf <= {spi_tx_buf[6:0], 1'bx};
       spi_tx_remaining <= spi_tx_remaining - 1;
     end
   end
+  wire spi_setcs_en = en_obtain_rq_get && mem_rq_iswrite && mem_rq_addr == 32'h10024018;
+  always @(posedge clk) begin
+    if (spi_setcs_en) begin
+        spi_csn <= !mem_rq_data[1];
+    end
+  end
+
+  reg [5:0] cnt = 0;
+  always @(posedge clk) begin
+    led[6] <= 0;
+    led [5:0] <= ~cnt;
+    if (en_obtain_rq_get && mem_rq_iswrite && mem_rq_addr == 32'h1001200c) begin
+      lightbulb <= mem_rq_data[23];
+      led[7] <= !mem_rq_data[23];
+      cnt <= cnt + 1;
+    end
+  end
 
 `ifndef SYNTHESIS
   always #1 clk = !clk;
   initial begin
     $dumpfile("system.vcd");
-    $dumpvars(1, led, spi_clk, spi_cs, spi_mosi, spi_miso, clk, resetn,
-      rdy_obtain_rq_get, en_obtain_rq_get, mem_rq_iswrite, mem_rq_addr, mem_rq_data, rdy_send_rs_put, ram_rs_en, instant_rs_en, ram_read, spi_tx_buf, spi_rx_buf);
-    #1000 $finish();
+    $dumpvars(1, mkTop.proc_m12_lastPc,
+    led, spi_clk, spi_csn, spi_mosi, spi_miso, clk, resetn,
+      rdy_obtain_rq_get, en_obtain_rq_get, mem_rq_addr, mem_rq_data, mem_rq_iswrite, ram_rs_en, ram_read, instant_rs_en, instant_rs, rdy_send_rs_put, spi_tx_buf, spi_rx_buf, spi_tx_rdy,
+
+       mkTop.CAN_FIRE_RL_proc_m12_reqLd,
+       mkTop.CAN_FIRE_RL_proc_m12_reqSt,
+       mkTop.CAN_FIRE_RL_proc_m12_wbNm,
+       mkTop.CAN_FIRE_RL_proc_m12_wbNmZ,
+       mkTop.WILL_FIRE_RL_proc_m10_decodeLd,
+       mkTop.WILL_FIRE_RL_proc_m10_decodeNm,
+       mkTop.WILL_FIRE_RL_proc_m10_decodeSt,
+       mkTop.WILL_FIRE_RL_proc_m11_execBypass,
+       mkTop.WILL_FIRE_RL_proc_m11_execNm,
+       mkTop.WILL_FIRE_RL_proc_m12_repLd,
+       mkTop.WILL_FIRE_RL_proc_m12_repLdZ,
+       mkTop.WILL_FIRE_RL_proc_m12_repSt,
+       mkTop.WILL_FIRE_RL_proc_m12_reqLd,
+       mkTop.WILL_FIRE_RL_proc_m12_reqSt,
+       mkTop.WILL_FIRE_RL_proc_m12_wbNm,
+       mkTop.WILL_FIRE_RL_proc_m12_wbNmZ,
+       mkTop.WILL_FIRE_RL_proc_m12_wrongEpoch,
+       mkTop.WILL_FIRE_RL_proc_m9_instFetchRq,
+       mkTop.WILL_FIRE_RL_proc_m9_instFetchRs,
+       mkTop.WILL_FIRE_RL_proc_m9_modifyPc,
+       mkTop.WILL_FIRE_RL_proc_m9_pgmInitRq,
+       mkTop.WILL_FIRE_RL_proc_m9_pgmInitRqEnd,
+       mkTop.WILL_FIRE_RL_proc_m9_pgmInitRs,
+       mkTop.WILL_FIRE_RL_proc_m9_pgmInitRsEnd
+);
+    #90000 $finish();
   end
 `endif
 endmodule