Changeset 2021


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

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

Location:
src/ASM
Files:
2 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
  • src/ASM/AssemblyProof.ma

    r1984 r2021  
    15741574   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
    15751575*)
     1576
     1577lemma load_code_memory_ok:
     1578 ∀program.
     1579 let program_size ≝ |program| in
     1580  program_size ≤ 2^16 →
     1581   ∀pc. ∀pc_ok: pc < program_size.
     1582    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
     1583 #program elim program
     1584 [ #_ #pc #abs normalize in abs; @⊥ /2/
     1585 | #hd #tl #IH #size_ok *
     1586   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
     1587     whd in match next; normalize nodelta
     1588   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
     1589     whd in match next; normalize nodelta
     1590   ]
     1591 cases daemon (*CSC: complete! *)
     1592qed.
     1593(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
     1594Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
     1595e' come fetchare l'i-esimo bit dalla memoria.
     1596Concludere assembly_ok come semplice corollario.
     1597*)
    15761598lemma assembly_ok:
    15771599  ∀program.
     
    15801602  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    15811603  ∀assembled.
    1582   ∀costs'.
     1604  ∀costs': BitVectorTrie costlabel 16.
    15831605  let 〈preamble, instr_list〉 ≝ program in
    15841606  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
     
    15861608  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
    15871609    〈assembled,costs'〉 = assembly program sigma policy →
    1588       costs = costs' ∧
     1610      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    15891611        let code_memory ≝ load_code_memory assembled in
    15901612        let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 
     
    15971619                  sigma newppc = add … pc (bitvector_of_nat … len).
    15981620  #program #sigma #policy #sigma_policy_witness #assembled #costs'
    1599   @pair_elim #preamble #instr_list #program_refl
    1600   @pair_elim #labels #costs #create_label_cost_refl
    1601   #assembly_refl % cases daemon (*
    1602   [1:
    1603     (* XXX: lemma on BitVectorTries *)
    1604     cases daemon
    1605   |2:
    1606     #ppc #sigma_policy_specification_witness
    1607     @pair_elim #pi #newppc #fetch_pseudo_refl
    1608     cases pi
    1609     [2,3: (* Cost and Comment cases *)
    1610       #comment_or_cost normalize in ⊢ (% → ?); #absurd cases absurd
    1611     |1: (* PreInstruction cases *)
    1612       #preinstruction #_
    1613       @pair_elim #len #assembled' #assembly_1_pseudo_refl
    1614       normalize nodelta %
    1615       [1:
    1616         cases assembled' normalize
    1617       |2:
    1618       ]
    1619     ]
    1620   ]
    1621   cases daemon (* XXX: !!! *) *)
     1621  cases (assembly program sigma policy) * #assembled' #costs''
     1622  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
     1623  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
     1624  #assembly_ok #Pair_eq destruct(Pair_eq) whd
     1625  #ppc @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
     1626  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     1627  lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] -assembly_ok
     1628  >eq_fetch_pseudo_instruction
     1629  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
     1630  >(? : assembly_1_pseudoinstruction ????? pi = 〈len,assembled〉)
     1631   [2: (*CSC: Provable, isn't it?*) cases daemon
     1632   | whd in ⊢ (% → ?); #assembly_ok
     1633  %
     1634  [2: (*CSC: Use Jaap's invariant here *) cases daemon
     1635  | lapply (load_code_memory_ok assembled' ?) [(*CSC: Jaap?*) cases daemon]
     1636    #load_code_memory_ok
     1637    -eq_assembly_1_pseudoinstruction -program -policy -costs'' -labels -preamble -instr_list -costs -pi -newppc
     1638    cut (len=|assembled|) [(*CSC: provable before cleaning*) cases daemon] #EQlen
     1639    (* Nice statement here *)
     1640    cut (∀j. ∀H: j < |assembled|.
     1641          nth_safe Byte j assembled H =
     1642          \snd (next (load_code_memory assembled')
     1643          (bitvector_of_nat 16
     1644           (nat_of_bitvector …
     1645            (add … (sigma ppc) (bitvector_of_nat … j))))))
     1646    [(*CSC: is it provable?*) cases daemon
     1647    | -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
     1648      elim assembled
     1649       [ #pc #_ whd <add_zero %
     1650       | #hd #tl #IH #pc #H %
     1651         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
     1652           >H -H whd in ⊢ (??%?); <add_zero //
     1653         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
     1654           [2: (*CSC: TRUE, ARITHMETIC*) cases daemon]
     1655           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
     1656           <(nth_safe_prepend … [hd] … LTj) #IH >IH
     1657           (*CSC: TRUE, ARITHMETICS*)
     1658           cases daemon
     1659         ]
     1660    ]
    16221661qed.
    16231662
     
    16301669  ∀ppc.
    16311670  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1632   let 〈assembled, costs'〉 ≝ assembly program sigma policy in
     1671  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
    16331672  let code_memory ≝ load_code_memory assembled in
    16341673  let data_labels ≝ construct_datalabels (\fst program) in
     
    16491688  normalize nodelta
    16501689  @pair_elim #labels' #costs' #create_label_map_refl' #H
    1651   cases (H (sym_eq … assembled_refl))
    1652   #_
     1690  lapply (H (sym_eq … assembled_refl)) -H
    16531691  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
    16541692  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
     
    18141852  λsigma.
    18151853  λpolicy.
    1816     let p ≝ assembly pap sigma policy in
     1854    let p ≝ pi1 … (assembly pap sigma policy) in
    18171855      load_code_memory (\fst p).
    18181856
     
    23292367  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
    23302368  #fetch_pseudo_refl
    2331   letin assembled ≝ (\fst (assembly program sigma policy))
    2332   letin costs ≝ (\snd (assembly program sigma policy))
     2369  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
     2370  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
    23332371  lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs)
    23342372  @pair_elim #preamble #instr_list #program_refl
    23352373  @pair_elim #labels #costs' #create_label_cost_map_refl
    2336   <eq_pair_fst_snd #H cases (H (refl …)) -H #costs_refl #H
     2374  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
    23372375  lapply (H ppc) -H
    23382376  @pair_elim #pi' #newppc #fetch_pseudo_refl'
Note: See TracChangeset for help on using the changeset viewer.