Changeset 2276


Ignore:
Timestamp:
Jul 30, 2012, 2:36:41 PM (7 years ago)
Author:
sacerdot
Message:

...

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2272 r2276  
    463463          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
    464464
     465definition lookup_from_internal_ram:
     466    ∀addr: Byte.
     467    ∀M: internal_pseudo_address_map.
     468      option address_entry ≝
     469  λaddr, M.
     470    let 〈low, high, accA〉 ≝ M in
     471    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
     472      if head' … bit_one then
     473        lookup_opt … seven_bits high
     474      else
     475        lookup_opt … seven_bits low.
     476
     477definition map_value_using_opt_address_entry:
     478  (Word → Word) → Byte → option address_entry → Byte ≝
     479  λsigma: Word → Word.
     480  λvalue: Byte.
     481  λul_addr: option address_entry.
     482  match ul_addr with
     483  [ None ⇒ value
     484  | Some upper_lower_word ⇒
     485    let 〈upper_lower, word〉 ≝ upper_lower_word in
     486      if eq_upper_lower upper_lower upper then
     487        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
     488          high
     489      else
     490        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
     491          low
     492  ].
     493
     494definition map_acc_a_using_internal_pseudo_address_map:
     495 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
     496   λM, sigma, v. map_value_using_opt_address_entry sigma v (\snd M).
     497
     498definition map_internal_ram_address_using_pseudo_address_map:
     499  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
     500  λM: internal_pseudo_address_map.
     501  λsigma: Word → Word.
     502  λaddress: Byte.
     503  λvalue: Byte.
     504   map_value_using_opt_address_entry sigma value
     505    (lookup_from_internal_ram … address M ).
     506
     507definition map_opt_value_using_opt_address_entry:
     508 (Word → Word) → option Byte → option address_entry → option Byte ≝
     509 λsigma,v,ul_addr.
     510  let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
     511  let v' ≝ map_value_using_opt_address_entry sigma v ul_addr in
     512    if eq_bv … v' (zero …) then
     513      None …
     514    else
     515      Some … v'.
     516
    465517definition internal_ram_of_pseudo_internal_ram:
    466518    ∀sigma: Word → Word.
     
    469521      BitVectorTrie Byte 7 ≝
    470522  λsigma, ram, map.
    471       bvt_map2 ??? ? ram map (λv. λul_addr.
    472         match
    473         match ul_addr with
    474         [ None ⇒ v
    475         | Some ul_addr' ⇒
    476           let 〈ul, addr〉 ≝ ul_addr' in
    477           let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
    478           match ul with
    479           [ upper ⇒
    480             let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
    481               Some … high
    482           | lower ⇒
    483             let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
    484               Some … low
    485           ]
    486         ] with
    487         [ None ⇒ None …
    488         | Some v ⇒
    489           if eq_bv … v (zero …) then
    490             None …
    491           else
    492             Some … v
    493         ]).
     523      bvt_map2 ??? ? ram map (map_opt_value_using_opt_address_entry sigma).
     524
     525axiom insert_internal_ram_of_pseudo_internal_ram:
     526 ∀M,M',sigma,addr,v,v',ram.
     527  v' = map_value_using_opt_address_entry sigma v (lookup_opt … addr M) →
     528  (∀addr'. addr' ≠ addr → lookup_opt … addr' M = lookup_opt … addr' M') →
     529  insert Byte … addr v' (internal_ram_of_pseudo_internal_ram sigma ram M)
     530  = internal_ram_of_pseudo_internal_ram sigma (insert ?? addr v ram) M'.
    494531
    495532definition low_internal_ram_of_pseudo_low_internal_ram:
     
    677714      | Some v' ⇒ insert_into_internal_ram addr v' M
    678715      ].
    679 
    680 definition lookup_from_internal_ram:
    681     ∀addr: Byte.
    682     ∀M: internal_pseudo_address_map.
    683       option address_entry ≝
    684   λaddr, M.
    685     let 〈low, high, accA〉 ≝ M in
    686     let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
    687       if head' … bit_one then
    688         lookup_opt … seven_bits high
    689       else
    690         lookup_opt … seven_bits low.
    691716   
    692717definition next_internal_pseudo_address_map0 ≝
  • src/ASM/AssemblyProofSplit.ma

    r2273 r2276  
    5656qed.
    5757
     58lemma get_arg_8_status_of_pseudo_status':
     59  ∀cm,ps,l.
     60  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
     61  ∀M. ∀sigma. ∀policy. ∀s.
     62      s = status_of_pseudo_status M cm ps sigma policy →
     63      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     64      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr)
     65      = get_arg_8 … ps l addr →
     66      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     67      s l addr = get_arg_8 … ps l addr.
     68 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
     69 try assumption %
     70qed.
     71
    5872lemma main_lemma_preinstruction:
    5973  ∀M, M': internal_pseudo_address_map.
     
    98112    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
    99113  (* XXX: takes about 45 minutes to type check! *)
    100   #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
     114  ** #low #high #accA #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
    101115  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
    102116  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
     
    513527  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    514528  whd in match execute_1_preinstruction; normalize nodelta
    515   [(*1,2: (* ADD and ADDC *)
     529  [1,2: (* ADD and ADDC *)
    516530    (* XXX: work on the right hand side *)
    517531    (* XXX: switch to the left hand side *)
     
    519533    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    520534    whd in maps_assm:(??%%);
    521     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     535    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    522536    [2,4: normalize nodelta #absurd destruct(absurd) ]
    523     inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     537    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    524538    [2,4: normalize nodelta #absurd destruct(absurd) ]
    525539    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    526     whd in ⊢ (??%?);
    527     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     540    letin M' ≝ (〈low,high,accA〉)
     541    whd in ⊢ (??%?);
     542    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    528543    whd in ⊢ (??%?);
    529544    normalize nodelta >EQs >EQticks <instr_refl
     
    531546    [1,3:
    532547      @eq_f3
    533       [1,2,4,5:
    534         @(pose … (set_clock ????)) #status #status_refl
    535         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    536         [1,5:
     548      [1,2,4,5: @(get_arg_8_status_of_pseudo_status' … M')
     549        [3,9:
    537550          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
    538551          @(subaddressing_mode_elim … addr1) %
    539         |3,7:
     552        |6,12:
    540553          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    541554          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    542         |2,6:
     555        |2,8:
    543556          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
    544557          @(subaddressing_mode_elim … addr1) %
    545         |4,8:
     558        |5,11:
    546559          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
    547560          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    548         ]
     561        |*: % ]
    549562      |3:
    550563        %
    551       |6:
    552         @sym_eq @(get_cy_flag_status_of_pseudo_status M')
    553         @sym_eq @set_clock_status_of_pseudo_status %
    554       ]
     564      |6: @(get_cy_flag_status_of_pseudo_status M') @set_clock_status_of_pseudo_status % ]
    555565    |2,4:
    556       #result #flags @sym_eq
    557       @set_flags_status_of_pseudo_status try %
    558       @sym_eq @set_arg_8_status_of_pseudo_status try %
    559       @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
    560     ]
    561   |3: (* SUBB *)
     566      #result #flags @set_flags_status_of_pseudo_status try %
     567      @set_arg_8_status_of_pseudo_status try %
     568      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)]
     569  |(*3: (* SUBB *)
    562570    (* XXX: work on the right hand side *)
    563571    (* XXX: switch to the left hand side *)
     
    11311139      ]
    11321140    ]
    1133   |*)12: (* JC *)
     1141  |12: (* JC *)
    11341142    >EQP -P normalize nodelta
    11351143    whd in match expand_pseudo_instruction; normalize nodelta
     
    18721880      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    18731881    ]
    1874   |*)42: (* PUSH *)
     1882  |*)*)42: (* PUSH *)
    18751883    >EQP -P normalize nodelta lapply instr_refl
    18761884    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
    18771885    #sigma_increment_commutation
    1878     whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta
     1886    whd in ⊢ (??%? → ?);
     1887    @vsplit_elim #bit_one #seven_bits
     1888    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
     1889    cases bitone #bit_one_seven_bits_refl normalize nodelta
     1890    [ @eq_bv_elim #seven_bits_refl normalize nodelta
     1891    | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
     1892      #lookup_from_internal_ram_refl ]
    18791893    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
    18801894    whd in ⊢ (??%?);
     
    18831897    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
    18841898    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
    1885     [1:
     1899    [1,3,5,7:
    18861900      @eq_f2 try %
    18871901      @(pose … (set_clock ????)) #status #status_refl
    1888       @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try %
    1889       @sym_eq @set_clock_status_of_pseudo_status
    1890       >EQs >EQticks <instr_refl %
    1891     |2:
     1902      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try %
     1903      @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
     1904    |*:
    18921905      >EQs >EQticks <instr_refl
    18931906      cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
  • src/ASM/Test.ma

    r2274 r2276  
    77lemma let_pair_in_status_of_pseudo_status:
    88  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
    9     c = c' →
    10     (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
     9    c' = c →
     10    (∀left, right.
     11      s' left right c' = status_of_pseudo_status M cm (s left right c') sigma policy) →
    1112    (let 〈left, right〉 ≝ c' in s' left right c') =
    1213    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
     
    1617lemma let_pair_as_in_status_of_pseudo_status:
    1718  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
    18     c = c'
    19     (∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') →
     19    c' = c
     20    (∀left, right, H, H'. s' left right H' c' = status_of_pseudo_status M cm (s left right H c) sigma policy) →
    2021    (let 〈left, right〉 as H' ≝ c' in s' left right H' c') =
    2122    status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
     
    3233  ∀t, t': bool.
    3334    t = t' →
    34     status_of_pseudo_status M cm s sigma policy = s'
    35     status_of_pseudo_status M cm s'' sigma policy = s'''
     35    s' = status_of_pseudo_status M cm s sigma policy
     36    s''' = status_of_pseudo_status M cm s'' sigma policy
    3637      if t then
    3738        s'
     
    5152  ∀new_ppc, new_ppc'.
    5253    sigma new_ppc = new_ppc' →
    53     status_of_pseudo_status M cm s sigma policy = s'
     54    s' = status_of_pseudo_status M cm s sigma policy
    5455    set_program_counter (BitVectorTrie Byte 16)
    5556      (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    5758    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
    5859  #M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
    59   #new_ppc_refl #s_refl <new_ppc_refl <s_refl //
     60  #new_ppc_refl #s_refl <new_ppc_refl >s_refl //
    6061qed.
    6162
     
    6768  ∀s,s'.
    6869  ∀v.
    69    status_of_pseudo_status M code_memory s sigma policy = s'
     70   s' = status_of_pseudo_status M code_memory s sigma policy
    7071    set_p1_latch (BitVectorTrie Byte 16)
    7172      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    7374    status_of_pseudo_status M code_memory
    7475      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
    75   #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
     76  #M #cm #sigma #policy #s #s' #new_ppc #s_refl >s_refl //
    7677qed.
    7778
     
    8384  ∀s, s'.
    8485  ∀v.
    85   status_of_pseudo_status M code_memory s sigma policy = s'
     86  s' = status_of_pseudo_status M code_memory s sigma policy
    8687    set_p3_latch (BitVectorTrie Byte 16)
    8788      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    8990    status_of_pseudo_status M code_memory
    9091      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
    91   #M #code_memory #sigma #policy #s #s' #v #s_refl <s_refl //
    92 qed.
    93 
    94 definition map_acc_a_using_internal_pseudo_address_map:
    95     ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
    96   λM, sigma, v.
    97   match \snd M with
    98   [ None ⇒ v
    99   | Some upper_lower_addr ⇒
    100     let 〈upper_lower, addr〉 ≝ upper_lower_addr in
    101       if eq_upper_lower upper_lower upper then
    102         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
    103           high
    104       else
    105         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
    106           low
    107   ].
    108 
    109 (*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *)
    110 definition map_internal_ram_address_using_pseudo_address_map:
    111   ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
    112   λM: internal_pseudo_address_map.
    113   λsigma: Word → Word.
    114   λaddress: Byte.
    115   λvalue: Byte.
    116   match lookup_from_internal_ram … address M with
    117   [ None ⇒ value
    118   | Some upper_lower_word ⇒
    119     let 〈upper_lower, word〉 ≝ upper_lower_word in
    120       if eq_upper_lower upper_lower upper then
    121         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
    122           high
    123       else
    124         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
    125           low
    126   ].
     92  #M #code_memory #sigma #policy #s #s' #v #s_refl >s_refl //
     93qed.
    12794
    12895definition map_address_using_internal_pseudo_address_map:
     
    277244      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    278245      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
    279       >sndM_refl normalize nodelta
     246      >sndM_refl normalize nodelta whd in match map_value_using_opt_address_entry; normalize nodelta
    280247      >eq_upper_lower_refl normalize nodelta
    281248      [1:
     
    331298      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    332299      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
    333       >sndM_refl normalize nodelta >high_low_refl normalize nodelta
     300      whd in match map_value_using_opt_address_entry; normalize nodelta
     301      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
    334302      >eq_upper_lower_refl normalize nodelta
    335303      whd in match (set_8051_sfr ?????); //
     
    342310lemma set_8051_sfr_status_of_pseudo_status:
    343311  ∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
    344     status_of_pseudo_status M code_memory s sigma policy = s'
     312    s' = status_of_pseudo_status M code_memory s sigma policy
    345313    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
    346314      set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
     
    348316        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
    349317  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
    350   <s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
     318  >s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
    351319qed.
    352320
     
    374342lemma get_8051_sfr_status_of_pseudo_status:
    375343  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
    376     status_of_pseudo_status M code_memory s sigma policy = s'
     344    s' = status_of_pseudo_status M code_memory s sigma policy
    377345    map_address_using_internal_pseudo_address_map M sigma sfr
    378346     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
     
    380348    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    381349     s' sfr = s''.
    382   #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'
     350  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' >s_refl <s_refl'
    383351  whd in match get_8051_sfr; normalize nodelta
    384352  @get_index_v_status_of_pseudo_status %
     
    387355lemma get_8052_sfr_status_of_pseudo_status:
    388356  ∀M, code_memory, sigma, policy, s, s', sfr.
    389   status_of_pseudo_status M code_memory s sigma policy = s'
     357  s' = status_of_pseudo_status M code_memory s sigma policy
    390358  (get_8052_sfr (BitVectorTrie Byte 16)
    391359    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    392360    s' sfr =
    393361   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
    394   #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl //
     362  #M #code_memory #sigma #policy #s #s' #sfr #s_refl >s_refl //
    395363qed.
    396364
    397365lemma set_8052_sfr_status_of_pseudo_status:
    398366  ∀M, code_memory, sigma, policy, s, s', sfr, v.
    399   status_of_pseudo_status M code_memory s sigma policy = s'
     367  s' = status_of_pseudo_status M code_memory s sigma policy
    400368    (set_8052_sfr (BitVectorTrie Byte 16)
    401369      (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
    402370    status_of_pseudo_status M code_memory
    403371     (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
    404   #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl //
     372  #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl >s_refl //
    405373qed.
    406374 
     
    429397        ∀s'.
    430398        ∀v'.
    431           status_of_pseudo_status M code_memory s sigma policy = s'
     399          s' = status_of_pseudo_status M code_memory s sigma policy
    432400            map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
    433401              (set_bit_addressable_sfr (BitVectorTrie Byte 16)
     
    457425         | _ ⇒ set_8051_sfr ?? s sfr v ]
    458426      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
    459   normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl
     427  normalize nodelta #M #sigma #policy #s' #v' #s_refl >s_refl
    460428  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
    461429  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
     
    466434 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
    467435  ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
    468   status_of_pseudo_status M code_memory s sigma policy = s'
     436  s' = status_of_pseudo_status M code_memory s sigma policy
    469437  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
    470438 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
     
    479447lemma set_low_internal_ram_status_of_pseudo_status:
    480448 ∀cm,sigma,policy,M,s,s',ram.
    481   status_of_pseudo_status M cm s sigma policy = s'
     449  s' = status_of_pseudo_status M cm s sigma policy
    482450  set_low_internal_ram (BitVectorTrie Byte 16)
    483451  (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    486454  = status_of_pseudo_status M cm
    487455    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
    488   #cm #sigma #policy #M #s #s' #ram #s_refl <s_refl //
     456  #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl //
    489457qed.
    490458
     
    607575lemma set_register_status_of_pseudo_status:
    608576 ∀M,sigma,policy,cm,s,s',r,v,v'.
    609   status_of_pseudo_status M cm s sigma policy = s'
     577  s' = status_of_pseudo_status M cm s sigma policy
    610578  map_internal_ram_address_using_pseudo_address_map M sigma
    611579   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
     
    615583  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
    616584    sigma policy.
    617   #M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok
     585  #M #sigma #policy #cm #s #s' #r #v #v' #s_refl >s_refl #v_ok
    618586 whd in match set_register; normalize nodelta
    619587 >bit_address_of_register_status_of_pseudo_status
     
    691659  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    692660  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
    693    status_of_pseudo_status M cm ps sigma policy = s'
     661   s' = status_of_pseudo_status M cm ps sigma policy
    694662   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    695663   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     
    747715          match other in False with [ ]
    748716      ] (subaddressing_modein … a)) normalize nodelta
    749   #M #sigma #policy #s' #v' #s_refl <s_refl
     717  #M #sigma #policy #s' #v' #s_refl >s_refl
    750718  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
    751719  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
     
    784752  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
    785753   addr = addr' →
    786    status_of_pseudo_status M cm ps sigma policy = s'
     754   s' = status_of_pseudo_status M cm ps sigma policy
    787755   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    788756   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     
    804772    ∀s: PreStatus … code_memory.
    805773    ∀s'.
    806     (status_of_pseudo_status M code_memory s sigma policy) = s'
     774    s' = status_of_pseudo_status M code_memory s sigma policy
    807775    (p1_latch (BitVectorTrie Byte 16)
    808776      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    809777      s' =
    810778    (p1_latch pseudo_assembly_program code_memory s)).
    811   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
     779  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
    812780qed.
    813781
     
    819787    ∀s: PreStatus … code_memory.
    820788    ∀s'.
    821     (status_of_pseudo_status M code_memory s sigma policy) = s'
     789    s' = status_of_pseudo_status M code_memory s sigma policy
    822790    (p3_latch (BitVectorTrie Byte 16)
    823791      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    824792      (status_of_pseudo_status M code_memory s sigma policy) =
    825793    (p3_latch pseudo_assembly_program code_memory s)).
    826   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
     794  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
    827795qed.
    828796
     
    834802    ∀l: bool.
    835803      Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
    836         status_of_pseudo_status M code_memory s sigma policy = s'
     804        s' = status_of_pseudo_status M code_memory s sigma policy
    837805        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    838806          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    869837    ]
    870838    ])
    871   #M #sigma #policy #s' #s_refl <s_refl normalize nodelta
     839  #M #sigma #policy #s' #s_refl >s_refl normalize nodelta
    872840  /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
    873841qed.
     
    882850      map_address_Byte_using_internal_pseudo_address_map M sigma
    883851         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
    884       (status_of_pseudo_status M code_memory s sigma policy) = s'
     852      s' = status_of_pseudo_status M code_memory s sigma policy
    885853        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    886854          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    888856 #code #s #d #v
    889857 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
    890  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %
     858 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl >s_refl' @relevant %
    891859qed.
    892860
     
    898866    ∀s''.
    899867    sigma (program_counter … s) = s'' →
    900     (status_of_pseudo_status M code_memory s sigma policy) = s'
     868    s' = status_of_pseudo_status M code_memory s sigma policy
    901869      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    902870        s' = s''.
    903   #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //
     871  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl >s_refl' //
    904872qed.
    905873
    906874lemma get_cy_flag_status_of_pseudo_status:
    907875  ∀M, cm, sigma, policy, s, s'.
    908   (status_of_pseudo_status M cm s sigma policy) = s'
     876  s' = status_of_pseudo_status M cm s sigma policy
    909877  (get_cy_flag (BitVectorTrie Byte 16)
    910878    (code_memory_of_pseudo_assembly_program cm sigma policy)
    911879    s' =
    912880  get_cy_flag pseudo_assembly_program cm s).
    913   #M #cm #sigma #policy #s #s' #s_refl <s_refl
     881  #M #cm #sigma #policy #s #s' #s_refl >s_refl
    914882  whd in match get_cy_flag; normalize nodelta
    915883  >(get_index_v_status_of_pseudo_status … (refl …)) %
     
    922890  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
    923891    Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
    924       (status_of_pseudo_status M cm ps sigma policy) = s'
     892      s' = status_of_pseudo_status M cm ps sigma policy
    925893      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    926894      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    972940        match other in False with [ ]
    973941      ] (subaddressing_modein … a)) normalize nodelta
    974   #M #sigma #policy #s' #s_refl <s_refl
     942  #M #sigma #policy #s' #s_refl >s_refl
    975943  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
    976944  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
     
    1023991  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
    1024992  ∀M. ∀sigma. ∀policy. ∀s', s''.
    1025       (status_of_pseudo_status M cm ps sigma policy) = s'
     993      s' = status_of_pseudo_status M cm ps sigma policy
    1026994      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
    1027995      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     
    10391007  ∀addr: [[data16]].
    10401008  ∀M. ∀sigma. ∀policy. ∀s'.
    1041     status_of_pseudo_status M cm ps sigma policy = s'
     1009    s' = status_of_pseudo_status M cm ps sigma policy
    10421010      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    10431011      s' addr =
     
    10521020  ∀v,v': Word.
    10531021  ∀M. ∀sigma. ∀policy. ∀s'.
    1054     status_of_pseudo_status M cm ps sigma policy = s'
     1022    s' = status_of_pseudo_status M cm ps sigma policy
    10551023    v=v' → addr=addr' →
    10561024      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    10571025      s' v' addr' =
    10581026      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
    1059   #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl
     1027  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl >s_refl #addr_refl
    10601028  <addr_refl #v_refl <v_refl
    10611029  @(subaddressing_mode_elim … addr)
     
    10631031  whd in match set_arg_16'; normalize nodelta
    10641032  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
    1065   @set_8051_sfr_status_of_pseudo_status try % @sym_eq
     1033  @set_8051_sfr_status_of_pseudo_status try %
    10661034  @set_8051_sfr_status_of_pseudo_status %
    10671035qed.
     
    11061074  ∀l.
    11071075    Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
    1108       status_of_pseudo_status M cm ps sigma policy = s'
     1076      s' = status_of_pseudo_status M cm ps sigma policy
    11091077      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    11101078      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    11521120      ] (subaddressing_modein … a)) normalize nodelta
    11531121  [4,5,8,9: //]
    1154   #M #sigma #policy #s' #s_refl <s_refl
     1122  #M #sigma #policy #s' #s_refl >s_refl
    11551123  [1:
    11561124    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
     
    11751143  ∀M. ∀sigma. ∀policy. ∀s'.
    11761144    addr = addr' →
    1177     status_of_pseudo_status M cm ps sigma policy = s'
     1145    s' = status_of_pseudo_status M cm ps sigma policy
    11781146      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    11791147      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    13451313lemma clock_status_of_pseudo_status:
    13461314 ∀M,cm,sigma,policy,s,s'.
    1347   (status_of_pseudo_status M cm s sigma policy) = s'
     1315  s' = status_of_pseudo_status M cm s sigma policy
    13481316  clock …
    13491317   (code_memory_of_pseudo_assembly_program cm sigma policy)
    13501318   s'
    13511319  = clock … cm s.
    1352   #M #cm #sigma #policy #s #s' #s_refl <s_refl //
     1320  #M #cm #sigma #policy #s #s' #s_refl >s_refl //
    13531321qed.
    13541322
    13551323lemma set_clock_status_of_pseudo_status:
    13561324 ∀M,cm,sigma,policy,s,s',v,v'.
    1357  status_of_pseudo_status M cm s sigma policy = s'
     1325 s' = status_of_pseudo_status M cm s sigma policy
    13581326 v = v' →
    13591327  set_clock …
     
    13611329   s' v
    13621330  = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
    1363   #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
    1364 qed.
    1365 
    1366 (*CSC: daemon
     1331  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl >s_refl <v_refl //
     1332qed.
     1333
    13671334lemma set_flags_status_of_pseudo_status:
    13681335  ∀M.
     
    13781345    opt = opt' →
    13791346    c = c' →
    1380     status_of_pseudo_status M code_memory s sigma policy = s'
     1347    s' = status_of_pseudo_status M code_memory s sigma policy
    13811348      set_flags … s' b opt c =
    13821349        status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
    1383   #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
    1384   #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl
    1385   whd in match status_of_pseudo_status; normalize nodelta
    1386   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    1387   cases (\snd M)
    1388   [1:
    1389     normalize nodelta %
    1390   |2: ** #address normalize nodelta
    1391     @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    1392     whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
    1393     @split_eq_status try % whd in match (sfr_8051_index ?);
    1394     cases daemon
    1395   ]
    1396 qed.*)
     1350  ** #low #high #accA #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
     1351  #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl >s_refl
     1352  whd in match set_flags; normalize nodelta
     1353  @set_8051_sfr_status_of_pseudo_status try %
     1354  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
     1355  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1356  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 
     1357  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1358  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1359  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1360  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 
     1361  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1362  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1363  %
     1364qed.
    13971365
    13981366lemma get_ac_flag_status_of_pseudo_status:
     
    14031371  ∀s: PreStatus ? code_memory.
    14041372  ∀s'.
    1405     status_of_pseudo_status M code_memory s sigma policy = s'
     1373    s' = status_of_pseudo_status M code_memory s sigma policy
    14061374      get_ac_flag ?? s' = get_ac_flag ? code_memory s.
    1407   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     1375  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
    14081376  whd in match get_ac_flag; normalize nodelta
    14091377  whd in match status_of_pseudo_status; normalize nodelta
     
    14231391  ∀s: PreStatus ? code_memory.
    14241392  ∀s'.
    1425     status_of_pseudo_status M code_memory s sigma policy = s'
     1393    s' = status_of_pseudo_status M code_memory s sigma policy
    14261394      get_ov_flag ?? s' = get_ov_flag ? code_memory s.
    1427   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     1395  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
    14281396  whd in match get_ov_flag; normalize nodelta
    14291397  whd in match status_of_pseudo_status; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.