include "common/ByteValues.ma".

(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
        not further back in the translation chain.                            *)
inductive OpAccs: Type[0] ≝
  Mul: OpAccs
| DivuModu: OpAccs.

inductive Op1: Type[0] ≝
  Cmpl: Op1
| Inc: Op1
| Rl: Op1. (* TODO: implement left rotation *)

inductive Op2: Type[0] ≝
  Add: Op2
| Addc: Op2
| Sub: Op2
| And: Op2
| Or: Op2
| Xor: Op2.

record Eval : Type[0] ≝
{
  opaccs: OpAccs → Byte → Byte → Byte × Byte;
  op1: Op1 → Byte → Byte;
  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
}.

axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
axiom op1_implementation: Op1 → Byte → Byte.
axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).

definition eval : Eval ≝
  mk_Eval opaccs_implementation
          op1_implementation
          op2_implementation.

axiom UnsupportedOp : String.

definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝
  λop,a,b.
  ! a' ← Byte_of_val UnsupportedOp a ;
  ! b' ← Byte_of_val UnsupportedOp b ;
  let 〈a'',b''〉 ≝ opaccs eval op a' b' in
  return 〈BVByte a'', BVByte b''〉.

definition be_op1 : Op1 → beval → res beval ≝
  λop,a.
  ! a' ← Byte_of_val UnsupportedOp a ;
  return BVByte (op1 eval op a').

definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝
λop,n,carry.
  let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit.
    let 〈res_tl, carry〉 ≝ pr in
    let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in
    〈res_hd ::: res_tl, carry'〉 in
  fold_right2_i … f 〈[[ ]],carry〉 n.

definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝
  λis_add,carry,a1,b2.
  let op ≝ if is_add then Addc else Sub in
  match a1 with
  [ BVByte b1 ⇒
    ! carry' ← Bit_of_val UnsupportedOp carry ;
    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
    return 〈BVByte rslt, BBbit carry''〉
  | BVptr b p o ⇒
    match p with
    [ O ⇒ λ_:0<size_pointer.λo : Vector Byte 1.
      if eq_bebit carry (BBbit false) then
        let o' ≝ from_singl … o in
        let 〈rslt,carry〉 ≝ op2 eval false op b2 o' in
        let p' : part ≝ mk_part 0 ? in
        return 〈BVptr b p' [[rslt]], BBptrcarry is_add b p' o [[b2]]〉
      else
        Error … [MSG UnsupportedOp]
    | S k ⇒ λSk_ok:S k<size_pointer.λo : Vector Byte (S (S k)).
      match carry with
      [ BBptrcarry is_add' b' p' o' by' ⇒
        if eq_b is_add is_add' ∧ eq_block b b' ∧ vsuffix … (eq_bv 8) o' o then
          If eqb k p' then with prf do
            let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in
            let 〈rslt,ignore〉 ≝ op2_bytes op … false o (b2 ::: by') in
            let Sk_part ≝ mk_part (S k) Sk_ok in
            OK … 〈BVptr b Sk_part rslt,
                     BBptrcarry is_add b Sk_part o (b2 ::: by')〉
          else Error … [MSG UnsupportedOp]
        else Error … [MSG UnsupportedOp]
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    ] (part_no_ok p) o
  | _ ⇒ Error … [MSG UnsupportedOp]
  ].
@hide_prf [//]
lapply prf @(eqb_elim k) #H * >H %
qed.

(* This tables shows what binary ops may be defined on bevals depending on
   the arguments (columns marked by 1st argument, rows by 2nd). Further
   checks for definedness are done for pointer parts taking into account
   blocks, parts and the carry value.
            | BVByte    | BVptr          | BVnull | BVnonzero | BVundef |
  ----------+-----------+----------------+--------+-----------+---------|
  BVByte    | all       | Add, Addc, Sub | none   | Or        | none    |
  ----------+-----------+----------------+--------+-----------+---------|
  BVptr     | Add, Addc | Sub, Xor       | Xor    | none      | none    |
  ----------+-----------+----------------+--------+-----------+---------|
  BVnull    | none      | Xor            | Xor    | none      | none    |
  ----------+-----------+----------------+--------+-----------+---------|
  BVnonzero | Or        | none           | none   | Or        | none    |
  ----------+-----------+----------------+--------+-----------+---------|
  BVundef   | none      | none           | none   | none      | none    |
  ----------------------------------------------------------------------+
*)
definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
  λcarry,op,a1,a2.
  match a1 with
  [ BVByte b1 ⇒
    match a2 with
    [ BVByte b2 ⇒
      ! carry ← Bit_of_val UnsupportedOp carry ;
      let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
      return 〈BVByte result, BBbit carry〉
    | BVptr bl2 p2 o2 ⇒
      match op with
      [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
      | Addc ⇒ be_add_sub_byte true carry a2 b1
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | BVnonzero ⇒
      match op with
      [ Or ⇒ return 〈BVnonzero, carry〉
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | _ ⇒ Error … [MSG UnsupportedOp]
    ]
  | BVptr bl1 p1 o1 ⇒
    match a2 with
    [ BVByte b2 ⇒
      match op with
      [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2
      | Addc ⇒ be_add_sub_byte true carry a1 b2
      | Sub ⇒ be_add_sub_byte false carry a1 b2
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | BVptr bl2 p2 o2 ⇒
      match op with
      [ Sub ⇒
        if eq_block bl1 bl2 ∧ eqb p1 p2 then
          ! carry ← Bit_of_val UnsupportedOp carry ;
          let by1 ≝ head' … o1 in
          let by2 ≝ head' … o2 in
          let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
          return 〈BVByte result, BBbit carry〉
        else Error … [MSG UnsupportedOp]
      | Xor ⇒
        if eq_block bl1 bl2 ∧ eqb p1 p2 then
          if vprefix … (eq_bv 8) o1 o2 (* equivalent to equality *) then
            return 〈BVByte (bv_zero …), carry〉
          else
            return 〈BVnonzero, carry〉
        else Error … [MSG UnsupportedOp]
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | BVnull p2 ⇒
      match op with
      [ Xor ⇒
        if eqb p1 p2 then
          return 〈BVnonzero, carry〉
        else
          Error … [MSG UnsupportedOp]
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | _ ⇒ Error … [MSG UnsupportedOp]
    ]
  | BVnonzero ⇒
    match op with
    [ Or ⇒
      match a2 with
      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
      | BVnonzero ⇒ return 〈BVnonzero, carry〉
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | _ ⇒ Error … [MSG UnsupportedOp]
    ]
  | BVnull p1 ⇒
    match op with
    [ Xor ⇒
      match a2 with
      [ BVptr _ p2 _ ⇒
        if eqb p1 p2 then
          return 〈BVnonzero, carry〉
        else
          Error … [MSG UnsupportedOp]
      | BVnull p2 ⇒
        if eqb p1 p2 then
          return 〈BVByte (bv_zero …), carry〉
        else
          Error … [MSG UnsupportedOp]
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | _ ⇒ Error … [MSG UnsupportedOp]
    ]
  | _ ⇒ Error … [MSG UnsupportedOp]
  ].