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 ptr p ⇒
    match ptype ptr with
    [ Code ⇒ Error … [MSG UnsupportedOp]
    | XData ⇒
      match p with
      [ O ⇒
        ! carry' ← Bit_of_val UnsupportedOp carry ;
        if carry' then Error … [MSG UnsupportedOp]
        else
          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
          let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
          return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉
      | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *)
        match carry with
        [ BBptrcarry is_add' ptr' p' by' ⇒
          if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
          then If eqb p' 0 then with prf do
            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
            let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in
            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
            let part1 ≝ mk_part 1 (le_n …) in
            let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
            OK … 〈BVptr ptr' part1,
                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
          else Error … [MSG UnsupportedOp]
          else Error … [MSG UnsupportedOp]
        | _ ⇒ Error … [MSG UnsupportedOp]
        ]
      ]
    ]
  | _ ⇒ Error … [MSG UnsupportedOp]
  ].
@hide_prf
lapply prf @(eqb_elim p') #H * >H %
qed.

definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝
λn,v,p,H.
let suffix : BitVector (8 + 8*p) ≝
  \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in
\fst (vsplit … suffix).
>(commutative_times_fast ? p)
change with (? = BitVector (? + S p*8))
>(commutative_times_fast (S p))
<distributive_times_plus_fast
<(plus_minus_m_m … H) %
qed.

definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝
λA,eq,m,n.
match m with
[ Some a ⇒
  match n with
  [ Some b ⇒ eq a b
  | _ ⇒ false
  ]
| _ ⇒
  match m with
  [ None ⇒ true
  | _ ⇒ false
  ]
].

(* 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.
   Neither BVundef nor BVpc allow any operations
  arg2\arg1 | BVByte    | BVptr (D)      | BVptr (C) | BVnull | BVXor | BVnonzero |
  ----------+-----------+----------------+-----------+--------+-------+-----------+
  BVByte    | all       | Add, Addc, Sub | --        | --     | --    | Or        |
  ----------+-----------+----------------+-----------+--------+-------+-----------+
  BVptr (D) | Add, Addc | Sub, Xor       | Xor       | Xor    | --    | --        |
  ----------+-----------+----------------+-----------+--------+-------+-----------+
  BVptr (C) | --        | Xor            | Xor       | Xor    | --    | --        |
  ----------+-----------+----------------+-----------+--------+-------+-----------+
  BVnull    | --        | Xor            | Xor       | Xor    | --    | --        |
  ----------+-----------+----------------+-----------+--------+-------+-----------+
  BVXor     | --        | --             | --        | --     | Or    | Or        |
  ----------+-----------+----------------+-----------+--------+-------+-----------+
  BVnonzero | Or        | --             | --        | --     | Or    | --        |
  ----------+-----------+----------------+-----------+--------+-------+-----------+
*)
definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
  λcarry,op,a1,a2.
  match a1 with
  [ BVByte b1 ⇒
(*    if match op with [ Or ⇒ true | _ ⇒ false ] ∧ eq_bv … (zero …) b1 then
      return 〈a2, carry〉
    else *) (* maybe it will be needed, need to see actual translations *)
      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 _ _ ⇒
        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 ptr1 p1 ⇒
    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 ptr2 p2 ⇒
      match op with
      [ Sub ⇒
        match ptype ptr1 with
        [ Code ⇒ Error … [MSG UnsupportedOp]
        | XData ⇒
          if eq_block (pblock ptr1) (pblock ptr2) ∧
             eqb p1 p2
          then
          ! carry ← Bit_of_val UnsupportedOp carry ;
            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
            return 〈BVByte result, BBbit carry〉
          else Error … [MSG UnsupportedOp]
        ]
      | Xor ⇒
        if eqb p1 p2 then
          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
        else Error … [MSG UnsupportedOp]
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | BVnull p2 ⇒
      match op with
      [ Xor ⇒
        if eqb p1 p2 then
          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
        else
          Error … [MSG UnsupportedOp]
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | _ ⇒ Error … [MSG UnsupportedOp]
    ]
  | BVnull p1 ⇒
    match op with
    [ Xor ⇒
      match a2 with
      [ BVptr ptr2 p2 ⇒
        if eqb p1 p2 then
          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
        else
          Error … [MSG UnsupportedOp]
      | BVnull p2 ⇒
        if eqb p1 p2 then
          return 〈BVXor (None ?) (None ?) p1, carry〉
        else
          Error … [MSG UnsupportedOp]
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | _ ⇒ Error … [MSG UnsupportedOp]
    ]
  | BVXor ptr1_opt ptr1_opt' p1 ⇒
    match op with
    [ Or ⇒
      match a2 with
      [ BVByte b2 ⇒
        if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
        else Error … [MSG UnsupportedOp]
      | BVnonzero ⇒ return 〈BVnonzero, carry〉
      | BVXor ptr2_opt ptr2_opt' p2 ⇒
        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
          let eq_at ≝ λp,ptr1,ptr2.
            eq_block (pblock ptr1) (pblock ptr2) ∧
            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
          then return 〈BVByte (bv_zero …), carry〉
          else 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〉
      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
      | _ ⇒ Error … [MSG UnsupportedOp]
      ]
    | _ ⇒ Error … [MSG UnsupportedOp]
    ]
  | _ ⇒ Error … [MSG UnsupportedOp]
  ].