(* Lane mapping of BULK in pcie/rtl/bitacc_engine.sv.

   The bit store has L lanes; word w lives in lane (w mod L) at local address
   (w div L). BULK pairs dst word D + k with src word S + k for k = 0 .. n-1,
   L elements per step j. Per lane i the RTL computes, once per operation:

     r i   = (i - S) mod L          src element offset   (RTL: LW'(i) - S[LW-1:0])
     sa i  = (S + r i) div L        src local base       (RTL: sa)
     q m   = (m - D) mod L          dst element offset   (RTL: q_off)
     da m  = (D + q m) div L        dst local base       (RTL: da)
     delta = (D - S) mod L          rotation             (RTL: r_delta)

   In step j, lane i reads src local address j + sa i, which holds element
   k = j*L + r i; dst lane m reads and writes local address j + da m, holding
   element j*L + q m, and takes its src word from lane (m - delta) mod L.

   Proved here, for every L > 0 (the RTL uses L = 2^LW, where LW-bit
   subtraction is subtraction mod L, Part 1):
   - lane i's src read is word S + k of lane i (Part 2);
   - every element k >= 0 is read by exactly one lane, in step k div L (Part 2);
   - the rotation delivers element k to the lane and local address of word
     D + k, i.e. dst lane m and src lane (m - delta) mod L hold the same k
     (Part 3).
   Bounds (k < n, addresses inside the store) are checked by the RTL's kvalid
   and the decode-time range checks, and tested in pcie/tb. *)

module LaneMap
  use int.Int
  use int.EuclideanDivision

  constant l : int
  axiom l_pos : l > 0

  (* Each lemma is a lemma function whose assertions name the quotient
     witnesses, so that every step is linear arithmetic plus one instance of
     the standard library's Div_mod, Div_unique, Div_mult or Mod_mult. *)

  (* ---------------------------------------------------------------- Part 1: residues *)
  let lemma mod_add_multiple (a t : int)
    ensures { mod (a + t * l) l = mod a l }
  = assert { a + t * l = l * t + a }

  (* Linear step of rotation_pairs_elements, kept apart so that the prover
     sees it without the residue lemmas in its context. *)
  let lemma rotation_arith (m d s t e : int)
    requires { d - s = l * t + e }
    ensures { m - e + (- s) = (m - d) + t * l }
  = ()

  let lemma rotation_mod (m d s t e : int)
    requires { d - s = l * t + e }
    ensures { mod (m - e + (- s)) l = mod (m - d) l }
  = rotation_arith m d s t e;
    mod_add_multiple (m - d) t

  let lemma div_add_multiple (a t : int)
    ensures { div (a + t * l) l = div a l + t }
  = assert { a + t * l = l * t + a }

  let lemma mod_small (a : int)
    requires { 0 <= a < l }
    ensures { mod a l = a }
  = assert { div a l = 0 };
    assert { a = l * div a l + mod a l }

  let lemma mod_sum_left (a b : int)
    ensures { mod (mod a l + b) l = mod (a + b) l }
  = assert { a = l * div a l + mod a l };
    assert { a + b = (mod a l + b) + div a l * l };
    mod_add_multiple (mod a l + b) (div a l)

  let lemma mod_sum_right (a b : int)
    ensures { mod (a + mod b l) l = mod (a + b) l }
  = mod_sum_left b a;
    assert { mod b l + a = a + mod b l /\ b + a = a + b }

  (* LW-bit subtraction of residues (the RTL's r, q_off, r_delta) is the
     residue of the difference when L = 2^LW. *)
  let lemma mod_sub_residues (a b : int)
    ensures { mod (mod a l - mod b l) l = mod (a - b) l }
  = assert { a = l * div a l + mod a l };
    assert { b = l * div b l + mod b l };
    assert { a - b = (mod a l - mod b l) + (div a l - div b l) * l };
    mod_add_multiple (mod a l - mod b l) (div a l - div b l)

  (* ---------------------------------------------------------------- Part 2: src side *)
  function r (s i : int) : int = mod (i - s) l
  function sa (s i : int) : int = div (s + r s i) l
  function k_src (s i j : int) : int = j * l + r s i

  lemma r_bounds : forall s i : int. 0 <= r s i < l

  (* Lane i's element of step j lives in lane i ... *)
  let lemma src_lane (s i j : int)
    requires { 0 <= i < l }
    ensures { mod (s + k_src s i j) l = i }
  = assert { i - s = l * div (i - s) l + r s i };
    assert { s + k_src s i j = i + (j - div (i - s) l) * l };
    mod_add_multiple i (j - div (i - s) l);
    mod_small i

  (* ... at local address j + sa i. *)
  let lemma src_local (s i j : int)
    ensures { div (s + k_src s i j) l = j + sa s i }
  = assert { s + k_src s i j = (s + r s i) + j * l };
    div_add_multiple (s + r s i) j

  (* Every element k is the element of lane (s + k) mod L in step k div L ... *)
  let lemma src_covers (s k : int)
    ensures { k_src s (mod (s + k) l) (div k l) = k }
  = mod_sum_left (s + k) (- s);
    assert { s + k + (- s) = k };
    assert { k = l * div k l + mod k l }

  (* ... and of no other lane in that step. *)
  let lemma src_unique (s i1 i2 j : int)
    requires { 0 <= i1 < l /\ 0 <= i2 < l }
    requires { k_src s i1 j = k_src s i2 j }
    ensures { i1 = i2 }
  = src_lane s i1 j;
    src_lane s i2 j

  (* The element of step j is in [j L, j L + L): different steps hold
     different elements. *)
  let lemma src_step (s i j : int)
    ensures { div (k_src s i j) l = j }
  = assert { j * l <= k_src s i j < j * l + l }

  let lemma src_steps_disjoint (s i1 i2 j1 j2 : int)
    requires { k_src s i1 j1 = k_src s i2 j2 }
    ensures { j1 = j2 }
  = src_step s i1 j1;
    src_step s i2 j2

  (* ---------------------------------------------------------------- Part 3: dst side, rotation *)
  (* The dst offsets have the same form as the src offsets, with d for s. *)
  function q (d m : int) : int = r d m
  function da (d m : int) : int = sa d m
  function k_dst (d m j : int) : int = k_src d m j
  function delta (d s : int) : int = mod (d - s) l
  function src_lane_for (d s m : int) : int = mod (m - delta d s) l

  (* Dst lane m's element of step j is word d + k of lane m, at j + da m. *)
  let lemma dst_lane (d m j : int)
    requires { 0 <= m < l }
    ensures { mod (d + k_dst d m j) l = m }
  = src_lane d m j

  let lemma dst_local (d m j : int)
    ensures { div (d + k_dst d m j) l = j + da d m }
  = src_local d m j

  (* The src lane the rotation selects is a lane ... *)
  lemma rotation_in_range :
    forall d s m : int. 0 <= src_lane_for d s m < l

  (* ... and it holds the same element k as dst lane m, in every step. *)
  let lemma rotation_pairs_elements (d s m j : int)
    ensures { k_src s (src_lane_for d s m) j = k_dst d m j }
  = let t = div (d - s) l in
    let e = delta d s in
    assert { r s (src_lane_for d s m) = mod (mod (m - e) l + (- s)) l };
    mod_sum_left (m - e) (- s);
    assert { r s (src_lane_for d s m) = mod (m - e + (- s)) l };
    assert { d - s = l * t + e };
    rotation_mod m d s t e

  (* Element k from src lane i goes to dst lane (i + delta) mod L. *)
  let lemma rotation_target (d s i j : int)
    requires { 0 <= i < l }
    ensures { mod (d + k_src s i j) l = mod (i + delta d s) l }
  = assert { i - s = l * div (i - s) l + r s i };
    assert { d + k_src s i j = (i + (d - s)) + (j - div (i - s) l) * l };
    mod_add_multiple (i + (d - s)) (j - div (i - s) l);
    mod_sum_right i (d - s)
end