diff --git a/ArchSemArm/VMPromising.v b/ArchSemArm/VMPromising.v
index e88baaa..e4896e3 100644
--- a/ArchSemArm/VMPromising.v
+++ b/ArchSemArm/VMPromising.v
@@ -82,6 +82,9 @@ Module Loc := UMPromising.Loc.
 Definition val := bv 64.
 #[global] Typeclasses Transparent val.
 
+Definition val_to_address (v : val) : address :=
+  bv_extract 0 56 v.
+
 (** We also reuse the Msg object from the User-Mode Promising Model. *)
 Module Msg := UMPromising.Msg.
 
@@ -159,11 +162,22 @@ Module Ev.
     | Msg msg => Msg.loc msg =? loc
     | Tlbi _ => false
     end.
+
+  Definition get_msg (ev : t) : option Msg.t :=
+    match ev with
+    | Msg msg => Some msg
+    | _ => None
+    end.
+
+  Definition get_tlbi (ev : t) : option TLBI.t :=
+    match ev with
+    | Tlbi tlbi => Some tlbi
+    | _ => None
+    end.
 End Ev.
 Coercion Ev.Msg : Msg.t >-> Ev.t.
 Coercion Ev.Tlbi : TLBI.t >-> Ev.t.
 
-
 (** A view is just a natural *)
 Definition view := nat.
 #[export] Typeclasses Transparent view.
@@ -200,8 +214,6 @@ Module Memory.
   Definition cut_after : nat -> t -> t := @cut_after Ev.t.
   Definition cut_before : nat -> t -> t := @cut_before Ev.t.
 
-
-
  (** Reads the last write to a location in some memory. Gives the value and the
      timestamp of the write that it read from.
      The timestamp is 0 if reading from initial memory. *)
@@ -215,7 +227,6 @@ Module Memory.
     | Ev.Tlbi _ :: mem' => read_last loc init mem'
     end.
 
-
   (** Read memory at a given timestamp without any weak memory behaviour *)
   Definition read_at (loc : Loc.t) (init : initial) (mem : t) (time : nat) :=
     read_last loc init (cut_before time mem).
@@ -298,7 +309,7 @@ Module Memory.
 
   (** Check that the write at the provided timestamp is indeed to that location
       and that no write to that location have been made by any other thread *)
-  Definition exclusive (loc : Loc.t) (v : view) (mem : t) : bool:=
+  Definition exclusive (loc : Loc.t) (v : view) (mem : t) : bool :=
     match mem !! v with
     | Some (Ev.Msg msg) =>
         if Msg.loc msg =? loc then
@@ -314,7 +325,6 @@ Module Memory.
         else false
     | _ => false
     end.
-
 End Memory.
 Import (hints) Memory.
 
@@ -402,11 +412,15 @@ Definition relaxed_regs : gset reg :=
       GReg VTTBR_EL2].
 
 (** Determine if input register is an unknown register from the architecture *)
-Definition reg_unknown (r : reg) : Prop :=
+Definition is_reg_unknown (r : reg) : Prop :=
   ¬(r ∈ relaxed_regs ∨ r ∈ strict_regs ∨ r = pc_reg).
-Instance Decision_reg_unknown (r : reg) : Decision (reg_unknown r).
+Instance Decision_is_reg_unknown (r : reg) : Decision (is_reg_unknown r).
 Proof. unfold_decide. Defined.
 
+Equations regval_to_val (r : reg) (v : reg_type r) : option val :=
+  regval_to_val (GReg (R_bitvector_64 _)) v := Some v.
+  (* regval_to_val _ _ := None. *)
+
 (** * The thread state *)
 
 Module WSReg.
@@ -421,12 +435,12 @@ Module WSReg.
     if decide (wsreg.(sreg) = sr) is left eq
     then Some $ (ctrans eq wsreg.(val), wsreg.(view))
     else None.
-  
+
   #[global] Instance eta : Settable _ := settable! make <sreg;val;view>.
 End WSReg.
 
