Changeset 2164


Ignore:
Timestamp:
Jul 7, 2012, 3:00:44 AM (5 years ago)
Author:
sacerdot
Message:

More steady progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2163 r2164  
    7272    let mapped ≝ sigma word in
    7373    let 〈high, low〉 ≝ vsplit bool 8 8 mapped in
     74      if eq_upper_lower upper_lower upper then
     75        high
     76      else
     77        low
     78  ].
     79
     80(*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *)
     81definition map_internal_ram_address_using_pseudo_address_map:
     82  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
     83  λM: internal_pseudo_address_map.
     84  λsigma: Word → Word.
     85  λaddress: Byte.
     86  λvalue: Byte.
     87  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
     88  [ None ⇒ value
     89  | Some upper_lower_word ⇒
     90    let 〈upper_lower, word〉 ≝ upper_lower_word in
     91    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
    7492      if eq_upper_lower upper_lower upper then
    7593        high
     
    319337qed.
    320338
    321 check status_of_pseudo_status
    322 
    323 lemma set_low_internal_fram_status_of_pseudo_status:
     339lemma set_low_internal_ram_status_of_pseudo_status:
    324340 ∀cm,sigma,policy,M,s,ram.
    325341  set_low_internal_ram (BitVectorTrie Byte 16)
     
    331347 //
    332348qed.
     349
     350(* Real axiom ATM *)
     351axiom insert_low_internal_ram_of_pseudo_low_internal_ram:
     352 ∀M,sigma,cm,s,addr,v,v'.
     353 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
     354  insert Byte 7 addr v'
     355  (low_internal_ram_of_pseudo_low_internal_ram M
     356   (low_internal_ram pseudo_assembly_program cm s))
     357  =low_internal_ram_of_pseudo_low_internal_ram M
     358   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
    333359               
    334 lemma set_low_internal_fram_status_of_pseudo_status:
    335  ∀M,cm,sigma,policy,s,addr,v.
    336   insert Byte 7 addr v
     360lemma insert_low_internal_ram_status_of_pseudo_status:
     361 ∀M,cm,sigma,policy,s,addr,v,v'.
     362 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
     363  insert Byte 7 addr v'
    337364   (low_internal_ram (BitVectorTrie Byte 16)
    338365    (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    341368     (insert Byte 7 addr v
    342369      (low_internal_ram pseudo_assembly_program cm s)).
    343  #M #cm #sigma #policy #s #addr #v
    344  
    345 
    346 definition map_address_mode_using_internal_pseudo_address_map ≝
    347  λM,sigma,addr,v.
     370 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
     371qed.
     372
     373(*CSC: Taken from AssemblyProofSplit *)
     374lemma get_index_v_set_index_miss:
     375  ∀T: Type[0].
     376  ∀n, i, j: nat.
     377  ∀v: Vector T n.
     378  ∀b: T.
     379  ∀i_proof: i < n.
     380  ∀j_proof: j < n.
     381  i ≠ j →
     382    get_index_v T n (set_index T n v i b i_proof) j j_proof =
     383      get_index_v T n v j j_proof.
     384  #T #n #i #j #v lapply i lapply j elim v #i #j
     385  [1:
     386    #b #i_proof
     387    cases (lt_to_not_zero … i_proof)
     388  |2:
     389    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
     390    lapply i_proof lapply i_neq_j cases i'
     391    [1:
     392      -i_neq_j #i_neq_j -i_proof #i_proof
     393      whd in match (set_index ??????);
     394      lapply j_proof lapply i_neq_j cases j'
     395      [1:
     396        #relevant @⊥ cases relevant -relevant #absurd @absurd %
     397      |2:
     398        #j' #_ -j_proof #j_proof %
     399      ]
     400    |2:
     401      #i' -i_neq_j #i_neq_j -i_proof #i_proof
     402      lapply j_proof lapply i_neq_j cases j'
     403      [1:
     404        #_ #j_proof %
     405      |2:
     406        #j' #i_neq_j #j_proof
     407        @inductive_hypothesis @nmk #relevant
     408        cases i_neq_j #absurd @absurd >relevant %
     409      ]
     410    ]
     411  ]
     412qed.
     413
     414lemma get_8051_sfr_status_of_pseudo_status:
     415 ∀M,cm,s,sigma,policy,sfr.
     416  get_8051_sfr …
     417   (code_memory_of_pseudo_assembly_program cm sigma policy)
     418   (status_of_pseudo_status M cm s sigma policy) sfr =
     419  map_address_using_internal_pseudo_address_map M sigma sfr
     420   (get_8051_sfr … cm s sfr).
     421 #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%);
     422 whd in match status_of_pseudo_status; normalize nodelta
     423 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     424 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
     425 cases (\snd M) normalize nodelta [cases sfr %]
     426 #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta
     427 cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta
     428 [18,37: @get_index_v_set_index
     429 |*: >get_index_v_set_index_miss % normalize #abs destruct]
     430qed.
     431
     432lemma bit_address_of_register_status_of_pseudo_status:
     433 ∀M,cm,s,sigma,policy,r.
     434  bit_address_of_register …
     435  (code_memory_of_pseudo_assembly_program cm sigma policy)
     436  (status_of_pseudo_status M cm s sigma policy) r =
     437  bit_address_of_register … cm s r.
     438 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
     439 >get_8051_sfr_status_of_pseudo_status
     440 @pair_elim #un #ln #_
     441 @pair_elim #r1 #r0 #_ %
     442qed.
     443
     444(*CSC: provable using the axiom in AssemblyProof, but this one seems more
     445  primitive *)
     446axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
     447 ∀M,sigma,cm,s,addr.
     448  lookup Byte 7 addr
     449  (low_internal_ram_of_pseudo_low_internal_ram M
     450   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
     451  =
     452  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
     453  (lookup Byte 7 addr
     454   (low_internal_ram pseudo_assembly_program cm s) (zero 8)).
     455
     456lemma get_register_status_of_pseudo_status:
     457 ∀M,cm,sigma,policy,s,r.
     458  get_register …
     459   (code_memory_of_pseudo_assembly_program cm sigma policy)
     460   (status_of_pseudo_status M cm s sigma policy) r =
     461  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
     462   (get_register … cm s r).
     463 #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta
     464 whd in match status_of_pseudo_status; normalize nodelta
     465 >bit_address_of_register_status_of_pseudo_status
     466 @lookup_low_internal_ram_of_pseudo_low_internal_ram
     467qed.
     468
     469definition map_address_mode_using_internal_pseudo_address_map_ok ≝
     470 λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'.
    348471  match addr with
    349472  [ DIRECT d ⇒
    350      let 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in
    351      match get_index_v ? ? nu 0 ? with
     473     let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in
     474     match head' … bit_one with
    352475     [ true ⇒
    353       map_address_Byte_using_internal_pseudo_address_map M sigma d v
    354      | false ⇒ v ]
    355   | _ ⇒ v ].
    356 //
    357 qed.
     476      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
     477     | false ⇒
     478      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] = v'
     479  | INDIRECT i ⇒
     480     assoc_list_lookup ??
     481      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … ∧
     482     let register ≝ get_register ?? s [[ false; false; i ]] in
     483     map_internal_ram_address_using_pseudo_address_map M sigma register v = v'
     484  | _ ⇒ v = v'].
    358485
    359486definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
     
    368495      [ DIRECT d ⇒
    369496        λdirect: True.
    370           let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
    371           let bit_one ≝ get_index_v ? ? nu 0 ? in
    372           let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    373             match bit_one with
    374               [ true ⇒ set_bit_addressable_sfr ?? s d v
     497          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
     498            match head' … bit_one with
     499              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
    375500              | false ⇒
    376                 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
     501                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
    377502                  set_low_internal_ram ?? s memory
    378503              ]
     
    380505        λindirect: True.
    381506          let register ≝ get_register ?? s [[ false; false; i ]] in
    382           let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
    383           let bit_1 ≝ get_index_v … nu 0 ? in
    384           let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    385             match bit_1 with
     507          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
     508            match head' … bit_one with
    386509              [ false ⇒
    387                 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
     510                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    388511                  set_low_internal_ram ?? s memory
    389512              | true ⇒
    390                 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
     513                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    391514                  set_high_internal_ram ?? s memory
    392515              ]
     
    409532          match other in False with [ ]
    410533      ] (subaddressing_modein … a).
    411   //
     534
     535(*CSC: move elsewhere*)
     536lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v.
     537 #A #n #v inversion v in ⊢ ?;
     538 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/
     539 | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ]
     540qed.
     541
     542(*CSC: move elsewhere*)
     543lemma tail_singleton: ∀A,v. tail A 0 v = [[]].
     544 #A #v inversion v in ⊢ ?;
     545 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H)
     546 | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize
     547   /2 by jmeq_to_eq/
     548 ]
     549qed.
     550
     551(*CSC: move elsewhere*)
     552lemma eq_cons_head_append:
     553 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n.
     554  head' A 0 hd:::tl = hd@@tl.
     555 #A #n #hd #tl >(eq_head' … hd) >tail_singleton %
    412556qed.
    413557
     
    417561  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    418562  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
    419    map_address_mode_using_internal_pseudo_address_map M sigma addr value = value' →
     563   map_address_mode_using_internal_pseudo_address_map_ok … M sigma cm ps addr value value' →
    420564    set_arg_8 (BitVectorTrie Byte 16)
    421565      (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    434578      [ DIRECT d ⇒
    435579        λdirect: True.
    436           deplet 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in
    437           let bit_one ≝ get_index_v ? ? nu 0 ? in
    438           let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    439             match bit_one with
    440               [ true ⇒ set_bit_addressable_sfr ?? s d v
     580          deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in
     581            match head' … bit_one with
     582              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
    441583              | false ⇒
    442                 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
     584                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
    443585                  set_low_internal_ram ?? s memory
    444586              ]
     
    446588        λindirect: True.
    447589          let register ≝ get_register ?? s [[ false; false; i ]] in
    448           let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
    449           let bit_1 ≝ get_index_v … nu 0 ? in
    450           let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    451             match bit_1 with
     590          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
     591            match head' … bit_one with
    452592              [ false ⇒
    453                 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
     593                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    454594                  set_low_internal_ram ?? s memory
    455595              | true ⇒
    456                 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
     596                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    457597                  set_high_internal_ram ?? s memory
    458598              ]
     
    475615          match other in False with [ ]
    476616      ] (subaddressing_modein … a)) normalize nodelta
    477   [3,6: // ] #M #sigma #policy #v' whd in ⊢ (??%? → ?);
     617  #M #sigma #policy #v' whd in match map_address_mode_using_internal_pseudo_address_map_ok; normalize nodelta
    478618  [1,2:
    479619    <vsplit_refl normalize nodelta >p normalize nodelta
    480     normalize nodelta in p1; >p1 normalize nodelta
    481     [ @set_bit_addressable_sfr_status_of_pseudo_status
    482     | #v_ok <v_ok @set_low_internal_ram_status_of_pseudo_status
    483     ]
    484   |2:   
    485 qed.
     620    [ >(vsplit_ok … vsplit_refl) @set_bit_addressable_sfr_status_of_pseudo_status
     621    | #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
     622  |3,4: * #EQ1 #EQ2 change with (get_register ????) in match register in p;
     623      >get_register_status_of_pseudo_status
     624      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
     625      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
     626      [
     627      | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
     628        @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
     629qed.
Note: See TracChangeset for help on using the changeset viewer.