icfpc2013.v

Require Import
        Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype
        Ssreflect.ssrnat Ssreflect.seq
        Coq.Logic.JMeq Coq.Bool.Bvector Coq.PArith.BinPosDef Coq.NArith.BinNat.

Set Implicit Arguments.

Axiom (PrintAxiom : forall (T : Type), T -> Prop).

Theorem minn_idPr' m n : n <= m -> minn m n = n.
Proof.
  rewrite /minn => H.
  have: m < n = false.
    elim: n m H => //= n IH [| m] //=.
    move: IH.
    rewrite /leq /subn /subn_rec /=.
    apply.
  by clear => ->.
Defined.

Theorem addKn' n : cancel (addn n) (subn^~ n).
Proof.
  rewrite /cancel /addn /addn_rec /subn /subn_rec.
  move => m; elim: n => //=.
  elim: m => //=.
Defined.

Theorem subSS' n m : m.+1 - n.+1 = m - n.
Proof.
  by rewrite /subn /subn_rec /=.
Defined.

Theorem minnSS' m n : minn m.+1 n.+1 = (minn m n).+1.
Proof.
  rewrite /minn /leq /subn /subn_rec /=.
  case: n => // n.
  by case: (m - n)%coq_nat.
Defined.

Theorem min0n' : left_zero 0 minn.
Proof.
  by rewrite /left_zero /minn; case.
Defined.

Theorem leq_addr' m n : n <= n + m.
Proof.
  rewrite /leq /addn /addn_rec /subn /subn_rec.
  by elim: n.
Defined.

Section EqVec.

Variable (T : eqType).

Fixpoint eqvec n : Vector.t T n -> Vector.t T n -> bool :=
  match n with
    | 0 => fun _ _ => true
    | n.+1 => fun v1 v2 =>
      (Vector.hd v1 == Vector.hd v2) && eqvec (Vector.tl v1) (Vector.tl v2)
  end.

Lemma eqvecP : forall n, Equality.axiom (@eqvec n).
Proof.
  rewrite /Equality.axiom; apply Vector.rect2 => /=.
  - by constructor.
  - move => n v1 v2; case => H a b.
    - case: (a =P b).
      - by rewrite H /= => ->; constructor.
      - by move => H0 /=; constructor => [[H1 _]].
    - rewrite andbC /=; constructor => H0.
      by apply H; case: (Vector.cons_inj _ _ _ _ _ _ H0).
Defined.

Canonical vec_eqMixin n := EqMixin (@eqvecP n).
Canonical vec_eqType n := Eval hnf in EqType (Vector.t T n) (vec_eqMixin n).

End EqVec.

