val lemma_equal_intro (regs1:t) (regs2:t) : Lemma
  (requires forall (r:reg). sel r regs1 == sel r regs2)
  (ensures equal regs1 regs2)
  [SMTPat (equal regs1 regs2)]
let lemma_equal_intro m1 m2 =
  reveal_opaque (`%t) t;
  reveal_opaque (`%Vale.Lib.Map16.sel) (Vale.Lib.Map16.sel #nat64);
  reveal_opaque (`%Vale.Lib.Map16.sel) (Vale.Lib.Map16.sel #quad32);
  reveal_opaque (`%sel) sel;
  reveal_opaque (`%upd) upd;
  let (m1_0, m1_1) = m1 in
  let (m2_0, m2_1) = m2 in
  assert (forall (i:nat). i < 16 ==> sel (Reg 0 i) m1 == sel (Reg 0 i) m2);
  assert (forall (i:nat). i < 16 ==> sel (Reg 1 i) m1 == sel (Reg 1 i) m2);
  Vale.Lib.Map16.lemma_equal m1_0 m2_0;
  Vale.Lib.Map16.lemma_equal m1_1 m2_1;
  ()
val lemma_equal_intro (regs1:t) (regs2:t) : Lemma
  (requires forall (r:reg). sel r regs1 == sel r regs2)
  (ensures equal regs1 regs2)
  [SMTPat (equal regs1 regs2)]
let lemma_equal_intro m1 m2 =
reveal_opaque (`%t) t;
reveal_opaque (`%Vale.Lib.Map16.sel) (Vale.Lib.Map16.sel #nat64);
reveal_opaque (`%Vale.Lib.Map16.sel) (Vale.Lib.Map16.sel #quad32);
reveal_opaque (`%sel) sel;
reveal_opaque (`%upd) upd;
let m1_0, m1_1 = m1 in
let m2_0, m2_1 = m2 in
assert (forall (i: nat). i < 16 ==> sel (Reg 0 i) m1 == sel (Reg 0 i) m2);
assert (forall (i: nat). i < 16 ==> sel (Reg 1 i) m1 == sel (Reg 1 i) m2);
Vale.Lib.Map16.lemma_equal m1_0 m2_0;
Vale.Lib.Map16.lemma_equal m1_1 m2_1;
()
Vale.X64.Regs.fst.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Map16.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.Regs.fst
Vale.X64.Regs.t Vale.Lib.Map16.map16 Vale.X64.Machine_s.nat64 Vale.X64.Machine_s.quad32 Prims.unit Vale.Lib.Map16.lemma_equal Prims._assert Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Prims.eq2 Vale.X64.Machine_s.t_reg Vale.X64.Machine_s.Reg Vale.X64.Regs.sel FStar.Pervasives.reveal_opaque Vale.X64.Machine_s.reg Vale.X64.Regs.upd Prims.int Vale.Lib.Map16.sel
module Vale.X64.Regs
open FStar.Mul
open Vale.X64.Machine_s

let of_fun m =
  reveal_opaque (`%sel) sel;
//  FStar.FunctionalExtensionality.on_dom reg m
  let m0_3 = ((m (Reg 0 0), m (Reg 0 1)), (m (Reg 0 2), m (Reg 0 3))) in
  let m4_7 = ((m (Reg 0 4), m (Reg 0 5)), (m (Reg 0 6), m (Reg 0 7))) in
  let m8_11 = ((m (Reg 0 8), m (Reg 0 9)), (m (Reg 0 10), m (Reg 0 11))) in
  let m12_15 = ((m (Reg 0 12), m (Reg 0 13)), (m (Reg 0 14), m (Reg 0 15))) in
  let m0 = ((m0_3, m4_7), (m8_11, m12_15)) in
  let m0_3 = ((m (Reg 1 0), m (Reg 1 1)), (m (Reg 1 2), m (Reg 1 3))) in
  let m4_7 = ((m (Reg 1 4), m (Reg 1 5)), (m (Reg 1 6), m (Reg 1 7))) in
  let m8_11 = ((m (Reg 1 8), m (Reg 1 9)), (m (Reg 1 10), m (Reg 1 11))) in
  let m12_15 = ((m (Reg 1 12), m (Reg 1 13)), (m (Reg 1 14), m (Reg 1 15))) in
  let m1 = ((m0_3, m4_7), (m8_11, m12_15)) in
  (m0, m1)
(*
  let m0_3 = ((m rRax, m rRbx), (m rRcx, m rRdx)) in
  let m4_7 = ((m rRsi, m rRdi), (m rRbp, m rRsp)) in
  let m8_11 = ((m rR8, m rR9), (m rR10, m rR11)) in
  let m12_15 = ((m rR12, m rR13), (m rR14, m rR15)) in
  let m' = ((m0_3, m4_7), (m8_11, m12_15)) in
  assert_norm (m rRax == sel rRax m');
  assert_norm (m rRbx == sel rRbx m');
  assert_norm (m rRcx == sel rRcx m');
  assert_norm (m rRdx == sel rRdx m');
  assert_norm (m rRsi == sel rRsi m');
  assert_norm (m rRdi == sel rRdi m');
  assert_norm (m rRbp == sel rRbp m');
  assert_norm (m rRsp == sel rRsp m');
  assert_norm (m rR8  == sel rR8  m');
  assert_norm (m rR9  == sel rR9  m');
  assert_norm (m rR10 == sel rR10 m');
  assert_norm (m rR11 == sel rR11 m');
  assert_norm (m rR12 == sel rR12 m');
  assert_norm (m rR13 == sel rR13 m');
  assert_norm (m rR14 == sel rR14 m');
  assert_norm (m rR15 == sel rR15 m');
  m'
*)

let lemma_upd_eq r v m =
  assert_norm (sel r (upd r v m) == v)

let lemma_upd_ne r r' v m =
  assert_norm (sel r (upd r' v m) == sel r m)

let equal m1 m2 = m1 == m2
val lemma_equal_intro (regs1:t) (regs2:t) : Lemma
  (requires forall (r:reg). sel r regs1 == sel r regs2)
  (ensures equal regs1 regs2)
  [SMTPat (equal regs1 regs2)]
regs1: Vale.X64.Regs.t -> regs2: Vale.X64.Regs.t
  -> FStar.Pervasives.Lemma
      (requires
        forall (r: Vale.X64.Machine_s.reg). Vale.X64.Regs.sel r regs1 == Vale.X64.Regs.sel r regs2)
      (ensures Vale.X64.Regs.equal regs1 regs2)
      [SMTPat (Vale.X64.Regs.equal regs1 regs2)]