(* Formalisation of 2048 byte sector *)

Module sector Import byte word lib_nat lib_nat_Le lib_nat_Lt ;

(* Using normal here isn't pretty but should avoid repeated evaluation... *)
[ num64 = (Normal (times eight eight)) ];
[ num128 = (Normal (plus num64 num64)) ];
[ num127 = (Normal (pred num128)) ];
[ num512 = (Normal (times eight num64)) ];
[ num2048 = (Normal (times four num512)) ];

[ index = [i:nat] (Lt i num2048) ];

[ sector = {i:nat} (index i) -> byte ];
[ wsector = {i:nat} (index i) -> word ];

(* A predicate for the range [128,2047] *)
[ in128to2048 = [i:nat] (Lt num127 i) # (index i) ];

[ is127 = Eq num127 ];

[ lt127 = [i:nat] Lt i num127 ];

[num84 = (Normal (plus num64 (plus ten ten)))];
[num85 = suc (num84)];
[num86 = suc (num85)];
[num87 = suc (num86)];
[num88 = suc (num87)];

(* Yee Haa... Hope you have a fast machine... *)
Goal index num512 ;
Intros B H;
Refine H;
Refine minus num2048 (suc num512);
Normal ;
Refine Eq_refl num2048 ;
Save index512;

(******** Prove that various numbers are indexes *********)

Goal Lt num128 num512;
Intros B H;
Refine H;
Refine minus num512 (suc num128);
Refine Eq_refl;
Save lt_128_512;

Goal Lt num127 num128;
Intros B H;
Refine H;
Refine zero;
Refine Eq_refl;
Save lt_127_128;

Goal Lt num88 num128;
Intros B H;
Refine H;
Refine minus num128 (suc num88);
Refine Eq_refl;
Save lt_88_128;

Goal Lt num87 num128;
Intros B H;
Refine H;
Refine minus num128 num88;
Refine Eq_refl;
Save lt_87_128;

Goal Lt num86 num128;
Intros B H;
Refine H;
Refine minus num128 num87;
Refine Eq_refl;
Save lt_86_128;

Goal Lt num85 num128;
Intros B H;
Refine H;
Refine minus num128 num86;
Refine Eq_refl;
Save lt_85_128;

Goal Lt num84 num128;
Intros B H;
Refine H;
Refine minus num128 num85;
Refine Eq_refl;
Save lt_84_128;

Goal index num128 ;
Refine Lt_trans;
Refine num512;
Refine lt_128_512 ;
Refine index512 ;
Save index128 ;

Goal index num127 ;
Refine Lt_trans;
Refine num128;
Refine lt_127_128 ;
Refine index128 ;
Save index127 ;


Goal index num84 ;
Refine Lt_trans;
Refine num128;
Refine lt_84_128 ;
Refine index128 ;
Save index84 ;


Goal index num85 ;
Refine Lt_trans;
Refine num128;
Refine lt_85_128 ;
Refine index128 ;
Save index85 ;


Goal index num86 ;
Refine Lt_trans;
Refine num128;
Refine lt_86_128 ;
Refine index128 ;
Save index86 ;


Goal index num87 ;
Refine Lt_trans;
Refine num128;
Refine lt_87_128 ;
Refine index128 ;
Save index87 ;


Goal index num88 ;
Refine Lt_trans;
Refine num128;
Refine lt_88_128 ;
Refine index128 ;
Save index88 ;