Changeset 1948 for src/ASM/Assembly.ma


Ignore:
Timestamp:
May 15, 2012, 11:13:14 AM (8 years ago)
Author:
mulligan
Message:

Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so all lemmas and functions that accepted a sigma before now accept a weakened sigma coupled with a policy. ASM/AssemblyProof.ma compiles until main_thm.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1946 r1948  
    55include alias "basics/logic.ma".
    66include alias "arithmetics/nat.ma".
    7 include "utilities/extralib.ma". 
     7include "utilities/extralib.ma".
    88
    99(**************************************** START OF POLICY ABSTRACTION ********************)
     
    419419
    420420definition expand_relative_jump_internal:
    421  ∀lookup_labels:Identifier → Word.∀sigma:Word → Word × bool.
     421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
    422422 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
    423423 list instruction
    424424 ≝
    425425  λlookup_labels.λsigma.λlbl.λppc,i.
    426    let lookup_address ≝ \fst (sigma (lookup_labels lbl)) in
    427    let pc ≝ \fst (sigma ppc) in
     426   let lookup_address ≝ sigma (lookup_labels lbl) in
     427   let pc ≝ sigma ppc in
    428428   let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
    429429   let 〈upper, lower〉 ≝ split ? 8 8 result in
     
    436436      LJMP (ADDR16 lookup_address)
    437437    ].
    438   @ I
     438  %
    439439qed.
    440440
     
    471471  preinstruction Identifier → list instruction ≝
    472472  λlookup_labels: Identifier → Word.
    473   λsigma:Word → Word × bool.
     473  λsigma:Word → Word.
    474474  λppc: Word.
    475475  (*λjmp_len: jump_length.*)
     
    517517
    518518definition expand_pseudo_instruction:
    519  ∀lookup_labels.∀sigma.Word → ? → pseudo_instruction → list instruction ≝
    520   λlookup_labels:Identifier → Word.
    521   λsigma:Word → Word × bool.
     519    ∀lookup_labels.
     520    ∀sigma: Word → Word.
     521    ∀policy: Word → bool.
     522      Word → ? → pseudo_instruction → list instruction ≝
     523  λlookup_labels: Identifier → Word.
     524  λsigma: Word → Word.
     525  λpolicy: Word → bool.
    522526  λppc.
    523527  λlookup_datalabels:Identifier → Word.
     
    527531  | Comment comment ⇒ [ ]
    528532  | Call call ⇒
    529     let 〈addr_5, resta〉 ≝ split ? 5 11 (\fst (sigma (lookup_labels call))) in
    530     let 〈pc, do_a_long〉 ≝ sigma ppc in
     533    let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in
     534    let pc ≝ sigma ppc in
     535    let do_a_long ≝ policy ppc in
    531536    let 〈pc_5, restp〉 ≝ split ? 5 11 pc in
    532537    if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
     
    534539        [ ACALL address ]
    535540    else
    536       let address ≝ ADDR16 (\fst (sigma (lookup_labels call))) in
     541      let address ≝ ADDR16 (sigma (lookup_labels call)) in
    537542        [ LCALL address ]
    538543  | Mov d trgt ⇒
     
    541546  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
    542547  | Jmp jmp ⇒
    543     let 〈pc, do_a_long〉 ≝ sigma ppc in
    544     let lookup_address ≝ \fst (sigma (lookup_labels jmp)) in
     548    let pc ≝ sigma ppc in
     549    let do_a_long ≝ policy ppc in
     550    let lookup_address ≝ sigma (lookup_labels jmp) in
    545551    let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
    546552    let 〈upper, lower〉 ≝ split ? 8 8 result in
     
    558564        [ LJMP address ]
    559565  ].
    560   @ I
     566  %
    561567qed.
    562568
     
    607613definition assembly_1_pseudoinstruction ≝
    608614  λlookup_labels.
    609   λsigma.
     615  λsigma: Word → Word.
     616  λpolicy: Word → bool.
    610617  λppc: Word.
    611618  λlookup_datalabels.
    612619  λi.
    613   let pseudos ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels i in
     620  let pseudos ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels i in
    614621  let mapped ≝ map ? ? assembly1 pseudos in
    615622  let flattened ≝ flatten ? mapped in
     
    618625
    619626definition instruction_size ≝
    620  λlookup_labels.λsigma.λppc.λi.
    621   \fst (assembly_1_pseudoinstruction lookup_labels sigma ppc (λx.zero …) i).
     627  λlookup_labels.
     628  λsigma: Word → Word.
     629  λpolicy: Word → bool.
     630  λppc.
     631  λi.
     632    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
    622633
    623634(* Jaap: never used
     
    11361147
    11371148(* The function that creates the label-to-address map *)
    1138 definition create_label_cost_map: ∀program:list labelled_instruction.
     1149definition create_label_cost_map0: ∀program:list labelled_instruction.
    11391150  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
    11401151    let 〈labels,costs〉 ≝ labels_costs in
    1141     (*∀i:ℕ.lt i (|program|) → *)
    11421152    ∀l.occurs_exactly_once ?? l program →
    1143     (*is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    1144     lookup ?? labels l = Some ? i*)
    11451153    bitvector_of_nat ? (lookup_def ?? labels l 0) =
    11461154     address_of_word_labels_code_mem program l
     
    11531161    ∀l.occurs_exactly_once ?? l prefix →
    11541162    bitvector_of_nat ? (lookup_def ?? labels l 0) =
    1155      address_of_word_labels_code_mem prefix l
    1156     (*
    1157     ∀i:ℕ.lt i (|prefix|) →
    1158     ∀l.occurs_exactly_once ?? l prefix →
    1159     is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    1160     lookup … labels l = Some ? i *)
    1161   )
     1163     address_of_word_labels_code_mem prefix l)
    11621164  program
    11631165  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
     
    11971199   ]
    11981200 ]
    1199 (*  |       
    1200     [ @Hocc
    1201     | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    1202     ]
    1203  [1,2: normalize nodelta
    1204    (* #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    1205   [3: #Hi *) #lbl #Hocc (*#Hlbl*) lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc
    1206     @eq_identifier_elim
    1207     [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl
    1208       @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/
    1209     | #Heq #Hocc normalize in Hocc; >lookup_add_miss
    1210       [ @(IH2 … i (le_S_S_to_le … Hi))
    1211         [ @Hocc
    1212         | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    1213         ]
    1214       | @sym_neq @Heq
    1215       ]
    1216     ]
    1217   |4: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
    1218     [ <minus_n_n #Hl normalize in Hl; >Hl >IH1 @lookup_add_hit
    1219     | @le_n
    1220     ]
    1221   |1: #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl
    1222     @(IH2 … i (le_S_S_to_le … Hi))
    1223     [ @Hocc
    1224     | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    1225     ]
    1226   |2: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
    1227     [ <minus_n_n #Hl cases Hl
    1228     | @le_n
    1229     ]
    1230   ]
    1231  ] *)
    12321201| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
    12331202  #l #abs cases (abs)
     
    12371206qed.
    12381207
     1208(* The function that creates the label-to-address map *)
     1209definition create_label_cost_map: ∀program:list labelled_instruction.
     1210  label_map × (BitVectorTrie costlabel 16) ≝
     1211    λprogram.
     1212      pi1 … (create_label_cost_map0 program).
     1213
    12391214theorem create_label_cost_map_ok:
    12401215 ∀pseudo_program: pseudo_assembly_program.
     
    12421217    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
    12431218     bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
    1244  #p @pi2
     1219 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
    12451220qed.
    12461221 
    12471222definition assembly:
    1248  ∀p:pseudo_assembly_program.∀sigma:Word → Word × bool.list Byte × (BitVectorTrie costlabel 16) ≝
    1249   λp.let 〈preamble, instr_list〉 ≝ p in
    1250    λsigma.
    1251     let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    1252     let datalabels ≝ construct_datalabels preamble in
    1253     let lookup_labels ≝ λx. \fst (sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0))) in
    1254     let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    1255     let result ≝
     1223    ∀p: pseudo_assembly_program.
     1224    ∀sigma: Word → Word.
     1225    ∀policy: Word → bool.
     1226      list Byte × (BitVectorTrie costlabel 16) ≝
     1227  λp.
     1228  let 〈preamble, instr_list〉 ≝ p in
     1229  λsigma.
     1230  λpolicy.
     1231  let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
     1232  let datalabels ≝ construct_datalabels preamble in
     1233  let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
     1234  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
     1235  let result ≝
    12561236     foldl_strong
    12571237      (option Identifier × pseudo_instruction)
     
    12621242          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
    12631243          let 〈len,assembledi〉 ≝
    1264            assembly_1_pseudoinstruction lookup_labels sigma ppc' lookup_datalabels pi in
     1244           assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
    12651245           True)
    12661246      instr_list
     
    12681248        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
    12691249        let 〈ppc, code〉 ≝ ppc_code in
    1270         let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels (\snd hd) in
     1250        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in
    12711251        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    12721252        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
     
    12751255    in
    12761256     〈\snd (\snd result),
    1277       fold … (λppc.λcost.λpc_to_costs. insert … (\fst (sigma ppc)) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
    1278  @pair_elim normalize nodelta #x #y #z @pair_elim normalize nodelta #w1 #w2 #w3 #w4 @pair_elim //
    1279 qed.
    1280 
    1281 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    1282  λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
     1257      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
     1258  @pair_elim normalize nodelta #x #y #z
     1259  @pair_elim normalize nodelta #w1 #w2 #w3 #w4
     1260  @pair_elim //
     1261qed.
     1262
     1263definition assembly_unlabelled_program:
     1264    assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
     1265  λp.
     1266    Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracChangeset for help on using the changeset viewer.