Changeset 1957


Ignore:
Timestamp:
May 16, 2012, 3:53:46 PM (7 years ago)
Author:
mulligan
Message:

Stitching proofs back together after slight change in statement of assembly_ok.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1955 r1957  
    14971497   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
    14981498*)
    1499 axiom assembly_ok:
     1499lemma assembly_ok:
    15001500  ∀program.
    15011501  ∀sigma: Word → Word.
     
    15031503  ∀assembled.
    15041504  ∀costs'.
    1505   let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     1505  let 〈preamble, instr_list〉 ≝ program in
     1506  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
    15061507  〈assembled,costs'〉 = assembly program sigma policy →
    15071508  costs = costs' ∧
     
    15171518   encoding_check code_memory pc pc_plus_len assembled ∧
    15181519       sigma newppc = add … pc (bitvector_of_nat … len).
     1520  #program #sigma #policy #assembled #costs'
     1521  @pair_elim #preamble #instr_list #program_refl
     1522  @pair_elim #labels #costs #create_label_cost_refl
     1523  #assembly_refl %
     1524  [1:
     1525    >(?: costs = \snd (create_label_cost_map instr_list))
     1526    [1:
     1527      >(?: costs' = \snd (assembly program sigma policy))
     1528      [1:
     1529        whd in match assembly; normalize nodelta
     1530        >program_refl normalize nodelta
     1531        >create_label_cost_refl in ⊢ (???%); normalize nodelta
     1532        whd in match create_label_cost_map; normalize nodelta
     1533        whd in match create_label_cost_map0; normalize nodelta
     1534      |2:
     1535        <assembly_refl %
     1536      ]
     1537    |2:
     1538      >create_label_cost_refl %
     1539    ]
     1540  |2:
     1541  ]
     1542  cases daemon (* XXX: !!! *)
     1543qed.
    15191544
    15201545(* XXX: should we add that costs = costs'? *)
     
    15421567  @pair_elim #pi #newppc #fetch_pseudo_refl
    15431568  lapply (assembly_ok 〈preamble, instr_list〉 sigma policy assembled costs')
     1569  normalize nodelta
    15441570  @pair_elim #labels' #costs' #create_label_map_refl' #H
    15451571  cases (H (sym_eq … assembled_refl))
     
    21992225    | _ ⇒ True
    22002226    ].
     2227
     2228lemma pair_destruct_right:
     2229  ∀A: Type[0].
     2230  ∀B: Type[0].
     2231  ∀a, c: A.
     2232  ∀b, d: B.
     2233    〈a, b〉 = 〈c, d〉 → b = d.
     2234  #A #B #a #b #c #d //
     2235qed.
    22012236   
    22022237(*CSC: ???*)
     
    22362271  letin costs ≝ (\snd (assembly program sigma policy))
    22372272  lapply (assembly_ok program sigma policy assembled costs)
     2273  @pair_elim #preamble #instr_list #program_refl
    22382274  @pair_elim #labels #costs' #create_label_cost_map_refl
    22392275  <eq_pair_fst_snd #H cases (H (refl …)) -H #costs_refl #H
     
    22492285  whd in match (fetch_pseudo_instruction ??);
    22502286  @pair_elim #lbl #instr #nth_refl normalize nodelta
    2251   #G destruct %
     2287  #G cases (pair_destruct_right ?????? G) %
    22522288qed.
    22532289
Note: See TracChangeset for help on using the changeset viewer.