Module cssexist Import misc cssrel cssexistl cssexistm cssexistx ;

(***** This puts together cssexistl, cssexistm and cssexistx to show that
       the CSS relation gives a function: For every input there is an output
 *****)

(***** So far we've been working with a key (K0 ... K4) and
       a sector (S) in our environment; we now discharge them to make
       them parameters. *****)

Discharge K0 ;

(************ This is the main theorem *********)
Goal
{K0,K1,K2,K3,K4:byte}        (* For every key... *)
{S:sector}                   (* And every sector ... *)
{i:nat}{ii:index i}          (* And every i < 2048 ... *)
Ex[b:byte]                   (* There is a byte ... *)
CSS K0 K1 K2 K3 K4 S i ii b; (* output by the CSS relation *)
(************ Proof: ***********)
intros K0 K1 K2 K3 K4 S i ii;
(* Use trichotomy i < = > 127 *)
Refine Trich_rec i num127;
(* i < 127 *)
intros lt ;
Refine ExIn (S i ii);
Refine pair;
Refine pair;
intros ;
Refine Eq_refl;
intros ;
Refine Eq_refl;
intros in ;
Refine not_Lt_Gt i num127 ;
Immed ;
Refine in.1;
(* i > 127 *)
intros gt ;
Refine Xproof K0 K1 K2 K3 K4 S i (gt, ii);
intros w xw ;
Refine ExIn (bXor (wLowByte w) (PAL (S i ii)));
Refine pair ;
Refine pair ;
intros lt ;
Refine not_Lt_Gt i num127 ;
Immed ;
intros eq ;
Refine not_Lt_Eq num127 i ;
Immed ;
intros in ;
Refine ExIn w ;
Refine pair ;
Immed ;
Refine Eq_refl ;
(* i = 127 *)
intros eq ;
Refine ExIn (S i ii);
Refine pair;
Refine pair;
intros ;
Refine Eq_refl;
intros ;
Refine Eq_refl;
intros in ;
Refine not_Gt_Eq i num127 ;
Immed ;
Refine in.1;
Save CSSproof; (* QED *)

(* There we have it - the CSS Relation really does define a function.
   Note that this is a purely mathematical result.  In particular, I have
   not shown that any particular program produces an output - I have
   carefully avoided repesenting any program for CSS, but have just used
   a mathematical relation between inputs and outputs.

   This is an important piece of information; it is not obvious from looking
   at the definition of CSS that it really does produce an output from every
   input.

   It would be disastrous if our theorem we not true : imagine making a movie
   but then finding that CSS cannot be used to put your movie onto DVD.

   Or buying a DVD drive and a DVD, but discovering that the CSS algorithm
   cannot decode the content of the DVD.

   This proof gives value to both consumers and content-producers, by giving
   them confidence in the reliability of the CSS technology.
 *)
   
(* However, my attempt to avoid actually giving a program for CSS is a 
   failure.  The proof - the object CSSproof defined above - is also a
   program.  This program implements the CSS algorithm.

   My failure to avoid giving a program is not due to incompetence or lack
   of skill on my part.  Rather, it is a consequence of a deep mathematical
   result - the Curry-Howard isomorphism - that shows that proofs are
   programs, and vice-versa.

   For the mathematical result above, the Curry-Howard isomorphism says

   Applied to the result we set out to prove; Curry-Howard says that any
   proof is a program implementing CSS; it is a mathematical impossibility
   to proof our result without giving such a program.
*)

(*
   Instructions for running the program.

   **** BEFORE RUNNING THIS PROGRAM, YOU MUST CHECK THE APPROPRIATE LOCAL
        LAWS.  I WILL NOT BE RESPONSIBLE IF FOLLOWING THESE INSTRUCTIONS
        VIOLATES THE DMCA OR ANY OTHER ACT ****

   (1) Encode your sector as an object of type {i:nat}(index i)->byte :

       [ S = ... : {i:nat}(index i)->byte ];

   (2) Encode your key as 5 bytes :

       [ K0 = ... : byte ];
       [ K1 = ... : byte ];
       [ K2 = ... : byte ];
       [ K3 = ... : byte ];
       [ K4 = ... : byte ];

   (3) Choose the index J of the byte you want to extract, and give a proof
       JJ that J < 2048:

       [ J = ... : nat ];
       [ JJ = ... : index J ];

   (4) Use the lego "Normal" directive to extract the byte:

   (Normal (witness (CSSproof K0 K1 K2 K3 K4 S J JJ)));

*)