Ignore:
Timestamp:
Jul 6, 2012, 5:26:21 PM (8 years ago)
Author:
mulligan
Message:

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2143 r2160  
    360360  ∀sigma: Word → Word.
    361361  ∀policy: Word → bool.
    362     \snd M = (None …)
     362    \snd M = data
    363363      special_function_registers_8051 pseudo_assembly_program cm s =
    364364        special_function_registers_8051 (BitVectorTrie Byte 16)
     
    372372qed.
    373373
    374 lemma special_function_registers_8051_set_program_counter:
    375   ∀cm: pseudo_assembly_program.
    376   ∀ps: PreStatus pseudo_assembly_program cm.
    377   ∀v: Word.
    378   special_function_registers_8051 pseudo_assembly_program cm
    379    (set_program_counter pseudo_assembly_program cm ps v) =
    380      special_function_registers_8051 pseudo_assembly_program cm ps.
    381   #cm #ps #v %
    382 qed.
    383 
    384 (*
    385 lemma get_arg_8_status_of_pseudo_status:
     374lemma n_lt_19_elim_prop:
     375  ∀P: nat → Prop.
     376    P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 →
     377    P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 →
     378      (∀n. n < 19 → P n).
     379  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
     380  #H15 #H16 #H17 #H18 #H19 #n
     381  cases n [1: // ]
     382  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     383  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     384  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     385  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     386  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     387  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     388  #n' normalize in ⊢ (% → ?);
     389  #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd)
     390  cases (lt_to_not_zero … absurd)
     391qed.
     392
     393lemma get_index_v_set_index_miss:
     394  ∀T: Type[0].
     395  ∀n, i, j: nat.
     396  ∀v: Vector T n.
     397  ∀b: T.
     398  ∀i_proof: i < n.
     399  ∀j_proof: j < n.
     400  i ≠ j →
     401    get_index_v T n (set_index T n v i b i_proof) j j_proof =
     402      get_index_v T n v j j_proof.
     403  #T #n #i #j #v lapply i lapply j elim v #i #j
     404  [1:
     405    #b #i_proof
     406    cases (lt_to_not_zero … i_proof)
     407  |2:
     408    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
     409    lapply i_proof lapply i_neq_j cases i'
     410    [1:
     411      -i_neq_j #i_neq_j -i_proof #i_proof
     412      whd in match (set_index ??????);
     413      lapply j_proof lapply i_neq_j cases j'
     414      [1:
     415        #relevant @⊥ cases relevant -relevant #absurd @absurd %
     416      |2:
     417        #j' #_ -j_proof #j_proof %
     418      ]
     419    |2:
     420      #i' -i_neq_j #i_neq_j -i_proof #i_proof
     421      lapply j_proof lapply i_neq_j cases j'
     422      [1:
     423        #_ #j_proof %
     424      |2:
     425        #j' #i_neq_j #j_proof
     426        @inductive_hypothesis @nmk #relevant
     427        cases i_neq_j #absurd @absurd >relevant %
     428      ]
     429    ]
     430  ]
     431qed.
     432
     433lemma get_index_v_special_function_registers_8051_not_acc_a:
    386434  ∀M: internal_pseudo_address_map.
    387435  ∀cm: pseudo_assembly_program.
    388   ∀ps.
     436  ∀s: PreStatus pseudo_assembly_program cm.
    389437  ∀sigma: Word → Word.
    390438  ∀policy: Word → bool.
    391   ∀b: bool.
    392   ∀addr1: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect_dptr]].
    393     get_arg_8 (BitVectorTrie Byte 16)
    394      (code_memory_of_pseudo_assembly_program cm sigma policy)
    395      (status_of_pseudo_status M cm ps sigma policy) b addr1 =
    396     get_arg_8 pseudo_assembly_program cm ps b addr1.
    397   [2,3:
    398     @(subaddressing_mode_elim … addr1) try #w @I
     439  ∀n: nat.
     440  ∀proof: n < 19.
     441    n ≠ 17 →
     442   (get_index_v Byte 19
     443    (special_function_registers_8051 pseudo_assembly_program cm s) n
     444    proof =
     445   get_index_v Byte 19
     446     (special_function_registers_8051 (BitVectorTrie Byte 16)
     447       (code_memory_of_pseudo_assembly_program cm sigma policy)
     448       (status_of_pseudo_status M cm s sigma policy)) n
     449       proof).
     450  #M #cm #s #sigma #policy #n #proof lapply proof
     451  @(n_lt_19_elim_prop … proof) -proof #proof
     452  [18:
     453    #absurd @⊥ cases absurd -absurd #absurd @absurd %
    399454  ]
    400   #M #cm #ps #sigma #policy #b #addr1
    401   @(subaddressing_mode_elim … addr1)
    402   try #w
    403   [1:
    404     whd in ⊢ (??%%);
    405     @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    406     @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    407     cases (get_index_v bool ????) normalize nodelta try %
    408     cases daemon (* XXX: require axioms from Assembly.ma *)
    409   |2:
    410     whd in ⊢ (??%%);
    411     @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    412     lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
    413     @(pair_replace ?????????? nu_nl_refl) [1: cases daemon (* XXX: !! *) ]
    414     @pair_elim #bit_one_v #three_bits #bit_one_v_three_bits_refl normalize nodelta
    415     cases (get_index_v bool ????) normalize nodelta
    416     cases daemon (* XXX: same as above *)
    417   |3:
    418     whd in ⊢ (??%%); @(bitvector_3_elim_prop … w)
    419     whd in match bit_address_of_register; normalize nodelta
    420     @pair_elim #un #ln #un_ln_refl
    421     cases (¬get_index_v bool ???? ∧ ¬get_index_v bool ????) normalize nodelta
    422     [1,3,5,7,9,11,13,15:
    423       cases daemon (* XXX: same as above *)
    424     |*:
    425       cases (¬get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
    426       [1,3,5,7,9,11,13,15:
    427         cases daemon (* XXX: same as above *)
    428       |*:
    429         cases (get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
    430         cases daemon (* XXX: same as above *)
    431       ]
    432     ]
    433   |4,5:
    434     whd in ⊢ (??%%); <status_of_pseudo_status_does_not_change_8051_sfrs %
    435   |6,7,8:
    436     %
    437   ]
    438 qed.
    439 *)
    440 
    441 (*
    442 lemma pi1_let_commute:
    443  ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
    444  pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
    445  #A #B #C #P * #a #b * //
    446 qed.
    447 
    448 lemma pi1_let_as_commute:
    449  ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
    450  pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
    451   (let 〈x1,y1〉 as H ≝ c in pi1 … t).
    452  #A #B #C #P * #a #b * //
    453 qed.
    454 
    455 lemma tech_pi1_let_as_commute:
    456  ∀A,B,C,P. ∀f. ∀c,c':A × B.
    457  ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
    458  ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
    459   c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
    460   pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
    461    f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
    462  #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
    463 qed.
    464 *)
     455  #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     456  whd in match status_of_pseudo_status; normalize nodelta
     457  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     458  cases M #left #right cases right normalize nodelta try %
     459  -right * #address
     460  @pair_elim #high #low #high_low_refl normalize nodelta
     461  whd in match sfr_8051_index; normalize nodelta
     462  >get_index_v_set_index_miss try %
     463  #absurd destruct(absurd)
     464qed.
    465465
    466466include alias "arithmetics/nat.ma".
     
    477477  #fetch_many_assm whd in fetch_many_assm;
    478478  cases (eq_bv_eq … fetch_many_assm) assumption
     479qed.
     480
     481(* XXX: this needs an extra invariant relating address and word that we look
     482        up!
     483*)
     484definition map_lower_internal_ram_address_using_pseudo_address_map:
     485    ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
     486  λM: internal_pseudo_address_map.
     487  λsigma: Word → Word.
     488  λaddress: Byte.
     489  λvalue: Byte.
     490  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
     491  [ None ⇒ value
     492  | Some upper_lower_word ⇒
     493    let 〈upper_lower, word〉 ≝ upper_lower_word in
     494    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
     495      if eq_upper_lower upper_lower upper then
     496        high
     497      else
     498        low
     499  ].
     500
     501lemma get_8051_sfr_status_of_pseudo_status:
     502  ∀M.
     503  ∀cm, ps, sigma, policy.
     504  ∀sfr.
     505    (sfr = SFR_ACC_A → \snd M = data) →
     506    get_8051_sfr (BitVectorTrie Byte 16)
     507      (code_memory_of_pseudo_assembly_program cm sigma policy)
     508      (status_of_pseudo_status M cm ps sigma policy) sfr =
     509    get_8051_sfr pseudo_assembly_program cm ps sfr.
     510  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
     511  [18:
     512     >relevant %
     513  ]
     514  cases sndM try % * #address
     515  whd in match get_8051_sfr;
     516  whd in match status_of_pseudo_status; normalize nodelta
     517  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     518  @pair_elim #upper #lower #upper_lower_refl
     519  @get_index_v_set_index_miss @nmk #relevant
     520  normalize in relevant; destruct(relevant)
     521qed.
     522
     523lemma bitvector_cases_hd_tl:
     524  ∀n: nat.
     525  ∀w: BitVector (S n).
     526   ∃hd: bool. ∃tl: BitVector n.
     527    w ≃ hd:::tl.
     528  #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant
     529qed.
     530
     531lemma external_ram_set_bit_addressable_sfr:
     532  ∀M: Type[0].
     533  ∀cm: M.
     534  ∀ps.
     535  ∀w.
     536  ∀result: Byte.
     537    external_ram M cm
     538      (set_bit_addressable_sfr M cm ps w result) =
     539    external_ram M cm ps.
     540  #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma!
     541  whd in match set_bit_addressable_sfr; normalize nodelta
     542  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     543  cases (eqb ??) normalize nodelta [1: % ]
     544  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     545  cases (eqb ??) normalize nodelta [1: % ]
     546  cases (eqb ??) normalize nodelta [1: % ]
     547  cases (eqb ??) normalize nodelta [1: % ]
     548  cases (eqb ??) normalize nodelta [1: % ]
     549  cases (eqb ??) normalize nodelta [1: % ]
     550  cases (eqb ??) normalize nodelta [1: % ]
     551  cases (eqb ??) normalize nodelta [1: % ]
     552  cases (eqb ??) normalize nodelta [1: % ]
     553  cases (eqb ??) normalize nodelta [1: % ]
     554  cases (eqb ??) normalize nodelta [1: % ]
     555  cases (eqb ??) normalize nodelta [1: % ]
     556  cases (eqb ??) normalize nodelta [1: % ]
     557  cases (eqb ??) normalize nodelta [1: % ]
     558  cases (eqb ??) normalize nodelta [1: % ]
     559  cases (eqb ??) normalize nodelta [1: % ]
     560  cases (eqb ??) normalize nodelta [1: % ]
     561  cases (eqb ??) normalize nodelta [1: % ]
     562  cases (eqb ??) normalize nodelta [1: % ]
     563  cases (eqb ??) normalize nodelta [1: % ]
     564  cases (eqb ??) normalize nodelta [1: % ]
     565  cases (eqb ??) normalize nodelta [1: % ]
     566  cases (eqb ??) normalize nodelta [1: % ]
     567  cases (eqb ??) normalize nodelta [1: % ]
     568  cases not_implemented *)
     569qed.
     570
     571lemma external_ram_set_arg_8:
     572  ∀M: Type[0].
     573  ∀cm: M.
     574  ∀ps.
     575  ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]].
     576  ∀result.
     577    external_ram M cm (set_arg_8 M cm ps addr1 result) =
     578      external_ram M cm ps.
     579  [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     580  #M #cm #ps #addr1 #result
     581  @(subaddressing_mode_elim … addr1) try #w try %
     582  whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
     583  [1:
     584    cases (vsplit bool ???) #nu #nl normalize nodelta
     585    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
     586    cases (get_index_v bool ????) normalize nodelta try %
     587    @external_ram_set_bit_addressable_sfr
     588  |2:
     589    cases (vsplit bool ???) #nu #nl normalize nodelta
     590    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
     591    cases (get_index_v bool ????) normalize nodelta %
     592  ]
     593qed.
     594
     595lemma special_function_registers_8051_set_clock:
     596  ∀M: Type[0].
     597  ∀cm: M.
     598  ∀ps.
     599  ∀t.
     600    special_function_registers_8051 M cm (set_clock M cm ps t) =
     601      special_function_registers_8051 M cm ps.
     602  //
     603qed.
     604
     605lemma get_arg_8_pseudo_addressing_mode_ok:
     606  ∀M: internal_pseudo_address_map.
     607  ∀cm: pseudo_assembly_program.
     608  ∀ps: PreStatus pseudo_assembly_program cm.
     609  ∀sigma: Word → Word.
     610  ∀policy: Word → bool.
     611  ∀addr1: [[registr; direct]].
     612    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
     613      get_arg_8 (BitVectorTrie Byte 16)
     614        (code_memory_of_pseudo_assembly_program cm sigma policy)
     615        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
     616      get_arg_8 pseudo_assembly_program cm ps true addr1.
     617  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     618  #M #cm #ps #sigma #policy #addr1
     619  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
     620  [1:
     621    whd in ⊢ (??%? → ??%?);
     622    whd in match bit_address_of_register; normalize nodelta
     623    @pair_elim #un #ln #un_ln_refl
     624    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
     625    @(pair_replace ?????????? un_ln_refl)
     626    [1:
     627      whd in match get_8051_sfr; normalize nodelta
     628      whd in match sfr_8051_index; normalize nodelta
     629      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
     630      try % #absurd destruct(absurd)
     631    |2:
     632      #assembly_mode_ok_refl
     633      >low_internal_ram_of_pseudo_internal_ram_miss
     634      [1:
     635        %
     636      |2:
     637        cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta
     638        #absurd try % @sym_eq assumption
     639      ]
     640    ]
     641  |2:
     642    #addressing_mode_ok_refl whd in ⊢ (??%?);
     643    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     644    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
     645    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
     646    [1:
     647      whd in ⊢ (??%%); normalize nodelta
     648      cases (eqb ??) normalize nodelta [1: % ]
     649      cases (eqb ??) normalize nodelta [1: % ]
     650      cases (eqb ??) normalize nodelta [1: % ]
     651      cases (eqb ??) normalize nodelta [1: % ]
     652      cases (eqb ??) normalize nodelta [1:
     653        @get_8051_sfr_status_of_pseudo_status
     654        #absurd destruct(absurd)
     655      ]
     656      cases (eqb ??) normalize nodelta [1:
     657        @get_8051_sfr_status_of_pseudo_status
     658        #absurd destruct(absurd)
     659      ]
     660      cases (eqb ??) normalize nodelta [1:
     661        @get_8051_sfr_status_of_pseudo_status
     662        #absurd destruct(absurd)
     663      ]
     664      cases (eqb ??) normalize nodelta [1:
     665        @get_8051_sfr_status_of_pseudo_status
     666        #absurd destruct(absurd)
     667      ]
     668      cases (eqb ??) normalize nodelta [1:
     669        @get_8051_sfr_status_of_pseudo_status
     670        #absurd destruct(absurd)
     671      ]
     672      cases (eqb ??) normalize nodelta [1: % ]
     673      cases (eqb ??) normalize nodelta [1: % ]
     674      cases (eqb ??) normalize nodelta [1: % ]
     675      cases (eqb ??) normalize nodelta [1: % ]
     676      cases (eqb ??) normalize nodelta [1: % ]
     677      cases (eqb ??) normalize nodelta [1:
     678        @get_8051_sfr_status_of_pseudo_status
     679        #absurd destruct(absurd)
     680      ]
     681      cases (eqb ??) normalize nodelta [1:
     682        @get_8051_sfr_status_of_pseudo_status
     683        #absurd destruct(absurd)
     684      ]
     685      cases (eqb ??) normalize nodelta [1:
     686        @get_8051_sfr_status_of_pseudo_status
     687        #absurd destruct(absurd)
     688      ]
     689      cases (eqb ??) normalize nodelta [1:
     690        @get_8051_sfr_status_of_pseudo_status
     691        #absurd destruct(absurd)
     692      ]
     693      cases (eqb ??) normalize nodelta [1:
     694        @get_8051_sfr_status_of_pseudo_status
     695        #absurd destruct(absurd)
     696      ]
     697      cases (eqb ??) normalize nodelta [1:
     698        @get_8051_sfr_status_of_pseudo_status
     699        #absurd destruct(absurd)
     700      ]
     701      cases (eqb ??) normalize nodelta [1:
     702        @get_8051_sfr_status_of_pseudo_status
     703        #absurd destruct(absurd)
     704      ]
     705      cases (eqb ??) normalize nodelta [1:
     706        @get_8051_sfr_status_of_pseudo_status
     707        #absurd destruct(absurd)
     708      ]
     709      cases (eqb ??) normalize nodelta [1:
     710        @get_8051_sfr_status_of_pseudo_status
     711        #absurd destruct(absurd)
     712      ]
     713      cases (eqb ??) normalize nodelta [1:
     714        @get_8051_sfr_status_of_pseudo_status
     715        #absurd destruct(absurd)
     716      ]
     717      inversion (eqb ??) #eqb_refl normalize nodelta [1:
     718        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
     719        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
     720        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
     721        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
     722        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
     723      ]
     724      cases (eqb ??) normalize nodelta [1:
     725        @get_8051_sfr_status_of_pseudo_status
     726        #absurd destruct(absurd)
     727      ] %
     728    |2:
     729      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
     730      whd in match status_of_pseudo_status; normalize nodelta
     731      >low_internal_ram_of_pseudo_internal_ram_miss try %
     732      cut(arg = false:::(three_bits@@nl))
     733      [1:
     734        <get_index_v_refl
     735        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
     736        [1:
     737          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
     738          [1:
     739            @le_S_S @le_O_n
     740          |2:
     741            cut(ignore = \fst (vsplit bool 1 3 nu))
     742            [1:
     743              >ignore_three_bits_refl %
     744            |2:
     745              #ignore_refl >ignore_refl
     746              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
     747              >nu_refl %
     748            ]
     749          |3:
     750            #ignore_refl >ignore_refl in ignore_three_bits_refl;
     751            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
     752            #nu_refl <nu_refl %
     753          ]
     754        |2:
     755          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
     756          @sym_eq @vsplit_ok >nu_nl_refl %
     757        ]
     758      |2:
     759        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
     760        normalize nodelta
     761        [1:
     762          cases (eq_bv ???) normalize #absurd destruct(absurd)
     763        |2:
     764          #_ %
     765        ]
     766      ]
     767    ]
     768  ]
     769qed.
     770
     771lemma special_function_registers_8051_set_program_counter:
     772  ∀M: Type[0].
     773  ∀cm: M.
     774  ∀ps.
     775  ∀pc: Word.
     776    special_function_registers_8051 M cm (set_program_counter M cm ps pc) =
     777      special_function_registers_8051 M cm ps.
     778  //
     779qed.
     780
     781lemma special_function_registers_8052_set_program_counter:
     782  ∀M: Type[0].
     783  ∀cm: M.
     784  ∀ps.
     785  ∀pc: Word.
     786    special_function_registers_8052 M cm (set_program_counter M cm ps pc) =
     787      special_function_registers_8052 M cm ps.
     788  //
     789qed.
     790
     791lemma set_index_set_index_commutation:
     792  ∀A: Type[0].
     793  ∀n: nat.
     794  ∀v: Vector A n.
     795  ∀m, o: nat.
     796  ∀m_lt_proof: m < n.
     797  ∀o_lt_proof: o < n.
     798  ∀e, f: A.
     799    m ≠ o →
     800      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
     801        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
     802  #A #n #v elim v
     803  [1:
     804    #m #o #m_lt_proof
     805    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
     806  |2:
     807    #n' #hd #tl #inductive_hypothesis
     808    #m #o
     809    cases m cases o
     810    [1:
     811      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
     812      @relevant %
     813    |2,3:
     814      #o' normalize //
     815    |4:
     816      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
     817      normalize @eq_f @inductive_hypothesis @nmk #relevant
     818      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
     819    ]
     820  ]
     821qed.
     822
     823lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
     824  ∀M: internal_pseudo_address_map.
     825  ∀cm: pseudo_assembly_program.
     826  ∀ps.
     827  ∀sigma: Word → Word.
     828  ∀policy: Word → bool.
     829  ∀sfr.
     830  ∀result: Byte.
     831    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
     832      special_function_registers_8051 (BitVectorTrie Byte 16)
     833        (code_memory_of_pseudo_assembly_program cm sigma policy)
     834        (set_8051_sfr (BitVectorTrie Byte 16)
     835        (code_memory_of_pseudo_assembly_program cm sigma policy)
     836        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
     837      sfr_8051_of_pseudo_sfr_8051 M
     838        (special_function_registers_8051 pseudo_assembly_program cm
     839        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
     840  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
     841  whd in match (set_8051_sfr ?????);
     842  cases M #callM * try % #upper_lower #address
     843  whd in match (special_function_registers_8051 ???);
     844  whd in match (sfr_8051_of_pseudo_sfr_8051 ???);
     845  @pair_elim #high #low #high_low_refl normalize nodelta
     846  cases (eq_upper_lower ??) normalize nodelta
     847  whd in match (set_8051_sfr ?????);
     848  @set_index_set_index_commutation @nmk #relevant
     849  @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))
     850qed.
     851
     852lemma special_function_registers_8051_set_arg_8:
     853  ∀M: internal_pseudo_address_map.
     854  ∀cm: pseudo_assembly_program.
     855  ∀ps.
     856  ∀sigma: Word → Word.
     857  ∀policy: Word → bool.
     858  ∀addr1: [[ registr; direct ]].
     859  ∀result.
     860    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
     861    special_function_registers_8051 (BitVectorTrie Byte 16)
     862      (code_memory_of_pseudo_assembly_program cm sigma policy)
     863      (set_arg_8 (BitVectorTrie Byte 16)
     864        (code_memory_of_pseudo_assembly_program cm sigma policy)
     865        (status_of_pseudo_status M cm ps sigma policy) addr1 result) =
     866   sfr_8051_of_pseudo_sfr_8051 M
     867     (special_function_registers_8051 pseudo_assembly_program cm
     868     (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.
     869  cases daemon
     870(*
     871  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     872  #M #cm #ps #sigma #policy #addr1 #result
     873  @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %
     874  whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?);
     875  whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));
     876  cases (vsplit bool ???) #nu #nl normalize nodelta
     877  cases (vsplit bool ???) #ignore #three_bits normalize nodelta
     878  cases (get_index_v bool ????) normalize nodelta try %
     879  whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);
     880  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     881  cases (eqb ??) normalize nodelta [1: % ]
     882  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     883  cases (eqb ??) normalize nodelta [1: % ]
     884  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     885  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     886  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     887  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     888  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     889  cases (eqb ??) normalize nodelta [1: % ]
     890  cases (eqb ??) normalize nodelta [1: % ]
     891  cases (eqb ??) normalize nodelta [1: % ]
     892  cases (eqb ??) normalize nodelta [1: % ]
     893  cases (eqb ??) normalize nodelta [1: % ]
     894  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     895  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     896  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     897  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     898  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     899  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     900  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     901  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     902  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     903  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     904  inversion (eqb ??) #eqb_refl normalize nodelta [1:
     905    whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;
     906    >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
     907    #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm
     908    whd in match (status_of_pseudo_status ?????);
     909    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     910    >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %
     911  ]
     912  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     913  cases not_implemented *)
    479914qed.
    480915
     
    507942  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
    508943  ∀ticks: nat × nat.
    509   ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
     944  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_datalabels sigma policy ppc (Instruction instr).
    510945  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
    511946  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
     
    9331368                  s
    9341369           ] (refl … instr))
    935   try (cases(other))
     1370  try cases other
    9361371  try assumption (*20s*)
    9371372  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
     
    9551390  [1,3:
    9561391    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    957     whd in ⊢ (??%?);
    9581392    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    9591393    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
     1394    whd in ⊢ (??%?);
    9601395    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1396    lapply maps_assm whd in ⊢ (??%? → ?);
     1397    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
     1398    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
    9611399    (* XXX: work on the left hand side *)
    9621400    @(pair_replace ?????????? p) normalize nodelta
    9631401    [1,3:
    964       >(get_arg_8_set_program_counter … true addr1) in ⊢ (??%?);
    965       [2,4: (* /2 by _/ *) cases daemon ] @eq_f3 [2,3,5,6: % ]
    966       whd in ⊢ (??%?); @(subaddressing_mode_elim … addr1)
    967       #arg normalize nodelta whd in ⊢ (???%);
    968       [1,3:
    969         whd in match get_register; normalize nodelta
    970         @(bitvector_3_elim_prop … arg)
    971         whd in match bit_address_of_register; normalize nodelta
    972         @pair_elim #un #ln #un_ln_refl
    973         lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
    974         @(pair_replace ?????????? un_ln_refl)
    975         [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
    976           whd in match get_8051_sfr; normalize nodelta
    977           whd in match sfr_8051_index; normalize nodelta
    978           @eq_f <status_of_pseudo_status_does_not_change_8051_sfrs
    979           >EQs
    980           [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
    981             /demod nohyps/ %
    982           |*:
    983             cases daemon
    984           ]
    985         |*:
    986           >low_internal_ram_of_pseudo_internal_ram_miss
    987           cases daemon
    988           (* XXX: require axioms about low_internal_ram_of_pseudo_low_internal_ram *)         
     1402      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
     1403      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1404      >(get_arg_8_set_program_counter … true addr1)
     1405      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1406      @get_arg_8_pseudo_addressing_mode_ok assumption
     1407    |2,4:
     1408      >p1 normalize nodelta >EQs
     1409      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
     1410      >set_program_counter_status_of_pseudo_status
     1411       whd in ⊢ (??%%);
     1412      @split_eq_status
     1413      [1,10:
     1414        whd in ⊢ (??%%); >set_arg_8_set_program_counter
     1415        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1416        >low_internal_ram_set_program_counter
     1417        [1:
     1418          >low_internal_ram_set_program_counter
     1419          (* XXX: ??? *)
     1420        |2:
     1421          >low_internal_ram_set_clock
     1422          (* XXX: ??? *)
    9891423        ]
    990       |2,4:
    991         @pair_elim #nu #nl #nu_nl_refl
    992         lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
    993         @pair_elim #ignore #three_bits #ignore_three_bits_refl
    994         lapply (refl_to_jmrefl ??? ignore_three_bits_refl) -ignore_three_bits_refl #ignore_three_bits_refl
    995         inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
    996         [1,3:
    997           @(pair_replace ?????????? ignore_three_bits_refl) try %
    998           >get_index_v_refl normalize nodelta >EQs %
    999         |2,4:
    1000           @(pair_replace ?????????? ignore_three_bits_refl) try %
    1001           >get_index_v_refl normalize nodelta >EQs
    1002           cases daemon
    1003           (* XXX: require axioms about low_internal_ram as above *)
     1424      |2,11:
     1425        whd in ⊢ (??%%); >set_arg_8_set_program_counter
     1426        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1427        >high_internal_ram_set_program_counter
     1428        [1:
     1429          >high_internal_ram_set_program_counter
     1430          (* XXX: ??? *)
     1431        |2:
     1432          >high_internal_ram_set_clock
     1433          (* XXX: ??? *)
    10041434        ]
     1435      |3,12:
     1436        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
     1437        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1438        >(external_ram_set_arg_8 ??? addr1)
     1439        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     1440      |4,13:
     1441        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
     1442        [1:
     1443          >program_counter_set_program_counter
     1444          >set_arg_8_set_program_counter
     1445          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1446          >set_clock_set_program_counter >program_counter_set_program_counter
     1447          change with (add ??? = ?)
     1448          (* XXX: ??? *)
     1449        |2:
     1450          >set_arg_8_set_program_counter
     1451          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1452          >program_counter_set_program_counter
     1453          >set_arg_8_set_program_counter
     1454          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1455          >set_clock_set_program_counter >program_counter_set_program_counter
     1456          >sigma_increment_commutation <EQppc
     1457          whd in match (assembly_1_pseudoinstruction ??????);
     1458          whd in match (expand_pseudo_instruction ??????);
     1459          (* XXX: ??? *)
     1460        ]
     1461      |5,14:
     1462        whd in match (special_function_registers_8051 ???);
     1463        [1:
     1464          >special_function_registers_8051_set_program_counter
     1465          >special_function_registers_8051_set_clock
     1466          >set_arg_8_set_program_counter in ⊢ (???%);
     1467          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1468          >special_function_registers_8051_set_program_counter
     1469          >set_arg_8_set_program_counter
     1470          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1471          >special_function_registers_8051_set_program_counter
     1472          @special_function_registers_8051_set_arg_8 assumption
     1473        |2:
     1474          >special_function_registers_8051_set_clock
     1475          >set_arg_8_set_program_counter
     1476          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1477          >set_arg_8_set_program_counter
     1478          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1479          >special_function_registers_8051_set_program_counter
     1480          >special_function_registers_8051_set_program_counter
     1481          @special_function_registers_8051_set_arg_8 assumption
     1482        ]
     1483      |6,15:
     1484        whd in match (special_function_registers_8052 ???);
     1485        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
     1486        [1:
     1487          >set_arg_8_set_program_counter
     1488          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1489          >set_arg_8_set_program_counter
     1490          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1491          >special_function_registers_8052_set_program_counter
     1492          >special_function_registers_8052_set_program_counter
     1493          @special_function_registers_8052_set_arg_8 assumption
     1494        |2:
     1495          whd in ⊢ (??%%);
     1496          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
     1497        ]
     1498        (* XXX: we need special_function_registers_8052_set_arg_8 *)
     1499      |7,16:
     1500        whd in match (p1_latch ???);
     1501        whd in match (p1_latch ???) in ⊢ (???%);
     1502        (* XXX: we need p1_latch_8052_set_arg_8 *)
     1503      |8,17:
     1504        whd in match (p3_latch ???);
     1505        whd in match (p3_latch ???) in ⊢ (???%);
     1506        (* XXX: we need p3_latch_8052_set_arg_8 *)
     1507      |9:
     1508        >clock_set_clock
     1509        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
     1510        >EQticks <instr_refl @eq_f2
     1511        [1:
     1512          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
     1513        |2:
     1514          (* XXX: we need clock_set_arg_8 *)
     1515        ]
     1516      |18:
    10051517      ]
    10061518    ]
     
    10181530    |7,16,25,34:
    10191531    |8,17,26,35:
    1020       whd in ⊢ (??%%);
     1532      whd in ⊢ (??%%);maps_assm
    10211533     
    10221534    |9,18,27,36:
Note: See TracChangeset for help on using the changeset viewer.