(**
  SQL Encoding function and Proofs of safety
  Yoshihiro Imai (IT Planning inc.)
*)

Require Import Bool.
Require Import List.

(** 
　　まずは準備。Coqで文字列を形式化し、基本的な性質を証明する。
*)

Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).

Inductive string : Set :=
  | EmptyString : string
  | String : ascii -> string -> string.

Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}.
  decide equality; apply bool_dec.
Defined.

Inductive IsMember : ascii -> string -> Prop :=
  | memhd : forall (a:ascii)(s:string), IsMember a (String a s)
  | memtl : forall (a b:ascii)(s:string),
      IsMember a s -> IsMember a (String b s).

Definition in_dec_ascii := List.In_dec ascii_dec.

(** "\" : ascii *)
Definition aBACKSLASH := Ascii false false true true  true false true false.
(** "'" : ascii *)
Definition aQUOTE := Ascii true true true false  false true false false.


(**
　　次に目的となるエンコード関数を書く。
*)

Fixpoint encode (esc:ascii)(keys:list ascii)(s:string){struct s} : string :=
  match s with
  | EmptyString => EmptyString
  | String hd tl =>
      match in_dec_ascii hd keys with
      | left _ => String esc (String hd (encode esc keys tl))
      | right _  => String hd (encode esc keys tl)
      end
  end.

Definition keywords : list ascii := aBACKSLASH :: aQUOTE :: nil.
Definition sql_encode s := encode aBACKSLASH keywords s.


(**
　　以下ではエンコード関数が正しく働くことを保証する証明をする。
　　この部分は実装には無関係である。
*)

(** エスケーピングする関数を用意　*)
Fixpoint escape (a:ascii)(s:string) {struct s} : string :=
  match s with
  | EmptyString => EmptyString
  | String hd1 tl =>
      match ascii_dec a hd1 with
      | left _ =>
         match tl with
         | EmptyString => s
         | String hd2 tltl => escape a tltl
         end
      | right _ => String hd1 (escape a tl)
      end
  end.

(** ここから少し一般的な性質の証明 *)
Section EncodingSafety.
Variable keys : list ascii.
Variable esc : ascii.
Hypothesis HH : In esc keys.

Lemma isntmem_cons : forall (k a:ascii) (s:string),
  In k keys ->  not (IsMember k (escape esc (encode esc keys s))) ->
   k <> a -> not (IsMember k (escape esc (encode esc keys (String a s)))).
Proof.
intros.
unfold encode in |- *.
case (in_dec_ascii a keys).
 intro; fold encode in |- *.
   unfold escape in |- *.
   case (ascii_dec esc esc).
  intro; fold escape in |- *.
    assumption.
  intro neq; elim neq; reflexivity.
 intro; fold encode in |- *.
   unfold escape in |- *.
   case (ascii_dec esc a).
  intro eq; rewrite <- eq in n.
    elim n; apply HH.
  intro neq; fold escape in |- *.
    intro.
    inversion H2.
   elim H1; assumption.
   elim H0; assumption.
Qed.

Theorem encoding_safety : forall (k:ascii)(s:string), 
  List.In k keys -> not (IsMember k (escape esc (encode esc keys s))).
Proof.
intros.
induction s.
 intro.
   unfold encode in H0.
   unfold escape in H0.
   inversion H0.
 case (ascii_dec k a).
  intro eq; rewrite <- eq.
    unfold encode in |- *.
    unfold in_dec_ascii in |- *.
    case (In_dec ascii_dec k keys).
   intro; fold encode in |- *.
     unfold escape in |- *.
     case (ascii_dec esc esc).
    intro; fold escape in |- *.
      apply IHs.
    intro neq; elim neq; reflexivity.
   intro not; elim not; assumption.
  apply isntmem_cons.
   assumption.
   assumption.
Qed.
End EncodingSafety.
(** 一般的な性質の証明終わり。 *)

Definition sql_safe (s:string) := not (IsMember aQUOTE (escape aBACKSLASH s)).

Fact f : In aBACKSLASH keywords.
Proof.
simpl.
left; reflexivity.
Qed.

Theorem sql_encoding_safety : forall (s:string), sql_safe (sql_encode s).
Proof.
intro s.
apply (encoding_safety keywords aBACKSLASH f aQUOTE s).
simpl.
right; left; reflexivity.
Qed.