Changeset 1934


Ignore:
Timestamp:
May 10, 2012, 3:37:07 PM (7 years ago)
Author:
boender
Message:
  • various & sundry moves of lemmas to better places
  • integrated Policy and Assembly
Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1928 r1934  
    529529    full_add n b c false.
    530530
     531example half_add_SO:
     532 ∀pc.
     533 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     534 cases daemon.
     535qed.
     536
    531537definition sign_bit : ∀n. BitVector n → bool ≝
    532538λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
  • src/ASM/Assembly.ma

    r1925 r1934  
    419419
    420420definition expand_relative_jump_internal:
    421  ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
     421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word × bool.
    422422 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
    423423 list instruction
    424424 ≝
    425   λlookup_labels.λsigma.λlbl.λpc,i.
    426    let lookup_address ≝ sigma (lookup_labels lbl) in
     425  λlookup_labels.λsigma.λlbl.λppc,i.
     426   let lookup_address ≝ \fst (sigma (lookup_labels lbl)) in
     427   let pc ≝ \fst (sigma ppc) in
    427428   let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
    428429   let 〈upper, lower〉 ≝ split ? 8 8 result in
     
    470471  preinstruction Identifier → list instruction ≝
    471472  λlookup_labels: Identifier → Word.
    472   λsigma:Word → Word.
    473   λpc: Word.
     473  λsigma:Word → Word × bool.
     474  λppc: Word.
    474475  (*λjmp_len: jump_length.*)
    475476  λi: preinstruction Identifier.
    476   let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
     477  (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*)
    477478  match i with
    478   [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JC ?)
    479   | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNC ?)
    480   | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JB ? baddr)
    481   | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JZ ?)
    482   | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNZ ?)
    483   | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JBC ? baddr)
    484   | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNB ? baddr)
    485   | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (CJNE ? addr)
    486   | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (DJNZ ? addr)
     479  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JC ?)
     480  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNC ?)
     481  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JB ? baddr)
     482  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JZ ?)
     483  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNZ ?)
     484  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JBC ? baddr)
     485  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNB ? baddr)
     486  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (CJNE ? addr)
     487  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (DJNZ ? addr)
    487488  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
    488489  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
     
    518519 ∀lookup_labels.∀sigma.Word → ? → pseudo_instruction → list instruction ≝
    519520  λlookup_labels:Identifier → Word.
    520   λsigma:Word → Word.
    521   λpc.
     521  λsigma:Word → Word × bool.
     522  λppc.
    522523  λlookup_datalabels:Identifier → Word.
    523524  λi.
     
    526527  | Comment comment ⇒ [ ]
    527528  | Call call ⇒
    528     let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
    529     let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
    530     if eq_bv ? ignore fst_5 then
    531       let address ≝ ADDR11 address in
     529    let 〈addr_5, resta〉 ≝ split ? 5 11 (\fst (sigma (lookup_labels call))) in
     530    let 〈pc, do_a_long〉 ≝ sigma ppc in
     531    let 〈pc_5, restp〉 ≝ split ? 5 11 pc in
     532    if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
     533      let address ≝ ADDR11 resta in
    532534        [ ACALL address ]
    533535    else
    534       let address ≝ ADDR16 (lookup_labels call) in
     536      let address ≝ ADDR16 (\fst (sigma (lookup_labels call))) in
    535537        [ LCALL address ]
    536538  | Mov d trgt ⇒
    537539    let address ≝ DATA16 (lookup_datalabels trgt) in
    538540      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
    539   | Instruction instr ⇒ expand_relative_jump lookup_labels sigma pc instr
     541  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
    540542  | Jmp jmp ⇒
    541     let 〈result, flags〉 ≝ sub_16_with_carry pc (lookup_labels jmp) false in
     543    let 〈pc, do_a_long〉 ≝ sigma ppc in
     544    let lookup_address ≝ \fst (sigma (lookup_labels jmp)) in
     545    let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
    542546    let 〈upper, lower〉 ≝ split ? 8 8 result in
    543     if eq_bv ? upper (zero 8) then
     547    if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
    544548      let address ≝ RELATIVE lower in
    545549        [ SJMP address ]
     
    547551      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in
    548552      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
    549       if eq_bv ? fst_5_addr fst_5_pc then
     553      if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
    550554        let address ≝ ADDR11 rest_addr in
    551555          [ AJMP address ]
    552556      else   
    553         let address ≝ ADDR16 (lookup_labels jmp) in
     557        let address ≝ ADDR16 lookup_address in
    554558        [ LJMP address ]
    555559  ].
     
    604608  λlookup_labels.
    605609  λsigma.
    606   (*λppc: Word.*)
    607   λpc: Word.
     610  λppc: Word.
    608611  λlookup_datalabels.
    609612  λi.
    610   let pseudos ≝ expand_pseudo_instruction lookup_labels sigma pc lookup_datalabels i in
     613  let pseudos ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels i in
    611614  let mapped ≝ map ? ? assembly1 pseudos in
    612615  let flattened ≝ flatten ? mapped in
     
    614617   〈pc_len, flattened〉.
    615618
    616 definition construct_costs ≝
    617   (*X?*)λlookup_labels.
    618   λsigma.
    619   λprogram_counter: nat.
    620   λpseudo_program_counter: nat.
    621   λcosts: BitVectorTrie costlabel 16.
    622   λi.
    623   match i with
    624   [ Cost cost ⇒
    625     let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    626      〈program_counter, (insert … program_counter_bv cost costs)〉
    627   | _ ⇒
    628     let pc_bv ≝ bitvector_of_nat ? program_counter in
    629     (*let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in*)
    630     let lookup_datalabels ≝ λx.zero ? in
    631     let pc_delta_assembled ≝
    632       assembly_1_pseudoinstruction (*X?(λx.pc_bv)*) lookup_labels
    633        sigma (*ppc_bv*) pc_bv lookup_datalabels i in
    634     let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
    635      〈pc_delta + program_counter, costs〉
    636   ].
    637  
    638 axiom nat_of_bitvector_bitvector_of_nat:
    639   ∀n,v.n < 2^v → nat_of_bitvector v (bitvector_of_nat v n) = n.
    640  
    641 axiom bitvector_of_nat_nat_of_bitvector:
    642   ∀n,v.bitvector_of_nat n (nat_of_bitvector n v) = v.
    643 
    644 lemma nth_cons:
    645   ∀n,A,h,t,y.
    646   nth (S n) A (h::t) y = nth n A t y.
    647  #n #A #h #t #y /2 by refl/
    648 qed.
    649  
     619definition instruction_size ≝
     620 λlookup_labels.λsigma.λppc.λi.
     621  \fst (assembly_1_pseudoinstruction lookup_labels sigma ppc (λx.zero …) i).
     622
     623(* Jaap: never used
    650624lemma fetch_pseudo_instruction_prefix:
    651625  ∀prefix.∀x.∀ppc.ppc < (|prefix|) →
     
    665639 ]
    666640qed.
     641*)
    667642
    668643(*
     
    834809qed.*)
    835810
    836 example half_add_SO:
    837  ∀pc.
    838  \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
    839  cases daemon.
    840 qed.
    841 
    842811(*CSC: Main axiom here, needs to be proved soon! *)
    843812(*lemma snd_assembly_1_pseudoinstruction_ok:
     
    881850qed.*)
    882851
     852(*CSC: FALSE!!!*)
    883853axiom fetch_pseudo_instruction_split:
    884854 ∀instr_list,ppc.
     
    10811051*)
    10821052
    1083 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
    1084  #A #a #b #EQ destruct //
    1085 qed.
    1086 
    10871053(*
    10881054lemma tech_pc_sigma00_append_Some:
     
    11211087   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *)
    11221088
    1123 axiom eq_identifier_eq:
     1089(*axiom eq_identifier_eq:
    11241090  ∀tag: String.
    11251091  ∀l.
     
    11311097  ∀l, r: identifier tag.
    11321098    eq_identifier tag l r = false → (l = r → False).
    1133 
    1134 definition build_maps0:
    1135  ∀pseudo_program:pseudo_assembly_program.∀sigma:Word → Word.
    1136   Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
    1137    let 〈labels, costs〉 ≝ res in
    1138     ∀id. occurs_exactly_once ?? id (\snd pseudo_program) →
    1139      lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
    1140   λpseudo_program.
    1141   λsigma.
    1142     let result ≝
    1143       foldl_strong
    1144         (option Identifier × pseudo_instruction)
    1145           (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
    1146             let 〈labels,ppc_pc_costs〉 ≝ res in
    1147             let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    1148             let 〈pc',costs〉 ≝ pc_costs in
    1149               And ( And (
    1150               And (bitvector_of_nat ? pc' = sigma (bitvector_of_nat ? ppc')) (*∧*)
    1151                 (ppc' = length … pre)) (*∧ *)
    1152                 (*(tech_pc_sigma00 pseudo_program (pi1 … pol) pre = 〈ppc',pc'〉)*) True) (*∧*)
    1153                 (∀id. occurs_exactly_once ?? id pre →
    1154                   lookup_def … labels id (zero …) = sigma (address_of_word_labels_code_mem pre id)))
    1155                 (\snd pseudo_program)
    1156         (λprefix,i,tl,prf,t.
    1157           let 〈labels, ppc_pc_costs〉 ≝ t in
    1158           let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
    1159           let 〈pc,costs〉 ≝ pc_costs in
    1160           let 〈label, i'〉 ≝ i in
    1161           let labels ≝
    1162             match label with
    1163             [ None ⇒ labels
    1164             | Some label ⇒
    1165                 let program_counter_bv ≝ bitvector_of_nat ? pc in
    1166                   add ? ? labels label program_counter_bv
    1167             ]
    1168           in
    1169             let construct ≝ construct_costs (λid.lookup_def … labels id (zero ?)) sigma
    1170               pc ppc costs i' in
    1171               〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
    1172     in
    1173       let 〈labels, ppc_pc_costs〉 ≝ result in
    1174       let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    1175       let 〈pc, costs〉 ≝ pc_costs in
    1176         〈labels, costs〉.
    1177 (* [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    1178    generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
    1179    [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
    1180    | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
    1181    | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
    1182    | #id normalize nodelta; -labels1; cases label; normalize nodelta
    1183      [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
    1184      | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
    1185        generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
    1186         [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
    1187           <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H]
    1188         | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
    1189           (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL)
    1190           lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
    1191           <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
    1192  |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ]
    1193  | generalize in match (pi2 … result) in ⊢ ?;
    1194    normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
    1195    normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H] *)
    1196  cases daemon
    1197 qed.
    1198 
    1199 definition build_maps:
    1200  ∀pseudo_program.∀sigma.
    1201   (identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)
    1202  ≝ λpseudo_program,sigma. build_maps0 pseudo_program sigma.
    1203 
    1204 theorem build_maps_ok:
     1099*)
     1100
     1101(* label_map: identifier ↦ pseudo program counter *)
     1102definition label_map ≝ identifier_map ASMTag ℕ.
     1103
     1104(* Labels *)
     1105definition is_label ≝
     1106  λx:labelled_instruction.λl:Identifier.
     1107  let 〈lbl,instr〉 ≝ x in
     1108  match lbl with
     1109  [ Some l' ⇒ l' = l
     1110  | _       ⇒ False
     1111  ].
     1112
     1113lemma label_does_not_occur:
     1114  ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier.
     1115  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.
     1116 #i #p #l generalize in match i; elim p
     1117 [ #i >nth_nil #H cases H
     1118 | #h #t #IH #i cases i -i
     1119   [ cases h #hi #hp cases hi
     1120     [ normalize #H cases H
     1121     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
     1122       whd in Heq; >Heq
     1123       >eq_identifier_refl / by refl/
     1124     ]
     1125   | #i #H whd in match (does_not_occur ????);
     1126     whd in match (instruction_matches_identifier ????);
     1127     cases h #hi #hp cases hi normalize nodelta
     1128     [ @(IH i) @H
     1129     | #l' @eq_identifier_elim
     1130       [ normalize / by /
     1131       | normalize #_ @(IH i) @H
     1132       ]
     1133     ]
     1134   ]
     1135 ]
     1136qed.
     1137
     1138(* The function that creates the label-to-address map *)
     1139definition create_label_cost_map: ∀program:list labelled_instruction.
     1140  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
     1141    let 〈labels,costs〉 ≝ labels_costs in
     1142    ∀i:ℕ.lt i (|program|) →
     1143    ∀l.occurs_exactly_once ?? l program →
     1144    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
     1145    lookup ?? labels l = Some ? i
     1146  ) ≝
     1147  λprogram.
     1148  \fst (foldl_strong (option Identifier × pseudo_instruction)
     1149  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × nat.
     1150    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
     1151    ppc = |prefix| ∧
     1152    ∀i:ℕ.lt i (|prefix|) →
     1153    ∀l.occurs_exactly_once ?? l prefix →
     1154    is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
     1155    lookup … labels l = Some ? i
     1156  )
     1157  program
     1158  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
     1159   let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
     1160   let 〈label,instr〉 ≝ x in
     1161   let labels ≝
     1162     match label with
     1163     [ None   ⇒ labels
     1164     | Some l ⇒ add … labels l ppc
     1165     ] in
     1166   let costs ≝
     1167     match instr with
     1168     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
     1169     | _ ⇒ costs ] in
     1170      〈labels,costs,S ppc〉
     1171   ) 〈(empty_map …),(Stub ??),0〉).
     1172[2: normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
     1173  -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
     1174 inversion label [#EQ | #l #EQ]
     1175 [1,2: normalize nodelta
     1176   #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     1177  [3: #Hi #lbl #Hocc #Hlbl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc
     1178    @eq_identifier_elim
     1179    [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl
     1180      @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/
     1181    | #Heq #Hocc normalize in Hocc; >lookup_add_miss
     1182      [ @(IH2 … i (le_S_S_to_le … Hi))
     1183        [ @Hocc
     1184        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
     1185        ]
     1186      | @sym_neq @Heq
     1187      ]
     1188    ]
     1189  |4: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
     1190    [ <minus_n_n #Hl normalize in Hl; >Hl >IH1 @lookup_add_hit
     1191    | @le_n
     1192    ]
     1193  |1: #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl
     1194    @(IH2 … i (le_S_S_to_le … Hi))
     1195    [ @Hocc
     1196    | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
     1197    ]
     1198  |2: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
     1199    [ <minus_n_n #Hl cases Hl
     1200    | @le_n
     1201    ]
     1202  ]
     1203 ]
     1204| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
     1205  #i #Hi normalize in Hi; cases (not_le_Sn_O i) #abs cases (abs Hi)
     1206| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
     1207  #_ #H @H
     1208]
     1209qed.
     1210
     1211(*theorem build_maps_ok:
    12051212 ∀pseudo_program.∀sigma:Word → Word.
    12061213   let 〈labels, costs〉 ≝ build_maps pseudo_program sigma in
     
    12081215     lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id).
    12091216 #pseudo_program #sigma @(pi2 … (build_maps0 … sigma))
    1210 qed.
     1217qed.*)
    12111218
    12121219definition assembly:
    1213  ∀p:pseudo_assembly_program.∀sigma:Word → Word.list Byte × (BitVectorTrie costlabel 16) ≝
     1220 ∀p:pseudo_assembly_program.∀sigma:Word → Word × bool.list Byte × (BitVectorTrie costlabel 16) ≝
    12141221  λp.let 〈preamble, instr_list〉 ≝ p in
    12151222   λsigma.
    1216     let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 sigma in
     1223    let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    12171224    let datalabels ≝ construct_datalabels preamble in
    1218     let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
     1225    let lookup_labels ≝ λx. \fst (sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0))) in
    12191226    let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    12201227    let result ≝
     
    12391246      〈(zero ?), 〈(zero ?), [ ]〉〉
    12401247    in
    1241      〈\snd (\snd result), costs〉.
    1242  cases daemon
     1248     〈\snd (\snd result),
     1249      fold … (λppc.λcost.λpc_to_costs. insert … (\fst (sigma ppc)) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
     1250 @pair_elim normalize nodelta #x #y #z @pair_elim normalize nodelta #w1 #w2 #w3 #w4 @pair_elim //
    12431251qed.
    12441252
  • src/ASM/Policy.ma

    r1933 r1934  
    1414(* Internal types *)
    1515
    16 (* label_map: identifier ↦ pseudo program counter *)
    17 definition label_map ≝ identifier_map ASMTag ℕ.
    18 
    1916(* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *)
    20 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × (option jump_length)) 16).
     17definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × bool) 16).
    2118
    2219(* The different properties that we want/need to prove at some point *)
     
    7269  ].
    7370 
    74 definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
     71(*definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
    7572  λprefix.λsigma.
    7673  ∀i:ℕ.i < |prefix| →
    7774  iff (is_jump (nth i ? prefix 〈None ?, Comment []〉))
    7875   (∃x:jump_length.
    79    \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).
     76   \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).*)
    8077
    8178(* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
     
    111108 λprogram.λop.λp.
    112109 ∀i.i < |program| →
    113    let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,None ?〉 in
    114    let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,None ?〉 in
    115      opc ≤ pc ∧
    116      match ox with
     110   let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,false〉 in
     111   let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,false〉 in
     112     opc ≤ pc.
     113     (*∧ match ox with
    117114     [ Some oj ⇒
    118115       match x with
     
    121118       ]
    122119     | _ ⇒ True
    123      ].
     120     ].*)
     121
     122(*
    124123
    125124(* Policy safety *)
    126 definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
     125(*definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    127126 λprogram.λlabels.λsigma.
    128127 ∀i.i < |program| →
    129  let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉 in
     128 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,false〉 in
    130129 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in
    131130 ∀dest.is_jump_to instr dest →
    132131   let paddr ≝ lookup_def … labels dest 0 in
    133    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,None ?〉) in
     132   let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,false〉) in
    134133   match j with
    135134   [ None ⇒ True
     
    147146     | long_jump   ⇒ True
    148147     ]
    149    ].
     148   ].*)
    150149
    151150(* this is the instruction size as determined by the distance from origin to destination *)
     
    291290  %2 @nmk #H destruct (H)
    292291qed.
    293 
    294 (* Labels *)
    295 definition is_label ≝
    296   λx:labelled_instruction.λl:Identifier.
    297   let 〈lbl,instr〉 ≝ x in
    298   match lbl with
    299   [ Some l' ⇒ l' = l
    300   | _       ⇒ False
    301   ].
    302 
    303 lemma label_does_not_occur:
    304   ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier.
    305   is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.
    306  #i #p #l generalize in match i; elim p
    307  [ #i >nth_nil #H cases H
    308  | #h #t #IH #i cases i -i
    309    [ cases h #hi #hp cases hi
    310      [ normalize #H cases H
    311      | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
    312        whd in Heq; >Heq
    313        >eq_identifier_refl / by refl/
    314      ]
    315    | #i #H whd in match (does_not_occur ????);
    316      whd in match (instruction_matches_identifier ????);
    317      cases h #hi #hp cases hi normalize nodelta
    318      [ @(IH i) @H
    319      | #l' @eq_identifier_elim
    320        [ normalize / by /
    321        | normalize #_ @(IH i) @H
    322        ]
    323      ]
    324    ]
    325  ]
    326 qed.
    327292 
    328293definition policy_isize_sum ≝
     
    343308    lookup ?? labels l = Some ? i
    344309  ) ≝
    345   λprogram.
    346   foldl_strong (option Identifier × pseudo_instruction)
    347   (λprefix.Σlabels:label_map.
    348     ∀i:ℕ.lt i (|prefix|) →
    349     ∀l.occurs_exactly_once ?? l prefix →
    350     is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    351     lookup … labels l = Some ? i
    352   )
    353   program
    354   (λprefix.λx.λtl.λprf.λlabels.
    355    let 〈label,instr〉 ≝ x in
    356      match label with
    357      [ None   ⇒ labels
    358      | Some l ⇒ add … labels l (|prefix|)
    359      ]
    360    ) (empty_map …).
    361 [1,2: #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    362   [ #Hi #lbl #Hocc #Hlbl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc
    363     @eq_identifier_elim
    364     [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl
    365       @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/
    366     | #Heq #Hocc normalize in Hocc; >lookup_add_miss
    367       [ @(pi2 … labels i (le_S_S_to_le … Hi))
    368         [ @Hocc
    369         | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    370         ]
    371       | @sym_neq @Heq
    372       ]
    373     ]
    374   | #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
    375     [ <minus_n_n #Hl normalize in Hl; >Hl @lookup_add_hit
    376     | @le_n
    377     ]
    378   | #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl
    379     @(pi2 … labels i (le_S_S_to_le … Hi))
    380     [ @Hocc
    381     | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    382     ]
    383   | #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
    384     [ <minus_n_n #Hl cases Hl
    385     | @le_n
    386     ]
    387   ]
    388 | #i #Hi #l #Hl cases Hl
    389 ]
     310 λprogram.
     311 
    390312qed.
    391313
     
    19461868] *)
    19471869qed.
     1870*)
    19481871
    19491872(* The glue between Policy and Assembly. *)
    19501873definition jump_expansion':
    19511874 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    1952  Σf:ℕ → ℕ × (option jump_length).
    1953    ∀ppc.match je_fixpoint (\snd program) with
    1954    [ None ⇒ True
    1955    | Some pol ⇒ \fst (f ppc) +
    1956       (instruction_size_sigma (create_label_map (\snd program)) pol (bitvector_of_nat ? (\fst (f ppc)))
    1957       (\snd (nth ppc ? (\snd program) 〈None ?, Comment []〉)))
    1958      = \fst (f (S ppc))
    1959    ] ≝
     1875  option (Σsigma:Word → Word × bool.
     1876   ∀ppc.
     1877    \snd
     1878     (half_add ?
     1879      (\fst (sigma ppc))
     1880      (bitvector_of_nat ?
     1881       (instruction_size
     1882        (λid. bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) id 0))
     1883        sigma ppc (\fst (fetch_pseudo_instruction (\snd program) ppc)))))
     1884    = \fst (sigma (\snd (half_add ? ppc (bitvector_of_nat ? 1)))))
     1885≝ ?.
     1886(*
    19601887λprogram.λppc:ℕ.
    19611888  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
     
    19631890  [ None ⇒ 〈0, Some ? long_jump〉
    19641891  | Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉
    1965   ].
     1892  ].*)
    19661893 cases daemon
    19671894qed.
  • src/ASM/Util.ma

    r1928 r1934  
    14131413  | #hd #tl #IH #l2 normalize <IH //]
    14141414qed.
     1415
     1416lemma nth_cons:
     1417  ∀n,A,h,t,y.
     1418  nth (S n) A (h::t) y = nth n A t y.
     1419 #n #A #h #t #y /2 by refl/
     1420qed.
     1421
     1422lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
     1423 #A #a #b #EQ destruct //
     1424qed.
Note: See TracChangeset for help on using the changeset viewer.