Ignore:
Timestamp:
Jun 16, 2011, 12:07:20 AM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r959 r971  
    924924   program counters. It is at the heart of the proof. *)
    925925(*CSC: code taken from build_maps *)
    926 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    927  λinstr_list.
     926definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     927 λinstr_list.λl:list labelled_instruction.
    928928  foldl ??
    929     (λt. λi.
     929   (λt,i.
    930930       match t with
    931931       [ None ⇒ None ?
     
    939939              let 〈pc,ignore〉 ≝ pc_ignore in
    940940              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
    941        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
    942        
    943 definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝
    944  λinstr_list.
    945   match sigma0 instr_list with
     941       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
     942
     943definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
     944 ≝ λprog.sigma00 prog (\snd prog).
     945
     946definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
     947 λprogram,instr_list.
     948  match sigma00 program instr_list with
    946949   [ None ⇒ None …
    947950   | Some result ⇒
    948951      let 〈ppc,pc_sigma_map〉 ≝ result in
    949        Some … pc_sigma_map ].
     952      let 〈pc,map〉 ≝ pc_sigma_map in
     953       Some … 〈ppc,pc〉 ].
    950954
    951955definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
     
    992996qed.
    993997
     998lemma does_not_occur_Some:
     999 ∀id,id',i,list_instr.
     1000  eq_bv ? id' id = false →
     1001   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
     1002    does_not_occur id list_instr.
     1003 #id #id' #i #list_instr elim list_instr
     1004  [ #H normalize in H ⊢ %; >H %
     1005  | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
     1006qed.
     1007
    9941008let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
    9951009 match l with
     
    10301044qed.
    10311045
    1032 axiom tech_pc_sigma0_append:
    1033  ∀preamble,instr_list,prefix,label,i,pc',code,ppc,pc,costs,costs'.
    1034   Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
    1035    construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    1036     tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.
    1037 
    1038 axiom tech_pc_sigma0_append_None:
    1039  ∀preamble,instr_list,prefix,i,ppc,pc,costs.
    1040   Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
    1041    construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     1046lemma occurs_exactly_once_Some:
     1047 ∀id,id',i,prefix.
     1048  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
     1049 #id #id' #i #prefix elim prefix
     1050  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1051    change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
     1052  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1053    cases he; normalize nodelta
     1054     [ #H @ (IH H)
     1055     | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
     1056       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv 16 x id) normalize nodelta;
     1057       [ #H  | #H @IH @H]
     1058qed.
     1059
     1060axiom tech_pc_sigma00_append_Some:
     1061 ∀program,prefix,costs,label,i,pc',code,ppc,pc.
     1062  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
     1063   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
     1064    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
     1065
     1066axiom tech_pc_sigma00_append_None:
     1067 ∀program,prefix,i,ppc,pc,costs.
     1068  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
     1069   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    10421070    → False.
    10431071
    1044 (*
    10451072definition build_maps' ≝
    10461073  λpseudo_program.
    1047   let 〈preamble,instr_list〉 ≝ pseudo_program in
    10481074  let result ≝
    10491075   foldl_strong
    10501076    (option Identifier × pseudo_instruction)
    1051     (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    1052       let pre' ≝ 〈preamble,pre〉 in
    1053       let 〈labels,pc_costs〉 ≝ res in
    1054        tech_pc_sigma0 pre' = Some … pc_costs ∧
     1077    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
     1078      let 〈labels,ppc_pc_costs〉 ≝ res in
     1079      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
     1080      let 〈pc',costs〉 ≝ pc_costs in
     1081       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
    10551082       ∀id. occurs_exactly_once id pre →
    1056         lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
    1057     instr_list
     1083        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
     1084    (\snd pseudo_program)
    10581085    (λprefix,i,tl,prf,t.
    1059       let 〈labels, pc_costs〉 ≝ t in
    1060       let 〈program_counter, costs〉 ≝ pc_costs in
     1086      let 〈labels, ppc_pc_costs〉 ≝ t in
     1087      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
     1088      let 〈pc,costs〉 ≝ pc_costs in
    10611089       let 〈label, i'〉 ≝ i in
    10621090       let labels ≝
     
    10641092         [ None ⇒ labels
    10651093         | Some label ⇒
    1066            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     1094           let program_counter_bv ≝ bitvector_of_nat ? pc in
    10671095             insert ? ? label program_counter_bv labels
    10681096         ]
    10691097       in
    1070          match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
     1098         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
    10711099         [ None ⇒
    1072             let dummy ≝ 〈labels,pc_costs〉 in
     1100            let dummy ≝ 〈labels,ppc_pc_costs〉 in
    10731101             dummy
    1074          | Some construct ⇒ 〈labels, construct
     1102         | Some construct ⇒ 〈labels, 〈S ppc,construct〉
    10751103         ]
    1076     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
     1104    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
    10771105  in
    1078    let 〈labels, pc_costs〉 ≝ result in
     1106   let 〈labels, ppc_pc_costs〉 ≝ result in
     1107   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    10791108   let 〈pc, costs〉 ≝ pc_costs in
    10801109    〈labels, costs〉.
    10811110 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
    1082  | whd cases construct in p3 #PC #CODE #JMEQ %
    1083     [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ)) | #id #Hid ]
    1084  | (* dummy case *) @⊥
    1085    @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ]
    1086  [*: generalize in match (sig2 … t) whd in ⊢ (% → ?)
    1087      >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ]
    1088  whd in ⊢ (??(????%?)?) -labels1;
    1089  cases label in Hid
    1090   [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
    1091      [ >(address_of_word_labels_code_mem_None … Hid)
    1092        (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
    1093      | whd in Hid >occurs_exactly_once_None in Hid // ]
    1094   | -label #label #Hid whd in ⊢ (??(????%?)?)
    1095    
    1096   ]
     1111 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2
     1112   cases construct in p4 #PC #CODE #JMEQ %
     1113   [ @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
     1114   | #id normalize nodelta; -labels1; cases label; normalize nodelta
     1115     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
     1116     | #l
     1117     ]]
     1118 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2
     1119   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
    10971120qed.
    10981121
Note: See TracChangeset for help on using the changeset viewer.