Changeset 1602 for src/ASM


Ignore:
Timestamp:
Dec 13, 2011, 4:23:40 PM (8 years ago)
Author:
mulligan
Message:

giving up on fetch proofs for time being

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r1600 r1602  
    2727    nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))).
    2828
     29lemma minus_leq_minus:
     30  ∀m, n, o: nat.
     31    n ≤ m → o ≤ m → o ≤ n → m - n ≤ m - o.
     32  #m #n #o #m_le_n #m_le_o #o_le_n
     33  cases daemon (* XXX: todo *)
     34qed.
     35
    2936definition next: BitVectorTrie Byte 16 → ∀program_counter: Word.
    30     nat_of_bitvector … program_counter < (code_memory_size - 1) →
    31       Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ≝
     37    nat_of_bitvector … program_counter < (code_memory_size - 24) →
     38      Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ∧
     39        (nat_of_bitvector … (\fst ret)) ≤ code_memory_size ≝
    3240  λpmem: BitVectorTrie Byte 16.
    3341  λpc: Word.
    3442  λproof.
    3543    〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
    36   @w_lt_half_add_increment @proof
     44  @conj
     45  [1:
     46    @w_lt_half_add_increment
     47    @(transitive_le
     48      (S (nat_of_bitvector … pc))
     49      (code_memory_size - 24)
     50      (code_memory_size - 1) ? ?)
     51    [1:
     52      @proof
     53    |2:
     54      @(minus_leq_minus code_memory_size 24 1) //
     55    ]
     56  |2:
     57    cases daemon (* XXX: todo *)
     58  ]
    3759qed.
    3860
     
    150172         else
    151173          let 〈b,v〉≝  head … v in if b then
    152            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
     174           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
    153175          else
    154176           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
     
    191213      let 〈b,v〉≝  head … v in if b then
    192214       let 〈b,v〉≝  head … v in if b then
    193         let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    194        else
    195         let 〈b,v〉≝  head … v in if b then
    196          let 〈b,v〉≝  head … v in if b then
    197           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    198          else
    199           let 〈b,v〉≝  head … v in if b then
    200            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
    201           else
    202            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     215        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     216       else
     217        let 〈b,v〉≝  head … v in if b then
     218         let 〈b,v〉≝  head … v in if b then
     219          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     220         else
     221          let 〈b,v〉≝  head … v in if b then
     222           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
     223          else
     224           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    203225        else
    204226         let 〈b,v〉≝  head … v in if b then
     
    255277           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    256278          else
    257            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
     279           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
    258280      else
    259281       let 〈b,v〉≝  head … v in if b then
     
    265287         else
    266288          let 〈b,v〉≝  head … v in if b then
    267            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
     289           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
    268290          else
    269291           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
     
    291313         else
    292314          let 〈b,v〉≝  head … v in if b then
    293            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
     315           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
    294316          else
    295317           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
     
    320342         let 〈b,v〉≝  head … v in if b then
    321343          let 〈b,v〉≝  head … v in if b then
    322            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     344           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    323345          else
    324346           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     
    344366         let 〈b,v〉≝  head … v in if b then
    345367          let 〈b,v〉≝  head … v in if b then
    346            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     368           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    347369          else
    348370           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     
    367389         let 〈b,v〉≝  head … v in if b then
    368390          let 〈b,v〉≝  head … v in if b then
    369            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     391           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    370392          else
    371393           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     
    399421           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    400422          else
    401            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     423           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    402424      else
    403425       let 〈b,v〉≝  head … v in if b then
     
    422444           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    423445          else
    424            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     446           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    425447     else
    426448      let 〈b,v〉≝  head … v in if b then
     
    441463           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
    442464          else
    443            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     465           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    444466         else
    445467          let 〈b,v〉≝  head … v in if b then
    446468           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    447469          else
    448            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     470           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    449471      else
    450472       let 〈b,v〉≝  head … v in if b then
     
    464486           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
    465487          else
    466            let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     488           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    467489         else
    468490          let 〈b,v〉≝  head … v in if b then
     
    471493           〈〈RealInstruction (NOP …), pc〉, 1〉.
    472494  try %
     495  cases daemon (*
    473496  try (
    474497    @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
     
    476499      (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)
    477500  )
    478   [1,2,3,4,5,6,7,8:
     501  [6,8,14,15,16,17,20,21,22,23,25,28,30,31,32,33,34,37,38,39,40,41,44,45,46,47,
     502   50,51,52,53,56,57,58,59,65,69,71,73,75:
     503    cases daemon (* XXX: segmentation fault *)
     504  |1,2,3,4,5,7,8,9,10,11,12,13,18,19,24,26,27,29,35,36,42,43,48,49,54,55,60,61,
     505   62,63,64,66,67,68,70,72,74,76:
    479506    @breakup_pair' cases (next pmem pc ?)
    480507    normalize * normalize #pc' #byte @lt_to_le
    481   |3:
    482     @breakup_pair' cases (next pmem pc ?)
    483     normalize * normalize #pc' #byte @lt_to_le
    484   |2:
    485     @breakup_pair' cases(next pmem pc ?)
    486     normalize * normalize #pc' #byte @lt_to_le
    487   [
    488   | 92:
    489     cases (next ???) in EQ; * #pc' #content #H #EQ whd in EQ:(??%?); destruct
    490    
    491    
    492     lapply(eq_pair_fst_snd ? ? (next pmem pc ?))
    493     #assm >assm
    494     cut(nat_of_bitvector … pc < nat_of_bitvector …
    495       (\fst  (next pmem pc
    496                 (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc)
    497                  code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof))))
    498     [ @sig2
    499     | #assm @lt_to_le assumption
    500     ]
    501   |92:
    502     check next.
    503     lapply pc -pc
    504     @sig2
    505   cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *)
     508  [30:
     509    generalize in match pc in EQ; #pc' #EQ' -pc
     510    cut(nat_of_bitvector … pc < nat_of_bitvector … pc')
     511    [1:
     512      cut(pc' = \fst (next pmem pc (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc)
     513         code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)))
     514      [1:
     515        //
     516      |2:
     517        #assm >assm @sig2
     518      ]
     519    | #lt_assm
     520      lapply(transitive_le
     521        (S (nat_of_bitvector … pc))
     522        (nat_of_bitvector … pc')
     523        (S (nat_of_bitvector … pc')) lt_assm ?)
     524      [1:
     525        //
     526      |2:
     527        #le_assm
     528        lapply(transitive_le
     529          (S (nat_of_bitvector … pc))
     530          (S (nat_of_bitvector … pc'))
     531          (code_memory_size - 1) le_assm ?)
     532        [2:
     533          //
     534        |1:
     535          @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
     536            (nat_of_bitvector … pc) code_memory_size 24 1 ? ?)
     537          [1:
     538            @le_S_S @le_S_S @le_O_n
     539          |2:
     540            assumption
     541          ]
     542        ]
     543      ]
     544    ] XXX: blah! *)
    506545qed.
    507546
  • src/ASM/Util.ma

    r1600 r1602  
    801801    %
    802802  | normalize
    803     /2/
     803    /3 by trans_eq, orb_true_l/
    804804  ]
    805805qed.
Note: See TracChangeset for help on using the changeset viewer.