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)));
*)