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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.
Note: See TracChangeset for help on using the changeset viewer.