Changeset 2021 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 7, 2012, 1:44:18 AM (8 years ago)
Author:
sacerdot
Message:

Proof skeleton in place. Several daemons to be closed adding invariants.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2015 r2021  
    12241224 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
    12251225qed.
    1226  
     1226
     1227(*CSC: move elsewhere; also proved in CostProofs as shift_nth_safe *)
     1228lemma nth_safe_prepend:
     1229 ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.
     1230  nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.
     1231 #A #l1 elim l1 normalize //
     1232qed.
     1233
     1234(*CSC: move elsewhere; also proved in CostProofs as shift_nth_prefix *)
     1235lemma shift_nth_prefix:
     1236 ∀T,l1,i,l2,K1,K2.
     1237  nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
     1238  #T #l1 elim l1 normalize
     1239  [
     1240    #i #l1 #K1 cases(lt_to_not_zero … K1)
     1241  |
     1242    #hd #tl #IH #i #l2
     1243    cases i
     1244    [
     1245      //
     1246    |
     1247      #i' #K1 #K2 whd in ⊢ (??%%);
     1248      @IH
     1249    ]
     1250  ]
     1251qed.
     1252
     1253lemma nth_cons:
     1254 ∀A,hd,tl,l2,j,d.
     1255  nth j A (tl@l2) d =nth (1+j) A (hd::tl@l2) d.
     1256//
     1257qed.
     1258
     1259(*CSC: move elsewhere *)
     1260lemma fetch_pseudo_instruction_append:
     1261 ∀l1,l2,ppc.
     1262  let code_newppc ≝ fetch_pseudo_instruction l2 ppc in
     1263  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) =
     1264  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
     1265 #l1 elim l1
     1266 [ #l2 #ppc >add_commutative <add_zero >add_commutative <add_zero //
     1267 | #hd #tl #IH #l2 #ppc whd whd in match fetch_pseudo_instruction in ⊢ (??%?); normalize nodelta
     1268   (*CSC: FALSE, NEED INVARIANT? *)
     1269   > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (|hd::tl|)) ppc)
     1270       = 1 + nat_of_bitvector … (add … (bitvector_of_nat … (|tl|)) ppc)) [2: cases daemon]
     1271   <nth_cons lapply (IH l2 ppc) -IH normalize nodelta cases (fetch_pseudo_instruction l2 ppc)
     1272   #i #newppc whd in match fetch_pseudo_instruction; normalize nodelta
     1273   cases (nth ? labelled_instruction ??) #i' #newppc' normalize nodelta #EQ
     1274   destruct -EQ change with (add ??? = ?) in e0;
     1275   (*CSC: TRUE, NEEDS TRIVIAL ARITHMETICS *) cases daemon
     1276 ]
     1277qed.
     1278
    12271279definition assembly:
    12281280    ∀p: pseudo_assembly_program.
    12291281    ∀sigma: Word → Word.
    12301282    ∀policy: Word → bool.
    1231       list Byte × (BitVectorTrie costlabel 16) ≝
     1283      Σres:list Byte × (BitVectorTrie costlabel 16).
     1284       let 〈preamble,instr_list〉 ≝ p in
     1285       let 〈assembled,costs〉 ≝ res in
     1286       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
     1287       let datalabels ≝ construct_datalabels preamble in
     1288       let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
     1289       let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
     1290       ∀ppc.
     1291        nat_of_bitvector … ppc < |instr_list| →
     1292         let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in
     1293         let 〈len,assembledi〉 ≝
     1294          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1295         ∀j:nat. ∀H: j < |assembledi|. ∀K.
     1296          nth_safe ? j assembledi H =
     1297           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
     1298            assembled K
     1299
    12321300  λp.
    12331301  λsigma.
    12341302  λpolicy.
    1235   let 〈preamble, instr_list〉 ≝ p in
     1303  deplet 〈preamble, instr_list〉 as p_refl ≝ p in
    12361304  let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    12371305  let datalabels ≝ construct_datalabels preamble in
    12381306  let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
    12391307  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    1240   let result ≝
    1241      pi1 ?? (foldl_strong
     1308  let 〈ignore,revcode〉 ≝ pi1 … (
     1309     foldl_strong
    12421310      (option Identifier × pseudo_instruction)
    1243       (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
    1244         let 〈pc,ppc_code〉 ≝ pc_ppc_code in
     1311      (λpre. Σppc_code:(Word × (list Byte)).
    12451312        let 〈ppc,code〉 ≝ ppc_code in
     1313         ppc = bitvector_of_nat … (|pre|) ∧
    12461314         ∀ppc'.
    1247           let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
    1248           let 〈len,assembledi〉 ≝
    1249            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
    1250            True)
     1315          nat_of_bitvector … ppc' < nat_of_bitvector … ppc →
     1316           let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
     1317           let 〈len,assembledi〉 ≝
     1318            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
     1319           ∀j:nat. ∀H: j < |assembledi|. ∀K.
     1320            nth_safe ? j assembledi H =
     1321             nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K)
    12511322      instr_list
    1252       (λprefix,hd,tl,prf,pc_ppc_code.
    1253         let 〈pc, ppc_code〉 ≝ pc_ppc_code in
    1254         let 〈ppc, code〉 ≝ ppc_code in
     1323      (λprefix,hd,tl,prf,ppc_code.
     1324        let 〈ppc, code〉 ≝ pi1 … ppc_code in
    12551325        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in
    1256         let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    12571326        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
    1258          〈new_pc, 〈new_ppc, (code @ program)〉〉)
    1259       〈(zero ?), 〈(zero ?), [ ]〉〉)
     1327         〈new_ppc, (reverse … program @ code)〉)
     1328      〈(zero ?), [ ]〉)
    12601329    in
    1261      〈\snd (\snd result),
     1330     〈reverse … revcode,
    12621331      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
    1263   @pair_elim normalize nodelta #x #y #z
    1264   @pair_elim normalize nodelta #w1 #w2 #w3 #w4
    1265   @pair_elim //
     1332  [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
     1333    >EQignore_revcode in Hfold; * #_ #Hfold whd >p1 whd #ppc #LTppc @Hfold
     1334    (* CSC: ??? *) cases daemon
     1335  | % // #ppc' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
     1336  | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
     1337    * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
     1338    whd #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2
     1339    cases (le_to_or_lt_eq … LTppc')
     1340    [2: #S_S_eq normalize nodelta in S_S_eq;
     1341        (*CSC: FALSE, NEEDS INVARIANT *)
     1342        cut (ppc' = ppc) [cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' #LTppc
     1343        >prf >IH1 in ⊢ match % with [_ ⇒ ?]; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ match % with [_ ⇒ ?];
     1344        @pair_elim #pi' #newppc' >fetch_pseudo_instruction_append #EQpair destruct(EQpair)
     1345        >p2
     1346        #j #LTj
     1347        (* CSC: FALSE, NEEDS INVARIANT *)
     1348        >(?: nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … j)) =
     1349             nat_of_bitvector … (sigma ppc) + j) [2: cases daemon]
     1350        >reverse_append >reverse_reverse
     1351        (* CSC: TRUE, NEEDS INVARIANT *)
     1352        >(? : nat_of_bitvector … (sigma ppc) = |reverse … code|) [2: cases daemon]
     1353        @nth_safe_prepend
     1354    | #LTppc' lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ]
     1355      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
     1356      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
     1357      change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ∀j:ℕ. ∀H:j<|assembledi|.?)
     1358      >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
     1359      >IH
     1360      [2: (*CSC: FALSE, NEEDS INVARIANT? *) cases daemon
     1361      | @shift_nth_prefix
     1362      ]
     1363    ]
     1364  ] 
    12661365qed.
    12671366
Note: See TracChangeset for help on using the changeset viewer.