Fixpoint vec_split (T : Type) (n m : nat) :
  Vector.t T n -> Vector.t T (minn n m) * Vector.t T (n - m) :=
  match n as n0 return
        Vector.t T n0 -> Vector.t T (minn n0 m) * Vector.t T (n0 - m) with
    | 0 => fun _ => (eq_rect_r (Vector.t T) [] (min0n' m), [])
    | n0.+1 =>
      match m as m0 return
            Vector.t T n0.+1 ->
            Vector.t T (minn n0.+1 m0) * Vector.t T (n0.+1 - m0) with
        | 0 => pair []
        | m0.+1 =>
          fun (v : Vector.t T n0.+1) =>
            match v as v0 in (Vector.t _ n1) return
                  n1 = n0.+1 ->
                  Vector.t T (minn n0.+1 m0.+1) *
                  Vector.t T (n0.+1 - m0.+1) with
              | [] =>
                fun (Heq : 0 = n0.+1) =>
                  False_rect
                    (Vector.t T (minn n0.+1 m0.+1) * Vector.t T (n0.+1 - m0.+1))
                    (O_S n0 Heq)
              | Vector.cons h wildcard' v0 =>
                fun (Heq : wildcard'.+1 = n0.+1) =>
                  let (r1, r2) := vec_split m0 v0 in
                  (eq_rect
                     (minn wildcard' m0).+1 (Vector.t T)
                     (h :: r1) (minn n0.+1 m0.+1)
                     (eq_trans (Logic.eq_sym (minnSS' wildcard' m0))
                               (f_equal (minn^~ m0.+1) Heq)),
                   eq_rect
                     (wildcard' - m0) (Vector.t T) r2 (n0.+1 - m0.+1)
                     (eq_trans (Logic.eq_sym (subSS' m0 wildcard'))
                               (f_equal (subn^~ m0.+1) Heq)))
            end (erefl n0.+1)
      end
  end.

(*
Program Fixpoint vec_split (T : Type) (n m : nat) :
  Vector.t T n -> Vector.t T (minn n m) * Vector.t T (n - m) :=
  match n with
    | 0 => fun _ => ([], [])
    | n.+1 =>
      match m with
        | 0 => fun v => ([], v)
        | m.+1 =>
          fun v => match v with
            | [] => ([], [])
            | h :: v => let (r1, r2) := vec_split m v in (h :: r1, r2)
          end
      end
  end.
Next Obligation.
  by rewrite min0n.
Defined.
Next Obligation.
  by rewrite minnSS.
Defined.
*)

Fixpoint vec_break (T : Type) (n m e : nat) :
  Vector.t T n -> n = m * e -> Vector.t (Vector.t T e) m :=
  match m as m0
        return (Vector.t T n -> n = m0 * e -> Vector.t (Vector.t T e) m0) with
    | 0 => fun _ _ => []
    | m0.+1 =>
      fun (v : Vector.t T n) (H : n = m0.+1 * e) =>
        let (vh, vt) := vec_split e v in
        eq_rect
          (minn n e) (Vector.t T) vh e
          (eq_trans (f_equal (minn^~ e) H)
                    (minn_idPr' _ _ (leq_addr' (m0 * e) e)))
          ::
          vec_break m0 e vt
          (eq_trans
             (f_equal (subn^~ e) H)
             (eq_trans (erefl (m0.+1 * e - e)) (addKn' e (m0 * e))))
  end.

(*
Program Fixpoint vec_break (T : Type) (n m e : nat) :
  Vector.t T n -> n = m * e -> Vector.t (Vector.t T e) m :=
  match m with
    | 0 => fun _ _ => []
    | m.+1 =>
      fun v H =>
        let (vh, vt) := vec_split e v in
        _ :: @vec_break T (n - e) m e vt _
  end.
Next Obligation.  
  move: vh.
  by rewrite mulSn -{3}(addn0 e) -addn_minr minn0 addn0.
Defined.
Next Obligation.
  by rewrite mulSn addKn.
Defined.
*)

Definition N_of_bvec : forall {n}, Bvector n -> N :=
  Vector.t_rect
     bool (fun _ _ => N) N0
     (fun b _ _ r => if b then N.succ_double r else N.double r).

Fixpoint bvec_of_positive n (p : positive) {struct p} : Bvector n :=
  match n with
    | 0 => []
    | n.+1 =>
      match p with
        | p~1 => true :: bvec_of_positive n p
        | p~0 => false :: bvec_of_positive n p
        | 1 => true :: Bvect_false n
      end%positive
  end.

Definition bvec_of_N n (m : N) : Bvector n :=
  match m with
    | N0 => Bvect_false n
    | Npos p => bvec_of_positive n p
  end.

(* language definition of \BV *)

Inductive op_arity1 := opnot | opshl1 | opshr1 | opshr4 | opshr16.

Inductive op_arity2 := opand | opor | opxor | opplus.

Inductive expr :=
  | ezero
  | eone
  | evar of nat
  | eif0 of expr & expr & expr
  | efold of expr & expr & expr
  | eop1 of op_arity1 & expr
  | eop2 of op_arity2 & expr & expr.

Fixpoint sizeof (e : expr) : nat :=
  match e with
    | eif0 e0 e1 e2 => (sizeof e0 + sizeof e1 + sizeof e2).+1
    | efold e0 e1 e2 => (sizeof e0 + sizeof e1 + sizeof e2).+2
    | eop1 _ e => (sizeof e).+1
    | eop2 _ e0 e1 => (sizeof e0 + sizeof e1).+1
    | _ => 1
  end.

Section BVlang_Eval.

Variable bytes : nat. (* bytes - 1 *)
Definition bits := bytes.+1 * 8.
Definition value := Bvector bits.

Definition zeroval : value := Bvect_false bits.

Definition oneval : value := true :: Bvect_false bits.-1.

Definition eval_op1 (op : op_arity1) (v : value) : value :=
  match op with
    | opnot => Vector.map negb v
    | opshl1 => BshiftL _ v false
    | opshr1 => BshiftRl _ v false
    | opshr4 => BshiftRl_iter _ v 4
    | opshr16 => BshiftRl_iter _ v 16
  end.

Definition eval_op2 (op : op_arity2) (v0 v1 : value) : value :=
  match op with
    | opand => Vector.map2 andb v0 v1
    | opor => Vector.map2 orb v0 v1
    | opxor => Vector.map2 xorb v0 v1
    | opplus =>
      snd (Vector.rect2
             (fun n _ _ => (bool * Bvector n)%type) (false, [])
             (fun n _ _ r a b =>
                (fst r && (a || b) || a && b, fst r (+) a (+) b :: snd r))
             v0 v1)
  end.

Fixpoint eval (ctx : seq value) (e : expr) : option value :=
  let value_of_byte (v : Bvector 8) : value :=
      Vector.append v (Bvect_false (bytes * 8)) in
  match e with
    | ezero => Some zeroval
    | eone => Some oneval
    | evar n => nth None (map some ctx) n
    | eif0 e0 e1 e2 =>
      obind
        (fun v1 => if v1 == zeroval then eval ctx e1 else eval ctx e2)
        (eval ctx e0)
    | efold e0 e1 e2 =>
      obind
        (fun v0 =>
           obind
             (fun v1 =>
                Vector.fold_left
                  (fun v1 v2 =>
                     obind
                       (fun v1' => eval [:: value_of_byte v2, v1' & ctx] e2)
                       v1)
                  (some v1)
                  (vec_break bytes.+1 8 v0 erefl))
             (eval ctx e1))
        (eval ctx e0)
    | eop1 op e =>
      omap (fun v => eval_op1 op v) (eval ctx e)
    | eop2 op e0 e1 =>
      obind
        (fun v1 =>
           omap (fun v0 => eval_op2 op v0 v1) (eval ctx e0))
        (eval ctx e1)
  end.

End BVlang_Eval.

(* constant value expression generator *)

Fixpoint expr_of_positive (p : positive) : expr :=
  match p with
    | p~1 => eop2 opor eone (eop1 opshl1 (expr_of_positive p))
    | p~0 => eop1 opshl1 (expr_of_positive p)
    | 1 => eone
  end%positive.

Definition expr_of_N (n : N) : expr :=
  match n with
    | N0 => ezero
    | Npos p => expr_of_positive p
  end.

Lemma expr_of_N_valid bytes ctx n :
  eval ctx (expr_of_N n) = Some (bvec_of_N (bits bytes) n).
Proof.
  case: n; rewrite /bvec_of_N.
  - by rewrite /= /zeroval.
  - elim => // p; rewrite /expr_of_N.
    - rewrite [expr_of_positive p~1]/= [bvec_of_positive _ p~1]/=.
      rewrite (lock eone) /= => ->.
      rewrite /= -(lock eone)
              -/mult -/muln_rec -/muln /eval /omap /obind /oapp.
      f_equal.
      rewrite /oneval /bits /muln /muln_rec
              [mult _ _]/= [_.-1]/= -/muln_rec -/muln.
      move: (bytes * 8).+3.+4 => /= n.
      f_equal.
      rewrite /Bvect_false.
Abort.

(* test codes *)

Eval vm_compute in (* shl8 *)
    (@eval 7 [:: bvec_of_N _ 255%N]
      (efold ezero (evar 0) (eop1 opshl1 (evar 1)))).

Eval vm_compute in (* bytewise reverse *)
    (@eval 7
      [:: bvec_of_N _
          (foldl (fun a => N.add (a * 256)) 0 [:: 1; 2; 3; 4; 5; 6; 7; 8])%N]
      (efold (evar 0) ezero
             (eop2 opor (evar 0)
                   (efold ezero (evar 1) (eop1 opshl1 (evar 1)))))).