-Module LEvent.
-  Inductive t := 
+Module LEv.
+  Inductive t :=
   | Cse (t : nat)
   | Wsreg (wsreg : WSReg.t).
 
@@ -441,7 +455,8 @@ Module LEvent.
     | Wsreg wsreg => Some wsreg
     | _ => None
     end.
-End LEvent.
+End LEv.
+Coercion LEv.Wsreg : WSReg.t >-> LEv.t.
 
 
 (** The thread state *)
@@ -455,7 +470,7 @@ Module TState.
         (* registers values and views. System(relaxed) registers are not
            modified in the [regs] field directly, but instead accumulate changes *)
         regs : dmap reg (λ reg, reg_type reg * view)%type;
-        levs : list LEvent.t;
+        levs : list LEv.t;
 
         (* The coherence views *)
         coh : gmap Loc.t view;
@@ -511,12 +526,12 @@ Module TState.
 
   Definition lev_cur (ts : t) := length ts.(levs).
 
-  Definition filter_wsreg (levs : list LEvent.t) : list WSReg.t :=
-    levs |> list_filter_map LEvent.get_wsreg.
+  Definition filter_wsreg (levs : list LEv.t) : list WSReg.t :=
+    levs |> list_filter_map LEv.get_wsreg.
+
+  Definition filter_cse (levs: list LEv.t) : list view :=
+    levs |> list_filter_map LEv.get_cse.
 
-  Definition filter_cse (levs: list LEvent.t) : list view :=
-    levs |> list_filter_map LEvent.get_cse.
-    
   (** Read the last system register write at system register position s *)
   Definition read_sreg_last (ts : t) (sreg : reg) (s : nat) :=
     let newval :=
@@ -563,9 +578,9 @@ Module TState.
     in
     read_sreg_by_cse ts sreg last_cse
       |$> list_filter_map (
-            λ valv, 
-              if bool_decide (valv.2 ≤ t) 
-              then Some valv
+            λ '(val, view),
+              if bool_decide (view ≤ t)
+              then Some (val, view)
               else None).
 
   (** Read uniformly a register of any kind. *)
@@ -588,7 +603,7 @@ Module TState.
 
   (** Add a system register write event to the local event list *)
   Definition add_wsreg (sreg : reg) (val : reg_type sreg) (v : view) : t → t :=
-    let lev := LEvent.Wsreg (WSReg.make sreg val v) in
+    let lev := LEv.Wsreg (WSReg.make sreg val v) in
     set levs (lev::.).
 
   (** Sets the coherence view of a location *)
@@ -631,14 +646,49 @@ Module TState.
 
   (** Perform a context synchronization event *)
   Definition cse (v : view) : t -> t :=
-    (update vcse v) ∘ (set levs (LEvent.Cse v ::.)).
+    (update vcse v) ∘ (set levs (LEv.Cse v ::.)).
 End TState.
 
 (*** VA helper ***)
 
 Definition Level := fin 4.
+
 #[export] Typeclasses Transparent Level.
 
+Definition root_lvl : Level := 0%fin.
+
+Definition child_lvl (lvl : Level) : option Level :=
+  match lvl in fin n return option Level with
+  | 0 => Some 1
+  | 1 => Some 2
+  | 2 => Some 3
+  | _ => None
+  end%fin.
+
+Lemma child_lvl_add_one (lvl clvl : Level)
+    (CHILD : child_lvl lvl = Some clvl) :
+  lvl + 1 = clvl.
+Proof.
+  unfold child_lvl in CHILD.
+  repeat case_split; cdestruct clvl |- ***.
+Qed.
+
+Definition parent_lvl (lvl : Level) : option Level :=
+  match lvl in fin n return option Level with
+  | 1 => Some 0
+  | 2 => Some 1
+  | 3 => Some 2
+  | _ => None
+  end%fin.
+
+Lemma parent_lvl_sub_one (lvl plvl : Level)
+    (PARENT : parent_lvl lvl = Some plvl) :
+  plvl + 1 = lvl.
+Proof.
+  unfold parent_lvl in PARENT.
+  repeat case_split; cdestruct plvl |- ***.
+Qed.
+
 (* It is important to be consistent on "level_length" and not write it as 9 *
    lvl + 9, otherwise some term won't type because the equality is only
    propositional *)
