Changeset 2108


Ignore:
Timestamp:
Jun 25, 2012, 2:39:06 PM (8 years ago)
Author:
mulligan
Message:

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

Location:
src/ASM
Files:
5 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Arithmetic.ma

    r2032 r2108  
    534534    \snd (half_add n l r).
    535535
    536 axiom add_zero:
     536lemma half_add_carry_Sn:
     537  ∀n: nat.
     538  ∀l: BitVector n.
     539  ∀hd: bool.
     540    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
     541      andb hd (\fst (half_add n l (zero n))).
     542  #n #l elim l
     543  [1:
     544    #hd normalize cases hd %
     545  |2:
     546    #n' #hd #tl #inductive_hypothesis #hd'
     547    whd in match half_add; normalize nodelta
     548    whd in match full_add; normalize nodelta
     549    normalize in ⊢ (??%%); cases hd' normalize
     550    @pair_elim #c1 #r #c1_r_refl cases c1 %
     551  ]
     552qed.
     553
     554lemma half_add_zero_carry_false:
     555  ∀m: nat.
     556  ∀b: BitVector m.
     557    \fst (half_add m b (zero m)) = false.
     558  #m #b elim b try %
     559  #n #hd #tl #inductive_hypothesis
     560  change with (false:::(zero ?)) in match (zero ?);
     561  >half_add_carry_Sn >inductive_hypothesis cases hd %
     562qed.
     563
     564axiom half_add_true_true_carry_true:
     565  ∀n: nat.
     566  ∀hd, hd': bool.
     567  ∀l, r: BitVector n.
     568    \fst (half_add (S n) (true:::l) (true:::r)) = true.
     569
     570lemma add_Sn_carry_add:
     571  ∀n: nat.
     572  ∀hd, hd': bool.
     573  ∀l, r: BitVector n.
     574    add (S n) (hd:::l) (hd':::r) =
     575      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
     576  #n #hd #hd' #l elim l
     577  [1:
     578    #r cases hd cases hd'
     579    >(BitVector_O … r) normalize %
     580  |2:
     581    #n' #hd'' #tl #inductive_hypothesis #r
     582    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
     583    cases hd cases hd' cases hd'' cases hd'''
     584    whd in match (xorb ??);
     585    cases daemon
     586  ]
     587qed.
     588 
     589lemma add_zero:
    537590  ∀n: nat.
    538591  ∀l: BitVector n.
    539592    l = add n l (zero …).
     593  #n #l elim l try %
     594  #n' #hd #tl #inductive_hypothesis
     595  change with (false:::zero ?) in match (zero ?);
     596  >add_Sn_carry_add >half_add_zero_carry_false
     597  cases hd <inductive_hypothesis %
     598qed.
     599
     600axiom most_significant_bit_zero:
     601  ∀size, m: nat.
     602  ∀size_proof: 0 < size.
     603    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
     604  normalize in size_proof; normalize @le_S_S assumption
     605qed.
     606   
     607axiom zero_add_head:
     608  ∀m: nat.
     609  ∀tl, hd.
     610    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
     611
     612lemma zero_add:
     613  ∀m: nat.
     614  ∀b: BitVector m.
     615    add m (zero m) b = b.
     616  #m #b elim b try %
     617  #m' #hd #tl #inductive_hypothesis
     618  <inductive_hypothesis in ⊢ (???%);
     619  >zero_add_head %
     620qed.
     621
     622axiom bitvector_of_nat_one_Sm:
     623  ∀m: nat.
     624    ∃b: BitVector m.
     625      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
     626
     627axiom increment_zero_bitvector_of_nat_1:
     628  ∀m: nat.
     629  ∀b: BitVector m.
     630    increment m b = add m (bitvector_of_nat m 1) b.
    540631
    541632axiom add_associative:
    542   ∀n: nat.
    543   ∀l, c, r: BitVector n.
    544     add … l (add … c r) = add … (add … l c) r.
     633  ∀m: nat.
     634  ∀l, c, r: BitVector m.
     635    add m l (add m c r) = add m (add m l c) r.
     636
     637lemma bitvector_of_nat_aux_buffer:
     638  ∀m, n: nat.
     639  ∀b: BitVector m.
     640    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
     641  #m #n elim n
     642  [1:
     643    #b change with (? = add ? (zero …) b)
     644    >zero_add %
     645  |2:
     646    #n' #inductive_hypothesis #b
     647    whd in match (bitvector_of_nat_aux ???);
     648    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
     649    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
     650    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
     651    <add_associative %
     652  ]
     653qed.
     654
     655definition sign_extension: Byte → Word ≝
     656  λc.
     657    let b ≝ get_index_v ? 8 c 1 ? in
     658      [[ b; b; b; b; b; b; b; b ]] @@ c.
     659  normalize
     660  repeat (@le_S_S)
     661  @le_O_n
     662qed.
     663
     664lemma bitvector_of_nat_sign_extension_equivalence:
     665  ∀m: nat.
     666  ∀size_proof: m < 128.
     667    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
     668  #m #size_proof whd in ⊢ (??%?);
     669  >most_significant_bit_zero
     670  [1:
     671    elim m
     672    [1:
     673      %
     674    |2:
     675      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
     676      whd in match (bitvector_of_nat_aux ???);
     677      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
     678      >(bitvector_of_nat_aux_buffer 16 n')
     679      cases daemon
     680    ]
     681  |2:
     682    assumption
     683  ]
     684qed.
    545685
    546686axiom add_commutative:

  • src/ASM/Assembly.ma

    r2101 r2108  
    604604qed.
    605605
    606 axiom eq_identifier_eq:
     606axiom eqb_succ_injective_Pos:
     607  ∀l, r: Pos.
     608    eqb (succ l) (succ r) = true → eqb l r = true.
     609
     610lemma eqb_true_to_refl_Pos:
     611  ∀l, r: Pos.
     612    eqb l r = true → l = r.
     613  #l #r @(pos_elim2 … l r)
     614  [1:
     615    #r cases r
     616    [1:
     617      #_ %
     618    |2,3:
     619      #l normalize in ⊢ (% → ?); #absurd destruct(absurd)
     620    ]
     621  |2:
     622    #l cases l
     623    [1:
     624      normalize in ⊢ (% → ?); #absurd destruct(absurd)
     625    |2,3:
     626      #l' normalize in ⊢ (% → ?); #absurd destruct(absurd)
     627    ]
     628  |3:
     629    #l #r #inductive_hypothesis #relevant @eq_f
     630    @inductive_hypothesis @eqb_succ_injective_Pos
     631    assumption
     632  ]
     633qed.
     634
     635lemma eq_identifier_eq:
    607636  ∀tag: String.
    608637  ∀l.
    609638  ∀r.
    610639    eq_identifier tag l r = true → l = r.
     640  #tag #l #r cases l cases r
     641  #pos_l #pos_r
     642  cases pos_l cases pos_r
     643  [1:
     644    #_ %
     645  |2,3,4,7:
     646    #p1_l normalize in ⊢ (% → ?);
     647    #absurd destruct(absurd)
     648  |5,9:
     649    #p1_l #p1_r normalize in ⊢ (% → ?);
     650    #relevant
     651    >(eqb_true_to_refl_Pos … relevant) %
     652  |*:
     653    #p_l #p_r normalize in ⊢ (% → ?);
     654    #absurd destruct(absurd)
     655  ]
     656qed.
    611657
    612658axiom neq_identifier_neq:
    … …  
    614660  ∀l, r: identifier tag.
    615661    eq_identifier tag l r = false → (l = r → False).
    616 
     662 
    617663(* label_map: identifier ↦ pseudo program counter *)
    618664definition label_map ≝ identifier_map ASMTag ℕ.

  • src/ASM/AssemblyProof.ma

    r2078 r2108  
    15211521  let datalabels ≝ construct_datalabels preamble in
    15221522  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
    1523     〈assembled,costs'〉 = assembly program length_proof sigma policy →
     1523    〈assembled,costs'〉 = assembly program sigma policy →
    15241524      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    15251525        let code_memory ≝ load_code_memory assembled in
    … …  
    15331533                  sigma newppc = add … pc (bitvector_of_nat … len).
    15341534  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
    1535   cases (assembly program length_proof sigma policy) * #assembled' #costs''
    1536   @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
    1537   @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
     1535  @pair_elim #preamble #instr_list #EQprogram
     1536  cases (assembly program sigma policy) * #assembled' #costs''
     1537  >EQprogram normalize nodelta
     1538  @pair_elim #labels #costs #EQcreate_label_cost_refl normalize nodelta
    15381539  #assembly_ok #Pair_eq destruct(Pair_eq) whd
    1539   #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
    1540   @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
    1541   lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] -assembly_ok
    1542   >eq_fetch_pseudo_instruction
     1540  #ppc #ppc_ok
     1541  @pair_elim #pi #newppc #EQfetch_pseudo_instruction
     1542  >EQprogram in sigma_policy_witness; #sigma_policy_witness
     1543  lapply (assembly_ok sigma_policy_witness ? ppc ?)
     1544  [2: >EQprogram in length_proof; #length_proof; assumption ] try assumption
     1545  >EQfetch_pseudo_instruction normalize nodelta
    15431546  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
    1544   >(? : assembly_1_pseudoinstruction ????? pi = 〈len,assembled〉)
    1545    [2: (*CSC: Provable, isn't it?*) cases daemon
    1546    | whd in ⊢ (% → ?); #assembly_ok
    1547   %
     1547  @pair_elim #len #assembledi #EQassembly_1_pseudo_instruction
     1548  letin lookup_labels ≝ (λx.sigma (bitvector_of_nat 16 (lookup_def ASMTag ℕ labels x O)))
     1549  letin lookup_datalabels ≝ (λx. lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16))
     1550  >(? : assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi = 〈len,assembledi〉)
     1551  [2: <EQassembly_1_pseudo_instruction % ]
     1552  whd in ⊢ (% → ?); #assembly_ok %
    15481553  [2: (*CSC: Use Jaap's invariant here *) cases daemon
    1549   | lapply (load_code_memory_ok assembled' ?) [(*CSC: Jaap?*) cases daemon]
     1554  |1:
     1555    lapply (load_code_memory_ok assembledi ?)
     1556    [1:
     1557      lapply sigma_policy_witness whd in match sigma_policy_specification;
     1558      normalize nodelta * #_ #relevant
     1559      (* XXX: wait for Jaap to propagate the property that program
     1560              is less than 2^16.
     1561       *)
     1562      cases daemon
     1563    ]
    15501564    #load_code_memory_ok
    1551     -eq_assembly_1_pseudoinstruction -program -policy -costs'' -labels -preamble -instr_list -costs -pi -newppc
    1552     cut (len=|assembled|) [(*CSC: provable before cleaning*) cases daemon] #EQlen
     1565    cut (len=|assembledi|)
     1566    [1: (*CSC: provable before cleaning *)
     1567        cases daemon
     1568    ]
     1569    #EQlen
    15531570    (* Nice statement here *)
    1554     cut (∀j. ∀H: j < |assembled|.
    1555           nth_safe Byte j assembled H =
     1571    cut (∀j. ∀H: j < |assembledi|.
     1572          nth_safe Byte j assembledi H =
    15561573          \snd (next (load_code_memory assembled')
    15571574          (bitvector_of_nat 16
    15581575           (nat_of_bitvector …
    15591576            (add … (sigma ppc) (bitvector_of_nat … j))))))
    1560     [(*CSC: is it provable?*) cases daemon
    1561     | -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
    1562       elim assembled
    1563        [ #pc #_ whd <add_zero %
     1577    [1:
     1578      cases daemon
     1579    |2:
     1580      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
     1581      elim assembledi
     1582      [1:
     1583        #pc #_ whd (* <add_zero %
    15641584       | #hd #tl #IH #pc #H %
    15651585         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
    … …  
    15721592           cases daemon
    15731593         ]
    1574     ]
     1594    ] *) cases daemon
     1595  ]
     1596  cases daemon
    15751597qed.
    15761598
    … …  
    15841606  ∀ppc.∀ppc_ok.
    15851607  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1586   let 〈assembled, costs'〉 ≝ pi1 … (assembly program length_proof sigma policy) in
     1608  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
    15871609  let code_memory ≝ load_code_memory assembled in
    15881610  let data_labels ≝ construct_datalabels (\fst program) in
    … …  
    16001622  letin lookup_datalabels ≝ (λx. ?)
    16011623  @pair_elim #pi #newppc #fetch_pseudo_refl
    1602   lapply (assembly_ok 〈preamble, instr_list〉 sigma ? policy sigma_policy_specification_witness assembled costs')
    1603   normalize nodelta
     1624  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
     1625  normalize nodelta try assumption
    16041626  @pair_elim #labels' #costs' #create_label_map_refl' #H
    16051627  lapply (H (sym_eq … assembled_refl)) -H
    … …  
    16681690definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
    16691691
     1692include alias "ASM/BitVectorTrie.ma".
     1693 
     1694include "common/AssocList.ma".
     1695
    16701696axiom low_internal_ram_of_pseudo_low_internal_ram:
    16711697 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    … …  
    16731699axiom high_internal_ram_of_pseudo_high_internal_ram:
    16741700 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    1675 
    1676 include "common/AssocList.ma".
    16771701
    16781702axiom low_internal_ram_of_pseudo_internal_ram_hit:
    … …  
    17601784            None ?       
    17611785        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
    1762  
    17631786
    17641787definition next_internal_pseudo_address_map ≝
    17651788 λM:internal_pseudo_address_map.
    17661789 λcm.
    1767   λs:PseudoStatus cm. λppc_ok.
    1768     next_internal_pseudo_address_map0 ?
    1769      (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M cm s.
     1790 λaddr_of.
     1791 λs:PseudoStatus cm.
     1792 λppc_ok.
     1793    next_internal_pseudo_address_map0 ? cm addr_of
     1794     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
    17701795
    17711796definition code_memory_of_pseudo_assembly_program:
    … …  
    22952320lemma snd_assembly_1_pseudoinstruction_ok:
    22962321  ∀program: pseudo_assembly_program.
     2322  ∀program_length_proof: |\snd program| < 2^16.
    22972323  ∀sigma: Word → Word.
    22982324  ∀policy: Word → bool.
    … …  
    23082334    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
    23092335      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
    2310   #program #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
     2336  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
    23112337  #lookup_labels #lookup_datalabels
    23122338  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
    … …  
    23162342  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
    23172343  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
    2318   lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs)
     2344  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
    23192345  @pair_elim #preamble #instr_list #program_refl
    23202346  @pair_elim #labels #costs' #create_label_cost_map_refl
    … …  
    23522378
    23532379(* XXX: easy but tedious *)
    2354 axiom assembly1_lt_128:
     2380lemma assembly1_lt_128:
    23552381  ∀i: instruction.
    23562382    |(assembly1 i)| < 128.
    2357 
    2358 axiom most_significant_bit_zero:
    2359   ∀size, m: nat.
    2360   ∀size_proof: 0 < size.
    2361     m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
    2362   normalize in size_proof; /2/
    2363 qed.
    2364 
    2365 lemma bitvector_of_nat_sign_extension_equivalence:
    2366   ∀m: nat.
    2367   ∀size_proof: m < 128.
    2368     sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
    2369   #m #size_proof whd in ⊢ (??%?);
    2370   >most_significant_bit_zero
    2371   [1:
    2372     cases daemon
    2373   |2:
    2374     assumption
    2375   |3:
    2376     //
     2383  #i cases i
     2384  try (#assm1 #assm2) try #assm1
     2385  [8:
     2386    cases assm1
     2387    try (#assm1 #assm2) try #assm1
     2388    whd in match assembly1; normalize nodelta
     2389    whd in match assembly_preinstruction; normalize nodelta
     2390    try @(subaddressing_mode_elim … assm2)
     2391    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
     2392    [32:
     2393      cases assm1 -assm1 #assm1 normalize nodelta
     2394      cases assm1 #addr1 #addr2 normalize nodelta
     2395      [1:
     2396        @(subaddressing_mode_elim … addr2)
     2397      |2:
     2398        @(subaddressing_mode_elim … addr1)
     2399      ]
     2400      #w
     2401    |35,36,37:
     2402      cases assm1 -assm1 #assm1 normalize nodelta
     2403      [1,3:
     2404        cases assm1 -assm1 #assm1 normalize nodelta
     2405      ]
     2406      cases assm1 #addr1 #addr2 normalize nodelta
     2407      @(subaddressing_mode_elim … addr2) try #w
     2408    |49:
     2409      cases assm1 -assm1 #assm1 normalize nodelta
     2410      [1:
     2411        cases assm1 -assm1 #assm1 normalize nodelta
     2412        [1:
     2413          cases assm1 -assm1 #assm1 normalize nodelta
     2414          [1:
     2415            cases assm1 -assm1 #assm1 normalize nodelta
     2416            [1:
     2417              cases assm1 -assm1 #assm1 normalize nodelta
     2418            ]
     2419          ]
     2420        ]
     2421      ]
     2422      cases assm1 #addr1 #addr2 normalize nodelta
     2423      [1,3,4,5:
     2424        @(subaddressing_mode_elim … addr2) try #w
     2425      |*:
     2426        @(subaddressing_mode_elim … addr1) try #w
     2427        normalize nodelta
     2428        [1,2:
     2429          @(subaddressing_mode_elim … addr2) try #w
     2430        ]
     2431      ]
     2432    |50:
     2433      cases assm1 -assm1 #assm1 normalize nodelta
     2434      cases assm1 #addr1 #addr2 normalize nodelta
     2435      [1:
     2436        @(subaddressing_mode_elim … addr2) try #w
     2437      |2:
     2438        @(subaddressing_mode_elim … addr1) try #w
     2439      ]
     2440    ]
     2441    normalize repeat @le_S_S @le_O_n
    23772442  ]
    2378 qed.
     2443  whd in match assembly1; normalize nodelta
     2444  [6:
     2445    normalize repeat @le_S_S @le_O_n
     2446  |7:
     2447    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
     2448  |*:
     2449    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
     2450  ]
     2451qed.

  • src/ASM/AssemblyProofSplit.ma

    r2047 r2108  
    405405include alias "ASM/Vector.ma".
    406406
    407 axiom main_lemma_preinstruction:
    408   ∀M, M': internal_pseudo_address_map.
    409   ∀preamble: preamble.
    410   ∀instr_list: list labelled_instruction.
    411   ∀cm: pseudo_assembly_program.
    412   ∀EQcm: cm = 〈preamble, instr_list〉.
    413   ∀sigma: Word → Word.
    414   ∀policy: Word → bool.
    415   ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
    416   ∀ps: PseudoStatus cm.
    417   ∀ppc: Word.
    418   ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
    419   ∀labels: label_map.
    420   ∀costs: BitVectorTrie costlabel 16.
    421   ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
    422   ∀newppc: Word.
    423   ∀lookup_labels: Identifier → Word.
    424   ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
    425   ∀lookup_datalabels: Identifier → Word.
    426   ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
    427   ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
    428   ∀instr: preinstruction Identifier.
    429   ∀ticks: nat × nat.
    430   ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
    431   ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
    432   ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
    433   ∀s: PreStatus pseudo_assembly_program cm.
    434   ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
    435   ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
    436   ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
    437               (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
    438                   lookup_datalabels (Instruction instr)))) →
    439               next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' →
    440                 fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
    441                   (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
    442                     ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
    443                       status_of_pseudo_status M' cm s sigma policy).
    444     P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
    445 
    446 (*
     407axiom sub16_with_carry_overflow:
     408  ∀left, right, result: BitVector 16.
     409  ∀flags: BitVector 3.
     410  ∀upper: BitVector 9.
     411  ∀lower: BitVector 7.
     412    sub_16_with_carry left right false = 〈result, flags〉 →
     413      vsplit bool 9 7 result = 〈upper, lower〉 →
     414        get_index_v bool 3 flags 2 ? = true →
     415          upper = [[true; true; true; true; true; true; true; true; true]].
     416  //
     417qed.
     418
    447419lemma main_lemma_preinstruction:
    448420  ∀M, M': internal_pseudo_address_map.
    … …  
    477449              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
    478450                  lookup_datalabels (Instruction instr)))) →
    479               next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' →
     451              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
    480452                fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
    481453                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
    … …  
    899871  [31,32: (* DJNZ *)
    900872  (* XXX: work on the right hand side *)
    901   >p normalize nodelta
     873  >p normalize nodelta >p1 normalize nodelta
    902874  (* XXX: switch to the left hand side *)
    903875  -instr_refl >EQP -P normalize nodelta
    904876  #sigma_increment_commutation #maps_assm #fetch_many_assm
    905877  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    906   whd in match (expand_relative_jump ????);
    907878  <EQppc in fetch_many_assm;
     879  whd in match (short_jump_cond ??);
     880  @pair_elim #sj_possible #disp
    908881  @pair_elim #result #flags #sub16_refl
    909882  @pair_elim #upper #lower #vsplit_refl
    910   cases (eq_bv ???) normalize nodelta
     883  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
     884  #sj_possible_pair destruct(sj_possible_pair)
     885  >p1 normalize nodelta
    911886  [1,3:
    912887    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    913888    whd in ⊢ (??%?);
     889    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
     890    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    914891    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    915892    (* XXX: work on the left hand side *)
    … …  
    927904    cases daemon
    928905  |2,4:
     906    XXX: here
    929907    >EQppc
    930908    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl

  • src/ASM/Interpret.ma

    r2062 r2108  
    33include "ASM/Fetch.ma".
    44include "ASM/AbstractStatus.ma".
    5 
    6 definition sign_extension: Byte → Word ≝
    7   λc.
    8     let b ≝ get_index_v ? 8 c 1 ? in
    9       [[ b; b; b; b; b; b; b; b ]] @@ c.
    10   normalize
    11   repeat (@le_S_S)
    12   @le_O_n
    13 qed.
    145   
    156lemma execute_1_technical:
Note: See TracChangeset for help on using the changeset viewer.