Changeset 2057


Ignore:
Timestamp:
Jun 13, 2012, 1:30:57 PM (5 years ago)
Author:
sacerdot
Message:

Repaired (was broken by fetch_pseudo_instruction now taking a proof obligation)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2032 r2057  
    14491449  ∀policy: Word → bool.
    14501450  let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
    1451   ∀ppc.
     1451  ∀ppc.∀ppc_ok.
    14521452  ∀code_memory.
    14531453  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    1454   let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
     1454  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
    14551455  let pc ≝ sigma ppc in
    14561456  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     
    14591459    encoding_check code_memory pc pc_plus_len assembled →
    14601460      fetch_many code_memory pc_plus_len pc instructions.
    1461   #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory
     1461  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
    14621462  letin lookup_datalabels ≝ (λx.?)
    14631463  letin pi ≝ (fst ???)
     
    14831483  λsigma: Word → Word.
    14841484  λpolicy: Word → bool.
    1485   ∀ppc: Word.
    1486     let 〈preamble, instr_list〉 ≝ program in
     1485  ∀ppc: Word. ∀ppc_ok.
     1486    let instr_list ≝ \snd program in
    14871487    let pc ≝ sigma ppc in
    14881488    let labels ≝ \fst (create_label_cost_map instr_list) in
    14891489    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    1490     let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc) in
     1490    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    14911491    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
    14921492      And (nat_of_bitvector … ppc ≤ |instr_list| →
     
    15421542        let code_memory ≝ load_code_memory assembled in
    15431543        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
    1544           ∀ppc.
    1545             let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in     
     1544          ∀ppc.∀ppc_ok.
     1545            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
    15461546            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    15471547            let pc ≝ sigma ppc in
     
    15541554  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
    15551555  #assembly_ok #Pair_eq destruct(Pair_eq) whd
    1556   #ppc @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
     1556  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
    15571557  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
    15581558  lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] -assembly_ok
     
    15981598  ∀policy.
    15991599  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    1600   ∀ppc.
     1600  ∀ppc.∀ppc_ok.
    16011601  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    16021602  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
     
    16051605  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
    16061606  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    1607   let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     1607  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
    16081608  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    16091609    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
    1610   * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc
     1610  * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
    16111611  @pair_elim #labels #costs #create_label_map_refl
    16121612  @pair_elim #assembled #costs' #assembled_refl
     
    16241624  #len #assembledi #EQ4 #H
    16251625  lapply (H ppc) >fetch_pseudo_refl #H
    1626   lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled))
    1627   >EQ4 #H1 cases H
     1626  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
     1627  >EQ4 #H1 cases (H ppc_ok)
    16281628  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
    16291629  >fetch_pseudo_refl in H1; #assm @assm assumption
     
    17731773 λM:internal_pseudo_address_map.
    17741774 λcm.
    1775   λs:PseudoStatus cm.
     1775  λs:PseudoStatus cm. λppc_ok.
    17761776    next_internal_pseudo_address_map0 ?
    1777      (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s))) M cm s.
     1777     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M cm s.
    17781778
    17791779definition code_memory_of_pseudo_assembly_program:
     
    20852085definition ticks_of:
    20862086    ∀p:pseudo_assembly_program.
    2087       (Word → Word) → (Word → bool) → Word → nat × nat ≝
     2087      (Word → Word) → (Word → bool) → ∀ppc:Word.
     2088       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
    20882089  λprogram: pseudo_assembly_program.
    20892090  λsigma.
    20902091  λpolicy.
    2091   λppc: Word.
    2092     let 〈preamble, pseudo〉 ≝ program in
    2093     let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
     2092  λppc: Word. λppc_ok.
     2093    let pseudo ≝ \snd program in
     2094    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
    20942095     ticks_of0 program sigma policy ppc fetched.
    20952096
     
    22882289  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    22892290  ∀ppc: Word.
    2290   ∀ppc_in_bounds: nat_of_bitvector 16 ppc |\snd program|.
     2291  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
    22912292  ∀pi.
    22922293  ∀lookup_labels.
     
    22942295    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
    22952296    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    2296     \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     2297    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
    22972298    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
    22982299      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
     
    23092310  @pair_elim #labels #costs' #create_label_cost_map_refl
    23102311  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
    2311   lapply (H ppc) -H
     2312  lapply (H ppc ppc_in_bounds) -H
    23122313  @pair_elim #pi' #newppc #fetch_pseudo_refl'
    23132314  @pair_elim #len #assembled #assembly1_refl #H
     
    23212322  <sigma_newppc_refl
    23222323  generalize in match fetch_pseudo_refl';
    2323   (* XXX: use ppc_in_bounds to get rid of the cases not_implemented in
    2324           fetch_pseudo_instruction, as this is exactly what we need now!
    2325   *)
    2326   whd in match (fetch_pseudo_instruction ??);
     2324  whd in match (fetch_pseudo_instruction ???);
    23272325  @pair_elim #lbl #instr #nth_refl normalize nodelta
    2328   #G cases (pair_destruct_right ?????? G)
    2329   lapply (sigma_policy_specification_witness ppc)
    2330   >program_refl normalize nodelta #policy_hyp
    2331   cases policy_hyp -policy_hyp #policy_hyp1 #_
    2332   >policy_hyp1
    2333   [1:
    2334     -policy_hyp1 whd in match instruction_size; normalize nodelta
    2335     <pi_refl' >(?: pi' = \fst (fetch_pseudo_instruction (\snd program) ppc))
    2336     [1: >program_refl % ] >fetch_pseudo_refl' %
    2337   |2:
    2338     >program_refl in ppc_in_bounds; #relevant assumption
    2339   ]
     2326  #G cases (pair_destruct_right ?????? G) %
    23402327qed.
    23412328
Note: See TracChangeset for help on using the changeset viewer.