@@ -653,40 +703,59 @@ Definition prefix_to_va {n : N} (p : bv n) : bv 64 :=
 Definition level_prefix {n : N} (va : bv n) (lvl : Level) : prefix lvl :=
   bv_extract (12 + 9 * (3 - lvl)) (9 * (lvl + 1)) va.
 
+Definition match_prefix_at {n n' : N} (lvl : Level) (va : bv n) (va' : bv n') : Prop :=
+  level_prefix va lvl = level_prefix va' lvl.
+Instance Decision_match_prefix_at {n n' : N} (lvl : Level) (va : bv n) (va' : bv n') :
+  Decision (match_prefix_at lvl va va').
+Proof. unfold_decide. Defined.
+
 Definition level_index {n : N} (va : bv n) (lvl : Level) : bv 9 :=
   bv_extract 0 9 (level_prefix va lvl).
 
+Definition index_to_offset (idx : bv 9) : bv 12 :=
+  bv_concat 12 idx (bv_0 3).
+
 Definition higher_level {n : N} (va : bv n) : bv (n - 9) :=
   bv_extract 9 (n - 9) va.
 
+Definition next_entry_addr {n : N} (addr : bv n) (index : bv 9) : address :=
+  bv_concat 56 (bv_0 8) (bv_concat 48 (bv_extract 12 36 addr) (index_to_offset index)).
+
 Definition next_entry_loc (loc : Loc.t) (index : bv 9) : Loc.t :=
   bv_concat 53 (bv_extract 9 44 loc) index.
 
-(*** TLB ***)
-
-Global Program Instance countable_sigT `{Countable A} (P : A → Type)
-    {eqdepP : EqDepDecision P} {eqP: ∀ a, EqDecision (P a)}
-    {cntP: ∀ a : A, Countable (P a)} : Countable (sigT P) :=
-  (inj_countable
-     (λ sig, (projT1 sig, encode (projT2 sig)))
-     (λ '(a, b),
-       bd ← decode b;
-       Some $ existT a bd)
-     _).
-Next Obligation.
-  intros.
-  cbn.
-  setoid_rewrite decode_encode.
-  hauto lq:on.
-Defined.
+Definition is_valid (e : val) : Prop :=
+  (bv_extract 0 1 e) = 1%bv.
+Instance Decision_is_valid (e : val) : Decision (is_valid e).
+Proof. unfold_decide. Defined.
 
-Module TLB.
-  (* TODO: pair programming to switch to dmaps. *)
+Definition is_table (e : val) : Prop :=
+  (bv_extract 0 2 e) = 3%bv.
+Instance Decision_is_table (e : val) : Decision (is_table e).
+Proof. unfold_decide. Defined.
 
+Definition is_block (e : val) : Prop :=
+  (bv_extract 0 2 e) = 1%bv.
+Instance Decision_is_block (e : val) : Decision (is_block e).
+Proof. unfold_decide. Defined.
+
+Definition is_final (lvl : Level) (e : val) : Prop :=
+  if lvl is 3%fin then (bv_extract 0 2 e) = 3%bv else is_block e.
+Instance Decision_is_final (lvl : Level) (e : val) : Decision (is_final lvl e).
+Proof. unfold_decide. Defined.
+
+Definition is_global (lvl : Level) (e : val) : Prop :=
+  is_final lvl e ∧ (bv_extract 11 1 e) = 0%bv.
+Instance Decision_is_global (lvl : Level) (e : val) : Decision (is_global lvl e).
+Proof. unfold_decide. Defined.
+
+(** * TLB ***)
+
+Module TLB.
+  (** ** TLB types definitions *)
   Module NDCtxt.
     Record t (lvl : Level) :=
-      make
-        {
+      make {
           va : prefix lvl;
           asid : option (bv 16);
         }.
@@ -704,8 +773,8 @@ Module TLB.
     Proof.
       eapply (inj_countable' (fun ndc => (va ndc, asid ndc))
                         (fun x => make x.1 x.2)).
-      sauto.
-    Qed.
+      abstract sauto.
+    Defined.
   End NDCtxt.
 
   Module Ctxt.
@@ -720,12 +789,25 @@ Module TLB.
   Module Entry.
     Definition t (lvl : Level) := vec val (S lvl).
     Definition pte {lvl} (tlbe : t lvl) := Vector.last tlbe.
+
+    Program Definition append {lvl clvl : Level}
+        (tlbe : t lvl)
+        (pte : val)
+        (CHILD : lvl + 1 = clvl) : t clvl :=
+      ctrans _ (tlbe +++ [#pte]).
+    Solve All Obligations with lia.
   End Entry.
   #[export] Typeclasses Transparent Entry.t.
 
   (* Full Entry *)
   Module FE.
     Definition t := { ctxt : Ctxt.t & Entry.t (Ctxt.lvl ctxt) }.
+    Definition ctxt : t → Ctxt.t := projT1.
+    Definition lvl (fe : t) : Level := Ctxt.lvl (ctxt fe).
+    Definition va (fe : t) : prefix (lvl fe) := Ctxt.va (ctxt fe).
+    Definition asid (fe : t) : option (bv 16) := Ctxt.asid (ctxt fe).
+    Definition ptes (fe : t) := projT2 fe.
+    Definition pte (fe : t) := Entry.pte (projT2 fe).
   End FE.
   #[export] Typeclasses Transparent FE.t.
 
@@ -745,141 +827,164 @@ Module TLB.
       get ctxt vatlb
       |> set_map (fun (e : Entry.t (Ctxt.lvl ctxt)) => existT ctxt e).
 
+    Definition singleton (ctxt : Ctxt.t) (entry : Entry.t (Ctxt.lvl ctxt)) : t :=
+      hset (Ctxt.lvl ctxt) {[(Ctxt.nd ctxt) := {[ entry ]}]} init.
+
+    #[global] Instance empty : Empty t := VATLB.init.
     #[global] Instance union : Union t := fun x y => hmap2 (fun _ => (∪ₘ)) x y.
   End VATLB.
 
   Record t :=
     make {
-        vatlb : VATLB.t
+        vatlb : VATLB.t;
       }.
 
   Definition init := make VATLB.init.
 
-  Definition read_sreg (tlb : t) (ts : TState.t) (time : view) (sreg : reg) :=
-    TState.read_sreg_at ts sreg time.
-
-
-
-  (* Program Definition va_fill_lvl0 (tlb : t) (ts : TState.t) *)
-  (*   (init : Memory.initial) *)
-  (*   (mem : Memory.t) (time : nat) : VATLB.t := *)
-  (*   tlb.(vatlb) ∪ *)
-  (*     fun ctxt => *)
-  (*       match ctxt.(Ctxt.lvl) with *)
-  (*       | 0%fin => *)
-  (*           match ctxt.(Ctxt.asid) return gset (Entry.t ctxt.(Ctxt.lvl)) with *)
-  (*           | Some asid => *)
-  (*               ( *)
-  (*                 let valttbrs := *)
-  (*                   (* read_sreg tlb ts time (Reg.TTBR0 0%fin) *) *)
-  (*                   (* |> List.filter (fun '(val,v) => bv_extract 48 16 val =? asid) *) *)
-  (*                   [] *)
-  (*                 in *)
-  (*                 valttbr ← valttbrs; *)
-  (*                 let root_addr := *)
-  (*                   bv_concat 64 (bv_0 16) (bv_extract 0 48 valttbr) in *)
-  (*                 root_loc ← Loc.from_va root_addr |> option_list; *)
-  (*                 let loc := next_entry_loc root_loc ctxt.(Ctxt.va) in *)
-  (*                 let '(val, _) := Memory.read_at loc init mem time in *)
-  (*                 [Vector.const val 1] *)
-  (*               ) *)
-  (*                |> list_to_set *)
-  (*           | None => ∅ *)
-  (*           end *)
-  (*       | _ => ∅ *)
-  (*       end. *)
-
-
-
-
-
-  (** WARNING HACK: Coq is shit so I'm forced to copy paste this function 3
-      times, because after 4 hours I didn't find a way to make it type a generic
-      version (among various internal crashes and similar errors). *)
-
-  (** Needed to do sensible match case on fin values *)
-  Definition fin_case {n : nat} (i : fin (S n)) : option (fin n) :=
-    match i with
-    | Fin.F1 => None
-    | FS n => Some n
-    end.
-
-  (* TODO report bug: Function is incompatible with Keyed Unification *)
-  #[local] Unset Keyed Unification.
-
-  Fixpoint fin_inj1 {n : nat} (p : fin n) : fin (S n) :=
-    match p with
-    | Fin.F1 => Fin.F1
-    | FS p' => FS (fin_inj1 p')
+  (** ** TLB filling *)
+
+  Definition is_active_asid (ts : TState.t)
+      (asid : option (bv 16))
+      (ttbr : reg) (time : nat) : Prop :=
+    match asid with
+    | Some asid =>
+      if TState.read_sreg_at ts ttbr time is Some sregs
+        then ∃ '(regval, view) ∈ sregs,
+              if (regval_to_val ttbr regval) is Some v
+                then asid = (bv_extract 48 16 v)
+                else False
+        else False
+    | None => True
     end.
-
-
-  Lemma fin_to_nat_fin_inj1 {n : nat} (p : fin n) : fin_inj1 p =@{nat} p.
-    Admitted.
-
-  (* Lemma va_fill_termination {n : nat} (i : fin (S n)) (j : fin n) : *)
-  (*   fin_case i = Some j -> (Fin.L 1 j < i)%nat. *)
-  (*   inv_fin i. *)
-
-  Set Printing Implicit.
-  Set Printing Coercions.
-
-  (* Function va_fill_lvl (tlb : t) (ts : TState.t) *)
-  (*   (init : Memory.initial) *)
-  (*   (mem : Memory.t) (time : nat) (lvl : Level) {measure fin_to_nat lvl } := *)
-  (*   match fin_case lvl return VATLB.t with *)
-  (*   | None => VATLB.init *)
-  (*   | Some n => *)
-  (*       va_fill_lvl tlb ts init mem time (fin_inj1 n) *)
-  (*   end *)
-  (*   ∪ tlb.(vatlb). *)
-  (* Proof. *)
-  (*   intros. *)
-  (*   inv_fin lvl. *)
-  (*   scongruence. *)
-  (*   cbn in *. *)
-  (*   intros. *)
-  (*   inversion teq as []. *)
-  (*   destruct H. *)
-  (*   rewrite fin_to_nat_fin_inj1. *)
-  (*   lia. *)
-  (* Qed. *)
-
-
-
-  (* Program Fixpoint va_fill_lvl (lvl : Level) {measure (fin_to_nat lvl) } := *)
-  (*   fun (tlb : t) (ts : TState.t) *)
-  (*   (init : Memory.initial) *)
-  (*   (mem : Memory.t) (time : nat) => *)
-  (*   match lvl return VATLB.t with *)
-  (*   | Fin.F1 => VATLB.init *)
-  (*   | FS n => va_fill_lvl (n : Level) tlb ts init mem time *)
-  (*   end. *)
-  (* Next Obligation. *)
-  (*   intros. *)
-  (* Admitted. *)
-  (* Next Obligation. *)
-  (* Admitted. *)
-  (* Next Obligation. *)
-  (* Admitted. *)
-
-  (* Print va_fill_lvl. *)
-
-
-  (* Definition va_fill (tlb : t) (ts : TState.t) (init : Memory.initial) *)
-  (*   (mem : Memory.t) (time : nat) : VATLB.t. *)
-  (* Admitted. *)
-
-
-  (** Get the TLB state at a certain timestamp *)
-  (* Definition get (ts : TState.t) (init : Memory.initial) (mem : Memory.t) *)
-  (*               (time : nat) : t. *)
+  Instance Decision_is_active_asid (ts : TState.t)
+      (asid : option (bv 16))
+      (ttbr : reg) (time : nat) : Decision (is_active_asid ts asid ttbr time).
+  Proof. unfold_decide. Defined.
+
+  Definition next_va {clvl : Level}
+    (ctxt : Ctxt.t)
+    (index : bv 9)
+    (CHILD : (Ctxt.lvl ctxt) + 1 = clvl) : prefix clvl :=
+    bv_concat (level_length clvl) (Ctxt.va ctxt) index.
+
+
+  (** Seed root-level TLB entries from [ttbr].
+      - Reads [ttbr] at [time], checks it is 64-bit.
+      - Computes root entry address for [va], reads memory.
+      - If entry is a table, builds a root context with ASID from TTBR
+        and inserts it into VATLB.
+      - Otherwise returns empty VATLB. *)
+  Definition va_fill_root (ts : TState.t)
+      (init : Memory.initial)
+      (mem : Memory.t)
+      (time : nat)
+      (va : prefix root_lvl)
+      (ttbr : reg) : result string VATLB.t :=
+    sregs ← othrow "TTBR should exist in initial state"
+              $ TState.read_sreg_at ts ttbr time;
+    vatlbs ←
+      for sreg in sregs do
+        val_ttbr ← othrow "TTBR should be a 64 bit value"
+                    $ regval_to_val ttbr sreg.1;
+        let entry_addr := next_entry_addr val_ttbr va in
+        let loc := Loc.from_addr_in entry_addr in
+        if (Memory.read_at loc init mem time) is Some (memval, _) then
+          guard_or "A root of a page table should be a table" (is_table memval);;
+          let asid := bv_extract 48 16 val_ttbr in
+          let ndctxt := NDCtxt.make va (Some asid) in
+          Ok $ VATLB.singleton (existT root_lvl ndctxt) [#memval]
+        else
+          Ok $ VATLB.init
+      end;
+    Ok (fold_left union vatlbs VATLB.init).
+
+  (** Extend one level down from a parent table entry [te].
+      - Requires [te] ∈ [vatlb] and ASID active for [ttbr].
+      - Reads next-level PTE at [index]; if valid and table, build child context
+        (ASID dropped if global) and insert into VATLB.
+      - Otherwise returns empty. *)
+  Definition va_fill_lvl (vatlb : VATLB.t) (ts : TState.t)
+      (init : Memory.initial)
+      (mem : Memory.t)
+      (time : nat)
+      (ctxt : Ctxt.t)
+      (te : Entry.t (Ctxt.lvl ctxt))
+      (index : bv 9)
+      (ttbr : reg) : result string VATLB.t :=
+    guard_or "ASID is not active"
+      $ is_active_asid ts (Ctxt.asid ctxt) ttbr time;;
+    guard_or "The translation entry is not in the TLB"
+      (te ∈ VATLB.get ctxt vatlb);;
+
+    if decide (¬is_table (Entry.pte te)) then Ok VATLB.init
+    else
+      let entry_addr := next_entry_addr (Entry.pte te) index in
+      let loc := Loc.from_addr_in entry_addr in
+      '(next_pte, _) ← othrow "The location of the next level address should be read"
+                        $ Memory.read_at loc init mem time;
+      if decide (is_valid next_pte) then
+        match inspect $ child_lvl (Ctxt.lvl ctxt) with
+        | Some clvl eq:e =>
+          let va := next_va ctxt index (child_lvl_add_one _ _ e) in
+          let asid := if bool_decide (is_global clvl next_pte) then None
+                      else Ctxt.asid ctxt in
+          let ndctxt := NDCtxt.make va asid in
+          let new_te := Entry.append te next_pte (child_lvl_add_one _ _ e) in
+          Ok $ VATLB.singleton (existT clvl ndctxt) new_te
+        | None eq:_ => mthrow "An intermediate level should have a child level"
+        end
+      else
+        Ok VATLB.init.
+
+  (** Make [tlb] containing entries for [va] at [lvl].
+      - At root: call [va_fill_root].
+      - At deeper levels: for each parent entry, call [va_fill_lvl].
+      - Returns [tlb] with added VATLB entries. *)
+  Definition va_fill (tlb : t) (ts : TState.t)
+      (init : Memory.initial)
+      (mem : Memory.t)
+      (time : nat)
+      (lvl : Level)
+      (va : bv 64)
+      (asid : option (bv 16))
+      (ttbr : reg) : result string t :=
+    vatlb ←
+      match parent_lvl lvl with
+      | None =>
+        vatlb_new ← va_fill_root ts init mem time (level_index va root_lvl) ttbr;
+        Ok $ vatlb_new ∪ tlb.(vatlb)
+      | Some plvl =>
+        let pva := level_prefix va plvl in
+        let ndctxt := NDCtxt.make pva asid in
+        let ctxt := existT plvl ndctxt in
+        let index := level_index va lvl in
+        vatlbs ←
+          for te in elements (VATLB.get ctxt tlb.(vatlb)) do
+            va_fill_lvl tlb.(vatlb) ts init mem time ctxt te index ttbr
+          end;
+        Ok $ (union_list vatlbs) ∪ tlb.(vatlb)
+      end;
+    Ok (TLB.make vatlb).
+
+  (** Fill TLB entries for [va] through all levels 0–3.
+      - Sequentially calls [va_fill] at each level.
+      - Produces a TLB with the full translation chain if available. *)
+  Definition update (tlb : t)
+      (ts : TState.t)
+      (init : Memory.initial)
+      (mem : Memory.t)
+      (time : nat)
+      (va : bv 64)
+      (asid : option (bv 16))
+      (ttbr : reg) : result string t :=
+    tlb0 ← va_fill tlb ts init mem time root_lvl va asid ttbr;
+    tlb1 ← va_fill tlb0 ts init mem time 1%fin va asid ttbr;
+    tlb2 ← va_fill tlb1 ts init mem time 2%fin va asid ttbr;
+    va_fill tlb2 ts init mem time 3%fin va asid ttbr.
 End TLB.
 
 Module VATLB := TLB.VATLB.
 
-
-
 (*** Instruction semantics ***)
 
 (** Intra instruction state for propagating views inside an instruction *)
@@ -959,7 +1064,7 @@ Definition read_mem_explicit (loc : Loc.t) (vaddr : view)
       if (fwd.(FwdItem.time) =? time) then read_fwd_view macc fwd else time
     else time in
   let vpost := vpre ⊔ read_view in
-  guard_discard (vpost <= invalidation_time)%nat;;
+  guard_discard (vpost ≤ invalidation_time)%nat;;
   mset fst $ TState.update_coh loc time;;
   mset fst $ TState.update TState.vrd vpost;;
   mset fst $ TState.update TState.vacq (view_if (is_rel_acq macc) vpost);;
@@ -1002,7 +1107,7 @@ Definition run_reg_write (reg : reg) (racc : reg_acc) (val : reg_type reg) :
     Exec.t (PPState.t TState.t Ev.t IIS.t) string unit :=
   guard_or
     "Cannot write to unknown register"
-    (reg_unknown reg);;
+    (is_reg_unknown reg);;
   guard_or
     "Non trivial write reg access types unsupported"
     (racc = None);;
@@ -1255,9 +1360,9 @@ Section RunOutcome.
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_cse
   | GenericFail s => mthrow ("Instruction failure: " ++ s)%string
   | _ => mthrow "Unsupported outcome".
+    (* TODO: translation - split lookup and update *)
 End RunOutcome.
 
-
 (** * Implement GenPromising ***)
 
 (** A thread is allowed to promise any promises with the correct tid for a