Ignore:
Timestamp:
Jan 28, 2012, 1:42:15 PM (8 years ago)
Author:
sacerdot
Message:

PreStatus? datatype change: the code_memory field is not a left parameter.
This greatly simplify the dependent type madness due to policy depending
on the code_memory and not really on the status. On the other hand it
makes the rest of the code uglier.

Note: the changes have not been propagated yet to ASMCosts, CostsProof? and
Interpret2. The AssemlyProof? is almost repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r1606 r1666  
    11include "ASM/Status.ma".
    22
     3(* clock_set_bit_addressable_sfr defined in ASM/Status.ma *)
     4
     5lemma clock_set_low_internal_ram:
     6  ∀M: Type[0]. ∀cm.
     7  ∀s: PreStatus M cm.
     8  ∀ram: BitVectorTrie Byte 7.
     9    clock M cm (set_low_internal_ram … s ram) = clock M cm s.
     10  //
     11qed.
     12
     13lemma clock_set_high_internal_ram:
     14  ∀m: Type[0]. ∀cm.
     15  ∀s: PreStatus m cm.
     16  ∀ram: BitVectorTrie Byte 7.
     17    clock ?? (set_high_internal_ram … s ram) = clock … s.
     18  //
     19qed.
     20
     21lemma clock_write_at_stack_pointer:
     22  ∀m: Type[0].
     23  ∀cm:m.
     24  ∀s: PreStatus m cm.
     25  ∀v: Byte.
     26    clock ?? (write_at_stack_pointer … s v) = clock ?? s.
     27  #m #s #v
     28  whd in match write_at_stack_pointer; normalize nodelta
     29  cases(split … 4 4 ?) #nu #nl normalize nodelta
     30  cases(get_index_v … 4 nu 0 ?) //
     31qed.
     32
     33lemma clock_set_clock:
     34  ∀M: Type[0]. ∀cm.
     35  ∀s: PreStatus M cm.
     36  ∀v.
     37    clock ?? (set_clock … s v) = v.
     38 //
     39qed.
     40
     41lemma clock_set_program_counter:
     42  ∀M: Type[0]. ∀cm.
     43  ∀s: PreStatus M cm.
     44  ∀pc: Word.
     45    clock M cm (set_program_counter … s pc) = clock … s.
     46  //
     47qed.
     48
     49lemma clock_set_8051_sfr:
     50  ∀M: Type[0]. ∀cm.
     51  ∀s: PreStatus M cm.
     52  ∀sfr: SFR8051.
     53  ∀v: Byte.
     54    clock ?? (set_8051_sfr … s sfr v) = clock … s.
     55 //
     56qed.
     57
     58lemma clock_set_flags:
     59 ∀M,cm,s,f1,f2,f3. clock M cm s = clock … (set_flags … s f1 f2 f3).
     60//
     61qed.
     62
    363lemma get_register_set_program_counter:
    4  ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
    5  #T #s #pc %
     64 ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s.
     65 //
    666qed.
    767
    868lemma get_8051_sfr_set_program_counter:
    9  ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
    10  #T #s #pc %
     69 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s.
     70 //
    1171qed.
    1272
    1373lemma get_bit_addressable_sfr_set_program_counter:
    14  ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
    15  #T #s #pc %
     74 ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s.
     75 //
    1676qed.
    1777
    1878lemma low_internal_ram_set_program_counter:
    19  ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
    20  #T #s #pc %
     79 ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s.
     80 //
    2181qed.
    2282
    2383example get_arg_8_set_program_counter:
    2484 ∀n.∀l:Vector addressing_mode_tag (S n).
    25   ∀T,s,pc,b.∀arg:l.
     85  ∀T,cm,s,pc,b.∀arg:l.
    2686   ∀prf:is_in ?
    2787    [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg.
    28    get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
    29  [ #n #l #T #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H
     88   get_arg_8 T cm (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
     89 [ #n #l #T #cm #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H
    3090 | cases arg in prf; *; normalize //
    3191 | skip ]
    3292qed.
    3393
     94(*
    3495lemma set_bit_addressable_sfr_set_code_memory:
    3596  ∀T, U: Type[0].
     
    121182  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    122183  try % @set_bit_addressable_sfr_set_code_memory
    123 qed.
     184qed. *)
    124185
    125186example set_arg_8_set_program_counter:
    126187  ∀n:nat.
    127188  ∀l:Vector addressing_mode_tag (S n).
    128     ∀T: Type[0].
    129     ∀ps: PreStatus ?.
     189    ∀T: Type[0]. ∀cm.
     190    ∀ps: PreStatus ? cm.
    130191    ∀pc.
    131192    ∀val.
     
    133194    ∀prf:is_in ?
    134195     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    135   set_arg_8 ? (set_program_counter T ps pc) b val =
    136   set_program_counter T (set_arg_8 ? ps b val) pc.
     196  set_arg_8 … (set_program_counter T cm ps pc) b val =
     197  set_program_counter T cm (set_arg_8 ?? ps b val) pc.
    137198  [2,3: cases b in prf; *; normalize //]
    138   #n #l #T #ps #pc #val * *;
     199  #n #l #T #cm #ps #pc #val * *;
    139200  #x try (#y #H) try #H whd in H; try cases H try %
    140201  whd in match set_arg_8; normalize nodelta
     
    146207qed.
    147208 
    148 
    149 lemma get_arg_8_set_code_memory:
     209(*lemma get_arg_8_set_code_memory:
    150210 ∀T1,T2,s,code_mem,b,arg.
    151211   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
     
    158218   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
    159219 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
    160 qed.
     220qed.*)
    161221
    162222lemma set_program_counter_set_flags:
    163  ∀T1,s,f1,f2,f3,pc.
    164   set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
     223 ∀T1,cm,s,f1,f2,f3,pc.
     224  set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc =
    165225   set_flags … (set_program_counter … s pc) f1 f2 f3.
    166  #T1 #s #f1 #f2 #f3 #pc  %
     226 //
    167227qed.
    168228
    169229lemma program_counter_set_flags:
    170  ∀T1,s,f1,f2,f3.
    171   program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
    172  #T1 #s #f1 #f2 #f3 %
     230 ∀T1,cm,s,f1,f2,f3.
     231  program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s.
     232 //
    173233qed.
    174234
    175235lemma special_function_registers_8051_write_at_stack_pointer:
    176  ∀T,s,x.
    177     special_function_registers_8051 T (write_at_stack_pointer T s x)
    178   = special_function_registers_8051 T s.
    179  #T #s #x whd in ⊢ (??(??%)?);
     236 ∀T,cm,s,x.
     237    special_function_registers_8051 T cm (write_at_stack_pointer T cm s x)
     238  = special_function_registers_8051 T cm s.
     239 #T #cm #s #x whd in ⊢ (??(???%)?);
    180240 cases (split ????) #nu #nl normalize nodelta;
    181241 cases (get_index_v bool ????) %
     
    183243
    184244lemma get_8051_sfr_write_at_stack_pointer:
    185  ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
    186  #T #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
    187 qed.
    188 
    189 lemma code_memory_write_at_stack_pointer:
     245 ∀T,cm,s,x,y. get_8051_sfr T cm (write_at_stack_pointer T cm s x) y = get_8051_sfr T cm s y.
     246 #T #cm #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
     247qed.
     248
     249(*lemma code_memory_write_at_stack_pointer:
    190250 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
    191251 #T #s #x whd in ⊢ (??(??%)?);
    192252 cases (split ????) #nu #nl normalize nodelta;
    193253 cases (get_index_v bool ????) %
    194 qed.
     254qed.*)
    195255
    196256lemma set_program_counter_set_low_internal_ram:
    197  ∀T,s,x,y.
    198   set_program_counter T (set_low_internal_ram … s x) y =
     257 ∀T,cm,s,x,y.
     258  set_program_counter T cm (set_low_internal_ram … s x) y =
    199259   set_low_internal_ram … (set_program_counter … s y) x.
    200260 //
     
    202262
    203263lemma set_clock_set_low_internal_ram:
    204  ∀T,s,x,y.
    205   set_clock T (set_low_internal_ram … s x) y =
     264 ∀T,cm,s,x,y.
     265  set_clock T cm (set_low_internal_ram … s x) y =
    206266   set_low_internal_ram … (set_clock … s y) x.
    207267 //
     
    209269
    210270lemma set_program_counter_set_high_internal_ram:
    211  ∀T,s,x,y.
    212   set_program_counter T (set_high_internal_ram … s x) y =
     271 ∀T,cm,s,x,y.
     272  set_program_counter T cm (set_high_internal_ram … s x) y =
    213273   set_high_internal_ram … (set_program_counter … s y) x.
    214274 //
     
    216276
    217277lemma set_clock_set_high_internal_ram:
    218  ∀T,s,x,y.
    219   set_clock T (set_high_internal_ram … s x) y =
     278 ∀T,cm,s,x,y.
     279  set_clock T cm (set_high_internal_ram … s x) y =
    220280   set_high_internal_ram … (set_clock … s y) x.
    221281 //
     
    223283
    224284lemma set_low_internal_ram_set_high_internal_ram:
    225  ∀T,s,x,y.
    226   set_low_internal_ram T (set_high_internal_ram … s x) y =
     285 ∀T,cm,s,x,y.
     286  set_low_internal_ram T cm (set_high_internal_ram … s x) y =
    227287   set_high_internal_ram … (set_low_internal_ram … s y) x.
    228288 //
     
    230290
    231291lemma external_ram_write_at_stack_pointer:
    232  ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
    233  #T #s #x whd in ⊢ (??(??%)?);
     292 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
     293 #T #cm #s #x whd in ⊢ (??(???%)?);
    234294 cases (split ????) #nu #nl normalize nodelta;
    235295 cases (get_index_v bool ????) %
     
    237297
    238298lemma special_function_registers_8052_write_at_stack_pointer:
    239  ∀T,s,x.
    240     special_function_registers_8052 T (write_at_stack_pointer T s x)
    241   = special_function_registers_8052 T s.
    242  #T #s #x whd in ⊢ (??(??%)?);
     299 ∀T,cm,s,x.
     300    special_function_registers_8052 T cm (write_at_stack_pointer T cm s x)
     301  = special_function_registers_8052 T cm s.
     302 #T #cm #s #x whd in ⊢ (??(???%)?);
    243303 cases (split ????) #nu #nl normalize nodelta;
    244304 cases (get_index_v bool ????) %
     
    246306
    247307lemma p1_latch_write_at_stack_pointer:
    248  ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
    249  #T #s #x whd in ⊢ (??(??%)?);
     308 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
     309 #T #cm #s #x whd in ⊢ (??(???%)?);
    250310 cases (split ????) #nu #nl normalize nodelta;
    251311 cases (get_index_v bool ????) %
     
    253313
    254314lemma p3_latch_write_at_stack_pointer:
    255  ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
    256  #T #s #x whd in ⊢ (??(??%)?);
    257  cases (split ????) #nu #nl normalize nodelta;
    258  cases (get_index_v bool ????) %
    259 qed.
    260 
    261 lemma clock_write_at_stack_pointer:
    262  ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
    263  #T #s #x whd in ⊢ (??(??%)?);
     315 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
     316 #T #cm #s #x whd in ⊢ (??(???%)?);
    264317 cases (split ????) #nu #nl normalize nodelta;
    265318 cases (get_index_v bool ????) %
     
    270323
    271324lemma get_8051_sfr_set_8051_sfr:
    272  ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
    273  #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);
     325 ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y.
     326 #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?);
    274327 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
    275328qed.
    276329
    277330lemma program_counter_set_8051_sfr:
    278  ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
     331 ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s.
    279332 //
    280333qed.
    281334
    282335axiom get_arg_8_set_low_internal_ram:
    283  ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.
     336 ∀M,cm,s,x,b,z. get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
    284337
    285338lemma split_eq_status:
    286  ∀T.
    287  ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
    288  ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
    289   A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
    290    mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
    291    mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
    292  //
    293 qed.
     339 ∀T,cm.
     340 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9.
     341 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9.
     342  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 →
     343   mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 =
     344   mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9.
     345 //
     346qed.
Note: See TracChangeset for help on using the changeset viewer.