Changeset 2124 for src/ASM


Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (7 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

Location:
src/ASM
Files:
10 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASM.ma

    r2123 r2124  
    2828| ADDR11: Word11 → addressing_mode
    2929| ADDR16: Word → addressing_mode.
     30
     31definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
     32  λa, b: addressing_mode.
     33  match a with
     34  [ DIRECT d ⇒
     35    match b with
     36    [ DIRECT e ⇒ eq_bv ? d e
     37    | _ ⇒ false
     38    ]
     39  | INDIRECT b' ⇒
     40    match b with
     41    [ INDIRECT e ⇒ eq_b b' e
     42    | _ ⇒ false
     43    ]
     44  | EXT_INDIRECT b' ⇒
     45    match b with
     46    [ EXT_INDIRECT e ⇒ eq_b b' e
     47    | _ ⇒ false
     48    ]
     49  | REGISTER bv ⇒
     50    match b with
     51    [ REGISTER bv' ⇒ eq_bv ? bv bv'
     52    | _ ⇒ false
     53    ]
     54  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
     55  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
     56  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
     57  | DATA b' ⇒
     58    match b with
     59    [ DATA e ⇒ eq_bv ? b' e
     60    | _ ⇒ false
     61    ]
     62  | DATA16 w ⇒
     63    match b with
     64    [ DATA16 e ⇒ eq_bv ? w e
     65    | _ ⇒ false
     66    ]
     67  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
     68  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
     69  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     70  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     71  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
     72  | BIT_ADDR b' ⇒
     73    match b with
     74    [ BIT_ADDR e ⇒ eq_bv ? b' e
     75    | _ ⇒ false
     76    ]
     77  | N_BIT_ADDR b' ⇒
     78    match b with
     79    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
     80    | _ ⇒ false
     81    ]
     82  | RELATIVE n ⇒
     83    match b with
     84    [ RELATIVE e ⇒ eq_bv ? n e
     85    | _ ⇒ false
     86    ]
     87  | ADDR11 w ⇒
     88    match b with
     89    [ ADDR11 e ⇒ eq_bv ? w e
     90    | _ ⇒ false
     91    ]
     92  | ADDR16 w ⇒
     93    match b with
     94    [ ADDR16 e ⇒ eq_bv ? w e
     95    | _ ⇒ false
     96    ]
     97  ].
     98
     99lemma eq_addressing_mode_refl:
     100  ∀a. eq_addressing_mode a a = true.
     101  #a
     102  cases a try #arg1 try #arg2
     103  try @eq_bv_refl try @eq_b_refl
     104  try normalize %
     105qed.
    30106
    31107(* dpm: renamed register to registr to avoid clash with brian's types *)
    … …  
    161237  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
    162238     is_a he A ∨ is_in ? tl A ].
     239
     240definition is_in_cons_elim:
     241 ∀len.∀hd,tl.∀m:addressing_mode
     242  .is_in (S len) (hd:::tl) m →
     243    (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
     244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
     245 cases (is_a hd am) in ISIN; /2/
     246qed.
    163247
    164248lemma is_a_to_mem_to_is_in:
    … …  
    425509| NOP: preinstruction A.
    426510
     511definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
     512  λi, j.
     513  match i with
     514  [ ADD arg1 arg2 ⇒
     515    match j with
     516    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     517    | _ ⇒ false
     518    ]
     519  | ADDC arg1 arg2 ⇒
     520    match j with
     521    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     522    | _ ⇒ false
     523    ]
     524  | SUBB arg1 arg2 ⇒
     525    match j with
     526    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     527    | _ ⇒ false
     528    ]
     529  | INC arg ⇒
     530    match j with
     531    [ INC arg' ⇒ eq_addressing_mode arg arg'
     532    | _ ⇒ false
     533    ]
     534  | DEC arg ⇒
     535    match j with
     536    [ DEC arg' ⇒ eq_addressing_mode arg arg'
     537    | _ ⇒ false
     538    ]
     539  | MUL arg1 arg2 ⇒
     540    match j with
     541    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     542    | _ ⇒ false
     543    ]
     544  | DIV arg1 arg2 ⇒
     545    match j with
     546    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     547    | _ ⇒ false
     548    ]
     549  | DA arg ⇒
     550    match j with
     551    [ DA arg' ⇒ eq_addressing_mode arg arg'
     552    | _ ⇒ false
     553    ]
     554  | JC arg ⇒
     555    match j with
     556    [ JC arg' ⇒ eq_addressing_mode arg arg'
     557    | _ ⇒ false
     558    ]
     559  | JNC arg ⇒
     560    match j with
     561    [ JNC arg' ⇒ eq_addressing_mode arg arg'
     562    | _ ⇒ false
     563    ]
     564  | JB arg1 arg2 ⇒
     565    match j with
     566    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     567    | _ ⇒ false
     568    ]
     569  | JNB arg1 arg2 ⇒
     570    match j with
     571    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     572    | _ ⇒ false
     573    ]
     574  | JBC arg1 arg2 ⇒
     575    match j with
     576    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     577    | _ ⇒ false
     578    ]
     579  | JZ arg ⇒
     580    match j with
     581    [ JZ arg' ⇒ eq_addressing_mode arg arg'
     582    | _ ⇒ false
     583    ]
     584  | JNZ arg ⇒
     585    match j with
     586    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
     587    | _ ⇒ false
     588    ]
     589  | CJNE arg1 arg2 ⇒
     590    match j with
     591    [ CJNE arg1' arg2' ⇒
     592      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
     593      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
     594      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     595        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     596    | _ ⇒ false
     597    ]
     598  | DJNZ arg1 arg2 ⇒
     599    match j with
     600    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     601    | _ ⇒ false
     602    ]
     603  | CLR arg ⇒
     604    match j with
     605    [ CLR arg' ⇒ eq_addressing_mode arg arg'
     606    | _ ⇒ false
     607    ]
     608  | CPL arg ⇒
     609    match j with
     610    [ CPL arg' ⇒ eq_addressing_mode arg arg'
     611    | _ ⇒ false
     612    ]
     613  | RL arg ⇒
     614    match j with
     615    [ RL arg' ⇒ eq_addressing_mode arg arg'
     616    | _ ⇒ false
     617    ]
     618  | RLC arg ⇒
     619    match j with
     620    [ RLC arg' ⇒ eq_addressing_mode arg arg'
     621    | _ ⇒ false
     622    ]
     623  | RR arg ⇒
     624    match j with
     625    [ RR arg' ⇒ eq_addressing_mode arg arg'
     626    | _ ⇒ false
     627    ]
     628  | RRC arg ⇒
     629    match j with
     630    [ RRC arg' ⇒ eq_addressing_mode arg arg'
     631    | _ ⇒ false
     632    ]
     633  | SWAP arg ⇒
     634    match j with
     635    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
     636    | _ ⇒ false
     637    ]
     638  | SETB arg ⇒
     639    match j with
     640    [ SETB arg' ⇒ eq_addressing_mode arg arg'
     641    | _ ⇒ false
     642    ]
     643  | PUSH arg ⇒
     644    match j with
     645    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
     646    | _ ⇒ false
     647    ]
     648  | POP arg ⇒
     649    match j with
     650    [ POP arg' ⇒ eq_addressing_mode arg arg'
     651    | _ ⇒ false
     652    ]
     653  | XCH arg1 arg2 ⇒
     654    match j with
     655    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     656    | _ ⇒ false
     657    ]
     658  | XCHD arg1 arg2 ⇒
     659    match j with
     660    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     661    | _ ⇒ false
     662    ]
     663  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
     664  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
     665  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
     666  | MOVX arg ⇒
     667    match j with
     668    [ MOVX arg' ⇒
     669      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
     670      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
     671      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     672        sum_eq arg arg'
     673    | _ ⇒ false
     674    ]
     675  | XRL arg ⇒
     676    match j with
     677    [ XRL arg' ⇒
     678      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
     679      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
     680      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     681        sum_eq arg arg'
     682    | _ ⇒ false
     683    ]
     684  | ORL arg ⇒
     685    match j with
     686    [ ORL arg' ⇒
     687      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
     688      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
     689      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
     690      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
     691      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     692        sum_eq arg arg'
     693    | _ ⇒ false
     694    ]
     695  | ANL arg ⇒
     696    match j with
     697    [ ANL arg' ⇒
     698      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
     699      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
     700      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
     701      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
     702      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     703        sum_eq arg arg'
     704    | _ ⇒ false
     705    ]
     706  | MOV arg ⇒
     707    match j with
     708    [ MOV arg' ⇒
     709      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
     710      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
     711      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
     712      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
     713      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
     714      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
     715      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
     716      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
     717      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
     718      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
     719      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
     720        sum_eq_5 arg arg'
     721    | _ ⇒ false
     722    ]
     723  ].
     724
     725lemma eq_preinstruction_refl:
     726  ∀i.
     727    eq_preinstruction i i = true.
     728  #i cases i try #arg1 try #arg2
     729  try @eq_addressing_mode_refl
     730  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
     731    whd in ⊢ (??%?); try %
     732    >eq_addressing_mode_refl
     733    >eq_addressing_mode_refl %
     734  |13,15:
     735    whd in ⊢ (??%?);
     736    cases arg1
     737    [*:
     738      #arg1_left normalize nodelta
     739      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
     740    ]
     741  |11,12:
     742    whd in ⊢ (??%?);
     743    cases arg1
     744    [1:
     745      #arg1_left normalize nodelta
     746      >(eq_sum_refl …)
     747      [1: % | 2,3: #arg @eq_prod_refl ]
     748      @eq_addressing_mode_refl
     749    |2:
     750      #arg1_left normalize nodelta
     751      @eq_prod_refl [*: @eq_addressing_mode_refl ]
     752    |3:
     753      #arg1_left normalize nodelta
     754      >(eq_sum_refl …)
     755      [1:
     756        %
     757      |2,3:
     758        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
     759      ]
     760    |4:
     761      #arg1_left normalize nodelta
     762      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
     763    ]
     764  |14:
     765    whd in ⊢ (??%?);
     766    cases arg1
     767    [1:
     768      #arg1_left normalize nodelta
     769      @eq_sum_refl
     770      [1:
     771        #arg @eq_sum_refl
     772        [1:
     773          #arg @eq_sum_refl
     774          [1:
     775            #arg @eq_sum_refl
     776            [1:
     777              #arg @eq_prod_refl
     778              [*:
     779                @eq_addressing_mode_refl
     780              ]
     781            |2:
     782              #arg @eq_prod_refl
     783              [*:
     784                #arg @eq_addressing_mode_refl
     785              ]
     786            ]
     787          |2:
     788            #arg @eq_prod_refl
     789            [*:
     790              #arg @eq_addressing_mode_refl
     791            ]
     792          ]
     793        |2:
     794          #arg @eq_prod_refl
     795          [*:
     796            #arg @eq_addressing_mode_refl
     797          ]
     798        ]
     799      |2:
     800        #arg @eq_prod_refl
     801        [*:
     802          #arg @eq_addressing_mode_refl
     803        ]
     804      ]
     805    |2:
     806      #arg1_right normalize nodelta
     807      @eq_prod_refl
     808      [*:
     809        #arg @eq_addressing_mode_refl
     810      ]
     811    ]
     812  |*:
     813    whd in ⊢ (??%?);
     814    cases arg1
     815    [*:
     816      #arg1 >eq_sum_refl
     817      [1,4:
     818        @eq_addressing_mode_refl
     819      |2,3,5,6:
     820        #arg @eq_prod_refl
     821        [*:
     822          #arg @eq_addressing_mode_refl
     823        ]
     824      ]
     825    ]
     826  ]
     827qed.
     828
    427829inductive instruction: Type[0] ≝
    428830  | ACALL: [[addr11]] → instruction
    … …  
    437839coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
    438840  RealInstruction on _p: preinstruction ? to instruction.
     841
     842definition eq_instruction: instruction → instruction → bool ≝
     843  λi, j.
     844  match i with
     845  [ ACALL arg ⇒
     846    match j with
     847    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
     848    | _ ⇒ false
     849    ]
     850  | LCALL arg ⇒
     851    match j with
     852    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
     853    | _ ⇒ false
     854    ]
     855  | AJMP arg ⇒
     856    match j with
     857    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
     858    | _ ⇒ false
     859    ]
     860  | LJMP arg ⇒
     861    match j with
     862    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
     863    | _ ⇒ false
     864    ]
     865  | SJMP arg ⇒
     866    match j with
     867    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
     868    | _ ⇒ false
     869    ]
     870  | JMP arg ⇒
     871    match j with
     872    [ JMP arg' ⇒ eq_addressing_mode arg arg'
     873    | _ ⇒ false
     874    ]
     875  | MOVC arg1 arg2 ⇒
     876    match j with
     877    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     878    | _ ⇒ false
     879    ]
     880  | RealInstruction instr ⇒
     881    match j with
     882    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
     883    | _ ⇒ false
     884    ]
     885  ].
     886 
     887lemma eq_instruction_refl:
     888  ∀i. eq_instruction i i = true.
     889  #i cases i [*: #arg1 ]
     890  try @eq_addressing_mode_refl
     891  try @eq_preinstruction_refl
     892  #arg2 whd in ⊢ (??%?);
     893  >eq_addressing_mode_refl >eq_addressing_mode_refl %
     894qed.
     895
     896lemma eq_instruction_to_eq:
     897  ∀i1, i2: instruction.
     898    eq_instruction i1 i2 = true → i1 ≃ i2.
     899  #i1 #i2
     900  cases i1 cases i2 cases daemon (* easy but tedious
     901  [1,10,19,28,37,46:
     902    #arg1 #arg2
     903    whd in match (eq_instruction ??);
     904    cases arg1 #subaddressing_mode
     905    cases subaddressing_mode
     906    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     907    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     908    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     909    #word11 #irrelevant
     910    cases arg2 #subaddressing_mode
     911    cases subaddressing_mode
     912    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     913    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     914    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     915    #word11' #irrelevant normalize nodelta
     916    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
     917qed.
    439918
    440919inductive pseudo_instruction: Type[0] ≝

  • src/ASM/Arithmetic.ma

    r2111 r2124  
    191191
    192192axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
     193
     194axiom eq_bitvector_of_nat_to_eq:
     195 ∀n,n1,n2.
     196  n1 < 2^n → n2 < 2^n →
     197   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
    193198
    194199lemma nat_of_bitvector_aux_injective:
    … …  
    707712    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
    708713   
     714lemma add_bitvector_of_nat_Sm:
     715  ∀n, m: nat.
     716    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
     717      bitvector_of_nat n (S m).
     718 #n #m @add_bitvector_of_nat_plus
     719qed.
     720
    709721definition sign_bit : ∀n. BitVector n → bool ≝
    710722λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
    … …  
    729741  ].
    730742
     743example sub_minus_one_seven_eight:
     744  ∀v: BitVector 7.
     745  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
     746  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
     747 cases daemon.
     748qed.
     749
     750axiom sub16_with_carry_overflow:
     751  ∀left, right, result: BitVector 16.
     752  ∀flags: BitVector 3.
     753  ∀upper: BitVector 9.
     754  ∀lower: BitVector 7.
     755    sub_16_with_carry left right false = 〈result, flags〉 →
     756      vsplit bool 9 7 result = 〈upper, lower〉 →
     757        get_index_v bool 3 flags 2 ? = true →
     758          upper = [[true; true; true; true; true; true; true; true; true]].
     759  //
     760qed.
     761
     762axiom sub_16_to_add_16_8_0:
     763 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
     764  get_index' ? 2 0 flags = false →
     765  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
     766   v1 = add ? v2 (sign_extension (false:::v3)).
     767
     768axiom sub_16_to_add_16_8_1:
     769 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
     770  get_index' ? 2 0 flags = true →
     771  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
     772   v1 = add ? v2 (sign_extension (true:::v3)).

  • src/ASM/AssemblyProof.ma

    r2122 r2124  
    3737qed.
    3838
    39 (*CSC: move elsewhere *)
    40 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
    41   λa, b: addressing_mode.
    42   match a with
    43   [ DIRECT d ⇒
    44     match b with
    45     [ DIRECT e ⇒ eq_bv ? d e
    46     | _ ⇒ false
    47     ]
    48   | INDIRECT b' ⇒
    49     match b with
    50     [ INDIRECT e ⇒ eq_b b' e
    51     | _ ⇒ false
    52     ]
    53   | EXT_INDIRECT b' ⇒
    54     match b with
    55     [ EXT_INDIRECT e ⇒ eq_b b' e
    56     | _ ⇒ false
    57     ]
    58   | REGISTER bv ⇒
    59     match b with
    60     [ REGISTER bv' ⇒ eq_bv ? bv bv'
    61     | _ ⇒ false
    62     ]
    63   | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
    64   | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
    65   | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
    66   | DATA b' ⇒
    67     match b with
    68     [ DATA e ⇒ eq_bv ? b' e
    69     | _ ⇒ false
    70     ]
    71   | DATA16 w ⇒
    72     match b with
    73     [ DATA16 e ⇒ eq_bv ? w e
    74     | _ ⇒ false
    75     ]
    76   | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
    77   | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
    78   | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
    79   | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
    80   | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
    81   | BIT_ADDR b' ⇒
    82     match b with
    83     [ BIT_ADDR e ⇒ eq_bv ? b' e
    84     | _ ⇒ false
    85     ]
    86   | N_BIT_ADDR b' ⇒
    87     match b with
    88     [ N_BIT_ADDR e ⇒ eq_bv ? b' e
    89     | _ ⇒ false
    90     ]
    91   | RELATIVE n ⇒
    92     match b with
    93     [ RELATIVE e ⇒ eq_bv ? n e
    94     | _ ⇒ false
    95     ]
    96   | ADDR11 w ⇒
    97     match b with
    98     [ ADDR11 e ⇒ eq_bv ? w e
    99     | _ ⇒ false
    100     ]
    101   | ADDR16 w ⇒
    102     match b with
    103     [ ADDR16 e ⇒ eq_bv ? w e
    104     | _ ⇒ false
    105     ]
    106   ].
    107 
    108 (*CSC: move elsewhere *)
    109 lemma eq_addressing_mode_refl:
    110   ∀a. eq_addressing_mode a a = true.
    111   #a
    112   cases a try #arg1 try #arg2
    113   try @eq_bv_refl try @eq_b_refl
    114   try normalize %
    115 qed.
    116  
    117 (*CSC: move elsewhere *)
    118 definition eq_sum:
    119     ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
    120   λlt, rt, leq, req, left, right.
    121     match left with
    122     [ inl l ⇒
    123       match right with
    124       [ inl l' ⇒ leq l l'
    125       | _ ⇒ false
    126       ]
    127     | inr r ⇒
    128       match right with
    129       [ inr r' ⇒ req r r'
    130       | _ ⇒ false
    131       ]
    132     ].
    133 
    134 (*CSC: move elsewhere *)
    135 definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
    136   λlt, rt, leq, req, left, right.
    137     let 〈l, r〉 ≝ left in
    138     let 〈l', r'〉 ≝ right in
    139       leq l l' ∧ req r r'.
    140 
    141 (*CSC: move elsewhere *)
    142 definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
    143   λi, j.
    144   match i with
    145   [ ADD arg1 arg2 ⇒
    146     match j with
    147     [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    148     | _ ⇒ false
    149     ]
    150   | ADDC arg1 arg2 ⇒
    151     match j with
    152     [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    153     | _ ⇒ false
    154     ]
    155   | SUBB arg1 arg2 ⇒
    156     match j with
    157     [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    158     | _ ⇒ false
    159     ]
    160   | INC arg ⇒
    161     match j with
    162     [ INC arg' ⇒ eq_addressing_mode arg arg'
    163     | _ ⇒ false
    164     ]
    165   | DEC arg ⇒
    166     match j with
    167     [ DEC arg' ⇒ eq_addressing_mode arg arg'
    168     | _ ⇒ false
    169     ]
    170   | MUL arg1 arg2 ⇒
    171     match j with
    172     [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    173     | _ ⇒ false
    174     ]
    175   | DIV arg1 arg2 ⇒
    176     match j with
    177     [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    178     | _ ⇒ false
    179     ]
    180   | DA arg ⇒
    181     match j with
    182     [ DA arg' ⇒ eq_addressing_mode arg arg'
    183     | _ ⇒ false
    184     ]
    185   | JC arg ⇒
    186     match j with
    187     [ JC arg' ⇒ eq_addressing_mode arg arg'
    188     | _ ⇒ false
    189     ]
    190   | JNC arg ⇒
    191     match j with
    192     [ JNC arg' ⇒ eq_addressing_mode arg arg'
    193     | _ ⇒ false
    194     ]
    195   | JB arg1 arg2 ⇒
    196     match j with
    197     [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    198     | _ ⇒ false
    199     ]
    200   | JNB arg1 arg2 ⇒
    201     match j with
    202     [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    203     | _ ⇒ false
    204     ]
    205   | JBC arg1 arg2 ⇒
    206     match j with
    207     [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    208     | _ ⇒ false
    209     ]
    210   | JZ arg ⇒
    211     match j with
    212     [ JZ arg' ⇒ eq_addressing_mode arg arg'
    213     | _ ⇒ false
    214     ]
    215   | JNZ arg ⇒
    216     match j with
    217     [ JNZ arg' ⇒ eq_addressing_mode arg arg'
    218     | _ ⇒ false
    219     ]
    220   | CJNE arg1 arg2 ⇒
    221     match j with
    222     [ CJNE arg1' arg2' ⇒
    223       let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
    224       let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
    225       let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    226         arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    227     | _ ⇒ false
    228     ]
    229   | DJNZ arg1 arg2 ⇒
    230     match j with
    231     [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    232     | _ ⇒ false
    233     ]
    234   | CLR arg ⇒
    235     match j with
    236     [ CLR arg' ⇒ eq_addressing_mode arg arg'
    237     | _ ⇒ false
    238     ]
    239   | CPL arg ⇒
    240     match j with
    241     [ CPL arg' ⇒ eq_addressing_mode arg arg'
    242     | _ ⇒ false
    243     ]
    244   | RL arg ⇒
    245     match j with
    246     [ RL arg' ⇒ eq_addressing_mode arg arg'
    247     | _ ⇒ false
    248     ]
    249   | RLC arg ⇒
    250     match j with
    251     [ RLC arg' ⇒ eq_addressing_mode arg arg'
    252     | _ ⇒ false
    253     ]
    254   | RR arg ⇒
    255     match j with
    256     [ RR arg' ⇒ eq_addressing_mode arg arg'
    257     | _ ⇒ false
    258     ]
    259   | RRC arg ⇒
    260     match j with
    261     [ RRC arg' ⇒ eq_addressing_mode arg arg'
    262     | _ ⇒ false
    263     ]
    264   | SWAP arg ⇒
    265     match j with
    266     [ SWAP arg' ⇒ eq_addressing_mode arg arg'
    267     | _ ⇒ false
    268     ]
    269   | SETB arg ⇒
    270     match j with
    271     [ SETB arg' ⇒ eq_addressing_mode arg arg'
    272     | _ ⇒ false
    273     ]
    274   | PUSH arg ⇒
    275     match j with
    276     [ PUSH arg' ⇒ eq_addressing_mode arg arg'
    277     | _ ⇒ false
    278     ]
    279   | POP arg ⇒
    280     match j with
    281     [ POP arg' ⇒ eq_addressing_mode arg arg'
    282     | _ ⇒ false
    283     ]
    284   | XCH arg1 arg2 ⇒
    285     match j with
    286     [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    287     | _ ⇒ false
    288     ]
    289   | XCHD arg1 arg2 ⇒
    290     match j with
    291     [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    292     | _ ⇒ false
    293     ]
    294   | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
    295   | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
    296   | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
    297   | MOVX arg ⇒
    298     match j with
    299     [ MOVX arg' ⇒
    300       let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
    301       let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
    302       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    303         sum_eq arg arg'
    304     | _ ⇒ false
    305     ]
    306   | XRL arg ⇒
    307     match j with
    308     [ XRL arg' ⇒
    309       let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
    310       let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
    311       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    312         sum_eq arg arg'
    313     | _ ⇒ false
    314     ]
    315   | ORL arg ⇒
    316     match j with
    317     [ ORL arg' ⇒
    318       let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
    319       let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
    320       let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
    321       let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
    322       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    323         sum_eq arg arg'
    324     | _ ⇒ false
    325     ]
    326   | ANL arg ⇒
    327     match j with
    328     [ ANL arg' ⇒
    329       let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
    330       let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
    331       let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
    332       let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
    333       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    334         sum_eq arg arg'
    335     | _ ⇒ false
    336     ]
    337   | MOV arg ⇒
    338     match j with
    339     [ MOV arg' ⇒
    340       let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
    341       let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
    342       let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
    343       let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
    344       let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
    345       let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
    346       let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
    347       let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
    348       let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
    349       let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
    350       let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
    351         sum_eq_5 arg arg'
    352     | _ ⇒ false
    353     ]
    354   ].
    355 
    356 (*CSC: move elsewhere *)
    357 lemma eq_sum_refl:
    358   ∀A, B: Type[0].
    359   ∀leq, req.
    360   ∀s.
    361   ∀leq_refl: (∀t. leq t t = true).
    362   ∀req_refl: (∀u. req u u = true).
    363     eq_sum A B leq req s s = true.
    364   #A #B #leq #req #s #leq_refl #req_refl
    365   cases s assumption
    366 qed.
    367 
    368 (*CSC: move elsewhere *)
    369 lemma eq_prod_refl:
    370   ∀A, B: Type[0].
    371   ∀leq, req.
    372   ∀s.
    373   ∀leq_refl: (∀t. leq t t = true).
    374   ∀req_refl: (∀u. req u u = true).
    375     eq_prod A B leq req s s = true.
    376   #A #B #leq #req #s #leq_refl #req_refl
    377   cases s
    378   whd in ⊢ (? → ? → ??%?);
    379   #l #r
    380   >leq_refl @req_refl
    381 qed.
    382 
    383 (*CSC: move elsewhere *)
    384 lemma eq_preinstruction_refl:
    385   ∀i.
    386     eq_preinstruction i i = true.
    387   #i cases i try #arg1 try #arg2
    388   try @eq_addressing_mode_refl
    389   [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    390     whd in ⊢ (??%?); try %
    391     >eq_addressing_mode_refl
    392     >eq_addressing_mode_refl %
    393   |13,15:
    394     whd in ⊢ (??%?);
    395     cases arg1
    396     [*:
    397       #arg1_left normalize nodelta
    398       >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
    399     ]
    400   |11,12:
    401     whd in ⊢ (??%?);
    402     cases arg1
    403     [1:
    404       #arg1_left normalize nodelta
    405       >(eq_sum_refl …)
    406       [1: % | 2,3: #arg @eq_prod_refl ]
    407       @eq_addressing_mode_refl
    408     |2:
    409       #arg1_left normalize nodelta
    410       @eq_prod_refl [*: @eq_addressing_mode_refl ]
    411     |3:
    412       #arg1_left normalize nodelta
    413       >(eq_sum_refl …)
    414       [1:
    415         %
    416       |2,3:
    417         #arg @eq_prod_refl #arg @eq_addressing_mode_refl
    418       ]
    419     |4:
    420       #arg1_left normalize nodelta
    421       @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
    422     ]
    423   |14:
    424     whd in ⊢ (??%?);
    425     cases arg1
    426     [1:
    427       #arg1_left normalize nodelta
    428       @eq_sum_refl
    429       [1:
    430         #arg @eq_sum_refl
    431         [1:
    432           #arg @eq_sum_refl
    433           [1:
    434             #arg @eq_sum_refl
    435             [1:
    436               #arg @eq_prod_refl
    437               [*:
    438                 @eq_addressing_mode_refl
    439               ]
    440             |2:
    441               #arg @eq_prod_refl
    442               [*:
    443                 #arg @eq_addressing_mode_refl
    444               ]
    445             ]
    446           |2:
    447             #arg @eq_prod_refl
    448             [*:
    449               #arg @eq_addressing_mode_refl
    450             ]
    451           ]
    452         |2:
    453           #arg @eq_prod_refl
    454           [*:
    455             #arg @eq_addressing_mode_refl
    456           ]
    457         ]
    458       |2:
    459         #arg @eq_prod_refl
    460         [*:
    461           #arg @eq_addressing_mode_refl
    462         ]
    463       ]
    464     |2:
    465       #arg1_right normalize nodelta
    466       @eq_prod_refl
    467       [*:
    468         #arg @eq_addressing_mode_refl
    469       ]
    470     ]
    471   |*:
    472     whd in ⊢ (??%?);
    473     cases arg1
    474     [*:
    475       #arg1 >eq_sum_refl
    476       [1,4:
    477         @eq_addressing_mode_refl
    478       |2,3,5,6:
    479         #arg @eq_prod_refl
    480         [*:
    481           #arg @eq_addressing_mode_refl
    482         ]
    483       ]
    484     ]
    485   ]
    486 qed.
    487 
    488 (*CSC: move elsewhere *)
    489 definition eq_instruction: instruction → instruction → bool ≝
    490   λi, j.
    491   match i with
    492   [ ACALL arg ⇒
    493     match j with
    494     [ ACALL arg' ⇒ eq_addressing_mode arg arg'
    495     | _ ⇒ false
    496     ]
    497   | LCALL arg ⇒
    498     match j with
    499     [ LCALL arg' ⇒ eq_addressing_mode arg arg'
    500     | _ ⇒ false
    501     ]
    502   | AJMP arg ⇒
    503     match j with
    504     [ AJMP arg' ⇒ eq_addressing_mode arg arg'
    505     | _ ⇒ false
    506     ]
    507   | LJMP arg ⇒
    508     match j with
    509     [ LJMP arg' ⇒ eq_addressing_mode arg arg'
    510     | _ ⇒ false
    511     ]
    512   | SJMP arg ⇒
    513     match j with
    514     [ SJMP arg' ⇒ eq_addressing_mode arg arg'
    515     | _ ⇒ false
    516     ]
    517   | JMP arg ⇒
    518     match j with
    519     [ JMP arg' ⇒ eq_addressing_mode arg arg'
    520     | _ ⇒ false
    521     ]
    522   | MOVC arg1 arg2 ⇒
    523     match j with
    524     [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    525     | _ ⇒ false
    526     ]
    527   | RealInstruction instr ⇒
    528     match j with
    529     [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
    530     | _ ⇒ false
    531     ]
    532   ].
    533  
    534 (*CSC: move elsewhere *)
    535 lemma eq_instruction_refl:
    536   ∀i. eq_instruction i i = true.
    537   #i cases i [*: #arg1 ]
    538   try @eq_addressing_mode_refl
    539   try @eq_preinstruction_refl
    540   #arg2 whd in ⊢ (??%?);
    541   >eq_addressing_mode_refl >eq_addressing_mode_refl %
    542 qed.
    543 
    544 (*CSC: in is_a_to_mem_to_is_in use vect_member in place of mem … *)
    545 definition vect_member ≝
    546  λA,n,eq,v,a. mem A eq (S n) v a.
    547 
    548 (*CSC: move elsewhere*)
    549 definition is_in_cons_elim:
    550  ∀len.∀hd,tl.∀m:addressing_mode
    551   .is_in (S len) (hd:::tl) m →
    552     (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
    553  #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
    554  cases (is_a hd am) in ISIN; /2/
    555 qed.
    556 
    557 (*CSC: move elsewhere*)
    558 lemma prod_eq_left:
    559   ∀A: Type[0].
    560   ∀p, q, r: A.
    561     p = q → 〈p, r〉 = 〈q, r〉.
    562   #A #p #q #r #hyp
    563   destruct %
    564 qed.
    565 
    566 (*CSC: move elsewhere*)
    567 lemma prod_eq_right:
    568   ∀A: Type[0].
    569   ∀p, q, r: A.
    570     p = q → 〈r, p〉 = 〈r, q〉.
    571   #A #p #q #r #hyp
    572   destruct %
    573 qed.
    574 
    57539let rec encoding_check
    57640  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
    … …  
    58347      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
    58448  ].
    585 
    586 (*CSC: move elsewhere *)
    587 lemma add_bitvector_of_nat_Sm:
    588   ∀n, m: nat.
    589     add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
    590       bitvector_of_nat n (S m).
    591  #n #m @add_bitvector_of_nat_plus
    592 qed.
    59349
    59450lemma encoding_check_append:
    … …  
    62278    ]
    62379  ]
    624 qed.
    625 
    626 (*CSC: move elsewhere*)
    627 lemma destruct_bug_fix_1:
    628   ∀n: nat.
    629     S n = 0 → False.
    630   #n #absurd destruct(absurd)
    631 qed.
    632 
    633 (*CSC: move elsewhere*)
    634 lemma destruct_bug_fix_2:
    635   ∀m, n: nat.
    636     S m = S n → m = n.
    637   #m #n #refl destruct %
    638 qed.
    639 
    640 (*CSC: move elsewhere*)
    641 definition bitvector_3_cases:
    642   ∀b: BitVector 3.
    643     ∃l, c, r: bool.
    644       b ≃ [[l; c; r]].
    645   #b
    646   @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
    647   [1:
    648     #absurd @⊥ -b @(destruct_bug_fix_1 2)
    649     >absurd %
    650   |2:
    651     #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
    652     cut (n = 2)
    653     [1:
    654       @destruct_bug_fix_2
    655       >size_refl %
    656     |2:
    657       #n_refl >n_refl in tl; #V
    658       @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
    659       [1:
    660         #absurd @⊥ -V @(destruct_bug_fix_1 1)
    661         >absurd %
    662       |2:
    663         #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
    664         cut (n' = 1)
    665         [1:
    666           @destruct_bug_fix_2 >size_refl' %
    667         |2:
    668           #n_refl' >n_refl' in tl'; #V'
    669           @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
    670           [1:
    671             #absurd @⊥ -V' @(destruct_bug_fix_1 0)
    672             >absurd %
    673           |2:
    674             #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
    675             cut (n'' = 0)
    676             [1:
    677               @destruct_bug_fix_2 >size_refl'' %
    678             |2:
    679               #n_refl'' >n_refl'' in tl''; #tl'''
    680               >(Vector_O … tl''') %
    681             ]
    682           ]
    683         ]
    684       ]
    685     ]
    686   ]
    687 qed.
    688 
    689 (*CSC: move elsewhere*)
    690 lemma bitvector_3_elim_prop:
    691   ∀P: BitVector 3 → Prop.
    692     P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
    693     P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
    694     P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
    695   #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
    696   cases (bitvector_3_cases … H9) #l #assm cases assm
    697   -assm #c #assm cases assm
    698   -assm #r #assm cases assm destruct
    699   cases l cases c cases r assumption
    70080qed.
    70181
    … …  
    750130        fetch_many code_memory final_pc pc' tl)
    751131  ].
    752 
    753 (*CSC: move elsewhere*)
    754 lemma option_destruct_Some:
    755   ∀A: Type[0].
    756   ∀a, b: A.
    757     Some A a = Some A b → a = b.
    758   #A #a #b #EQ
    759   destruct %
    760 qed.
    761 
    762 (*CSC: move elsewhere*)
    763 lemma eq_instruction_to_eq:
    764   ∀i1, i2: instruction.
    765     eq_instruction i1 i2 = true → i1 ≃ i2.
    766   #i1 #i2
    767   cases i1 cases i2 cases daemon (* easy but tedious
    768   [1,10,19,28,37,46:
    769     #arg1 #arg2
    770     whd in match (eq_instruction ??);
    771     cases arg1 #subaddressing_mode
    772     cases subaddressing_mode
    773     try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    774     try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    775     try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
    776     #word11 #irrelevant
    777     cases arg2 #subaddressing_mode
    778     cases subaddressing_mode
    779     try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    780     try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    781     try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
    782     #word11' #irrelevant normalize nodelta
    783     #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
    784 qed.
    785132         
    786133lemma fetch_assembly_pseudo':
    … …  
    1429776     ticks_of0 program sigma policy ppc fetched.
    1430777
    1431 (*CSC: move elsewhere*)
    1432 lemma eq_rect_Type1_r:
    1433   ∀A: Type[1].
    1434   ∀a: A.
    1435   ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    1436   #A #a #P #H #x #p
    1437   generalize in match H;
    1438   generalize in match P;
    1439   cases p //
    1440 qed.
    1441 
    1442778(*
    1443779lemma blah:
    … …  
    1569905*)
    1570906
    1571 (*CSC: move elsewhere*)
    1572 lemma Some_Some_elim:
    1573  ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
    1574  #T #x #y #P #H #K @H @option_destruct_Some //
    1575 qed.
    1576 
    1577 (*CSC: move elsewhere*)
    1578 lemma pair_destruct_right:
    1579   ∀A: Type[0].
    1580   ∀B: Type[0].
    1581   ∀a, c: A.
    1582   ∀b, d: B.
    1583     〈a, b〉 = 〈c, d〉 → b = d.
    1584   #A #B #a #b #c #d //
    1585 qed.
    1586    
    1587907(*CSC: ???*)
    1588908(* XXX: we need a precondition here stating that the PPC is within the
    … …  
    1633953  @pair_elim #lbl #instr #nth_refl normalize nodelta
    1634954  #G cases (pair_destruct_right ?????? G) %
    1635 qed.
    1636 
    1637 (*CSC: move elsewhere*)
    1638 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
    1639   /2/
    1640955qed.
    1641956

  • src/ASM/AssemblyProofSplit.ma

    r2122 r2124  
    170170qed.
    171171
    172 (*CSC: move elsewhere*)
    173 lemma pair_replace:
    174  ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
    175   P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
    176  #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
    177 qed.
    178 
    179172lemma get_arg_8_set_program_counter:
    180173  ∀M: Type[0].
    … …  
    327320qed.
    328321
    329 (*CSC: move elsewhere*)
    330 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
    331  #P #A #a #abs destruct
    332 qed.
    333 
    334322(*
    335323lemma pi1_let_commute:
    … …  
    360348include alias "basics/logic.ma".
    361349include alias "ASM/BitVectorTrie.ma".
    362 
    363 (*CSC: move elsewhere*)
    364 lemma jmpair_as_replace:
    365  ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.
    366   ∀EQ:c ≃ 〈a,b〉.
    367   P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')).
    368   [2:
    369     >EQc @EQ
    370   |1:
    371     #A #B #T #P #a #b
    372     #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ
    373     letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ]
    374     change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ;
    375     @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta
    376     -EQ cases c in f; normalize //
    377   ]
    378 qed.
    379 
    380 (*CSC: move elsewhere*)
    381 lemma if_then_else_replace:
    382   ∀T: Type[0].
    383   ∀P: T → Prop.
    384   ∀t1, t2: T.
    385   ∀c, c', c'': bool.
    386     c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
    387   #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
    388   assumption
    389 qed.
    390350
    391351lemma fetch_many_singleton:
    … …  
    398358  #fetch_many_assm whd in fetch_many_assm;
    399359  cases (eq_bv_eq … fetch_many_assm) assumption
    400 qed.
    401 
    402 (*CSC: move elsewhere*)
    403 lemma refl_to_jmrefl:
    404   ∀a: Type[0].
    405   ∀l, r: a.
    406     l = r → l ≃ r.
    407   #a #l #r #refl destruct %
    408360qed.
    409361

  • src/ASM/BitVector.ma

    r2122 r2124  
    236236    String.
    237237
    238 example sub_minus_one_seven_eight:
    239   ∀v: BitVector 7.
    240   false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
    241   \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
    242  cases daemon.
    243 qed.
    244 
    245 axiom sub16_with_carry_overflow:
    246   ∀left, right, result: BitVector 16.
    247   ∀flags: BitVector 3.
    248   ∀upper: BitVector 9.
    249   ∀lower: BitVector 7.
    250     sub_16_with_carry left right false = 〈result, flags〉 →
    251       vsplit bool 9 7 result = 〈upper, lower〉 →
    252         get_index_v bool 3 flags 2 ? = true →
    253           upper = [[true; true; true; true; true; true; true; true; true]].
    254   //
    255 qed.
    256 
    257 axiom sub_16_to_add_16_8_0:
    258  ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
    259   get_index' ? 2 0 flags = false →
    260   sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
    261    v1 = add ? v2 (sign_extension (false:::v3)).
    262 
    263 axiom sub_16_to_add_16_8_1:
    264  ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
    265   get_index' ? 2 0 flags = true →
    266   sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
    267    v1 = add ? v2 (sign_extension (true:::v3)).
     238definition bitvector_3_cases:
     239  ∀b: BitVector 3.
     240    ∃l, c, r: bool.
     241      b ≃ [[l; c; r]].
     242  #b
     243  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
     244  [1:
     245    #absurd @⊥ -b @(destruct_bug_fix_1 2)
     246    >absurd %
     247  |2:
     248    #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
     249    cut (n = 2)
     250    [1:
     251      @destruct_bug_fix_2
     252      >size_refl %
     253    |2:
     254      #n_refl >n_refl in tl; #V
     255      @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
     256      [1:
     257        #absurd @⊥ -V @(destruct_bug_fix_1 1)
     258        >absurd %
     259      |2:
     260        #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
     261        cut (n' = 1)
     262        [1:
     263          @destruct_bug_fix_2 >size_refl' %
     264        |2:
     265          #n_refl' >n_refl' in tl'; #V'
     266          @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
     267          [1:
     268            #absurd @⊥ -V' @(destruct_bug_fix_1 0)
     269            >absurd %
     270          |2:
     271            #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
     272            cut (n'' = 0)
     273            [1:
     274              @destruct_bug_fix_2 >size_refl'' %
     275            |2:
     276              #n_refl'' >n_refl'' in tl''; #tl'''
     277              >(Vector_O … tl''') %
     278            ]
     279          ]
     280        ]
     281      ]
     282    ]
     283  ]
     284qed.
     285
     286lemma bitvector_3_elim_prop:
     287  ∀P: BitVector 3 → Prop.
     288    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
     289    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
     290    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
     291  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     292  cases (bitvector_3_cases … H9) #l #assm cases assm
     293  -assm #c #assm cases assm
     294  -assm #r #assm cases assm destruct
     295  cases l cases c cases r assumption
     296qed.

  • src/ASM/Fetch.ma

    r2119 r2124  
    1717  λpc: Word.
    1818    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
    19 
    20 (*CSC: move elsewhere *)
    21 axiom eq_bitvector_of_nat_to_eq:
    22  ∀n,n1,n2.
    23   n1 < 2^n → n2 < 2^n →
    24    bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
    25 
    26 discriminator Prod.
    2719
    2820definition load_code_memory0:

  • src/ASM/Interpret.ma

    r2108 r2124  
    957957qed.
    958958
    959 discriminator Prod.
    960 
    961959definition compute_target_of_unconditional_jump:
    962960    ∀program_counter: Word.

  • src/ASM/StatusProofs.ma

    r2032 r2124  
    344344   program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s.
    345345
    346 (* XXX: to be moved elsewhere *)
    347346lemma program_counter_set_arg_8:
    348347  ∀m, cm, s, addr, v.

  • src/ASM/Util.ma

    r2123 r2124  
    14781478qed.
    14791479
     1480(*CSC: just a synonim, get rid of it!*)
     1481lemma Some_eq:
     1482 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y ≝ option_destruct_Some.
     1483
    14801484lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
    14811485  s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
    … …  
    14831487qed.
    14841488
    1485 lemma Some_eq:
    1486  ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
    1487  #T #x #y #H @option_destruct_Some @H
    1488 qed.
    1489 
    14901489lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?.
    14911490#A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS')
    … …  
    14941493coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝
    14951494  not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?.
     1495
     1496lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
     1497 #P #A #a #abs destruct
     1498qed.
     1499
     1500discriminator Prod.
     1501
     1502lemma pair_replace:
     1503 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
     1504  P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
     1505 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
     1506qed.
     1507
     1508lemma jmpair_as_replace:
     1509 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.
     1510  ∀EQ:c ≃ 〈a,b〉.
     1511  P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')).
     1512  [2:
     1513    >EQc @EQ
     1514  |1:
     1515    #A #B #T #P #a #b
     1516    #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ
     1517    letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ]
     1518    change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ;
     1519    @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta
     1520    -EQ cases c in f; normalize //
     1521  ]
     1522qed.
     1523
     1524lemma if_then_else_replace:
     1525  ∀T: Type[0].
     1526  ∀P: T → Prop.
     1527  ∀t1, t2: T.
     1528  ∀c, c', c'': bool.
     1529    c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
     1530  #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
     1531  assumption
     1532qed.
     1533
     1534lemma refl_to_jmrefl:
     1535  ∀a: Type[0].
     1536  ∀l, r: a.
     1537    l = r → l ≃ r.
     1538  #a #l #r #refl destruct %
     1539qed.
     1540
     1541lemma prod_eq_left:
     1542  ∀A: Type[0].
     1543  ∀p, q, r: A.
     1544    p = q → 〈p, r〉 = 〈q, r〉.
     1545  #A #p #q #r #hyp
     1546  destruct %
     1547qed.
     1548
     1549lemma prod_eq_right:
     1550  ∀A: Type[0].
     1551  ∀p, q, r: A.
     1552    p = q → 〈r, p〉 = 〈r, q〉.
     1553  #A #p #q #r #hyp
     1554  destruct %
     1555qed.
     1556
     1557lemma destruct_bug_fix_1:
     1558  ∀n: nat.
     1559    S n = 0 → False.
     1560  #n #absurd destruct(absurd)
     1561qed.
     1562
     1563lemma destruct_bug_fix_2:
     1564  ∀m, n: nat.
     1565    S m = S n → m = n.
     1566  #m #n #refl destruct %
     1567qed.
     1568
     1569lemma eq_rect_Type1_r:
     1570  ∀A: Type[1].
     1571  ∀a: A.
     1572  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     1573  #A #a #P #H #x #p
     1574  generalize in match H;
     1575  generalize in match P;
     1576  cases p //
     1577qed.
     1578
     1579lemma Some_Some_elim:
     1580 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
     1581 #T #x #y #P #H #K @H @option_destruct_Some //
     1582qed.
     1583
     1584lemma pair_destruct_right:
     1585  ∀A: Type[0].
     1586  ∀B: Type[0].
     1587  ∀a, c: A.
     1588  ∀b, d: B.
     1589    〈a, b〉 = 〈c, d〉 → b = d.
     1590  #A #B #a #b #c #d //
     1591qed.
     1592
     1593lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
     1594  /2/
     1595qed.
     1596
     1597definition eq_sum:
     1598    ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
     1599  λlt, rt, leq, req, left, right.
     1600    match left with
     1601    [ inl l ⇒
     1602      match right with
     1603      [ inl l' ⇒ leq l l'
     1604      | _ ⇒ false
     1605      ]
     1606    | inr r ⇒
     1607      match right with
     1608      [ inr r' ⇒ req r r'
     1609      | _ ⇒ false
     1610      ]
     1611    ].
     1612
     1613lemma eq_sum_refl:
     1614  ∀A, B: Type[0].
     1615  ∀leq, req.
     1616  ∀s.
     1617  ∀leq_refl: (∀t. leq t t = true).
     1618  ∀req_refl: (∀u. req u u = true).
     1619    eq_sum A B leq req s s = true.
     1620  #A #B #leq #req #s #leq_refl #req_refl
     1621  cases s assumption
     1622qed.
     1623
     1624definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
     1625  λlt, rt, leq, req, left, right.
     1626    let 〈l, r〉 ≝ left in
     1627    let 〈l', r'〉 ≝ right in
     1628      leq l l' ∧ req r r'.
     1629
     1630lemma eq_prod_refl:
     1631  ∀A, B: Type[0].
     1632  ∀leq, req.
     1633  ∀s.
     1634  ∀leq_refl: (∀t. leq t t = true).
     1635  ∀req_refl: (∀u. req u u = true).
     1636    eq_prod A B leq req s s = true.
     1637  #A #B #leq #req #s #leq_refl #req_refl
     1638  cases s
     1639  whd in ⊢ (? → ? → ??%?);
     1640  #l #r
     1641  >leq_refl @req_refl
     1642qed.
    14961643 
    14971644lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.

  • src/ASM/Vector.ma

    r2122 r2124  
    223223 vsplit' A m n v.
    224224
    225 lemma vsplit_ok:
    226   ∀A: Type[0].
    227   ∀m, n: nat.
    228   ∀v: Vector A (m + n).
    229   ∀upper: Vector A m.
    230   ∀lower: Vector A n.
    231     〈upper, lower〉 = vsplit A m n v →
    232       upper @@ lower = v.
    233   #A #m #n #v #upper #lower
    234   cases daemon
    235 qed.
    236 
    237225lemma vsplit_zero:
    238226  ∀A,m.
    … …  
    376364   
    377365interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
     366
     367
     368lemma vsplit_ok:
     369  ∀A: Type[0].
     370  ∀m, n: nat.
     371  ∀v: Vector A (m + n).
     372  ∀upper: Vector A m.
     373  ∀lower: Vector A n.
     374    〈upper, lower〉 = vsplit A m n v →
     375      upper @@ lower = v.
     376  #A #m #n #v #upper #lower
     377  cases daemon
     378qed.
    378379
    379380lemma vector_append_zero:
Note: See TracChangeset for help on using the changeset viewer.