Changeset 2055


Ignore:
Timestamp:
Jun 13, 2012, 12:11:21 PM (5 years ago)
Author:
sacerdot
Message:

Warning: this commit adds an hypothesis that breaks all of assembly stuff.

Location:
src/ASM
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2051 r2055  
    672672*)
    673673
    674 (*
    675 (* This establishes the correspondence between pseudo program counters and
    676    program counters. It is at the heart of the proof. *)
    677 (*CSC: code taken from build_maps *)
    678 definition sigma00:
    679  ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? →
    680  (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
    681   let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    682   let 〈program_counter, sigma_map〉 ≝ pc_map in
    683   ppc = |l| ∧
    684   (ppc = |l| →
    685    (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
    686    (∀x.x < |l| →
    687     ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
    688    let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
    689    bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
    690    bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
    691    (\fst (assembly_1_pseudoinstruction lookup_labels(*X?(λx.pc_x)*) (jump_expansion (*?(λx.pc_x)*)) pc_x
    692      (λx.zero ?) pi)))))
    693  ) ≝
    694  (*?*)λlookup_labels.
    695  λjump_expansion(*X?: policy_type2*).
    696  λl:list labelled_instruction.
    697  λacc.
    698   foldl_strong ?
    699    (λprefix.(Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
    700      let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    701      let 〈program_counter, sigma_map〉 ≝ pc_map in
    702      (ppc = |prefix|) ∧
    703      (ppc = |prefix| →
    704       (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
    705       (∀x.x < |prefix| →
    706        ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
    707        let pc_x ≝  bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
    708        bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
    709        bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
    710        (\fst (assembly_1_pseudoinstruction (*X?(λx.pc_x)*)lookup_labels (jump_expansion (*X?(λx.pc_x)*)) pc_x
    711         (λx.zero ?) pi))))))
    712     )
    713    l
    714    (λhd.λi.λtl.λp.λppc_pc_map.
    715      let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    716      let 〈program_counter, sigma_map〉 ≝ pc_map in
    717      let 〈label, i〉 ≝ i in
    718       let 〈pc,ignore〉 ≝ construct_costs lookup_labels program_counter (jump_expansion (*X?(λx.bitvector_of_nat ? program_counter)*)) ppc (Stub …) i in
    719          〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉
    720    ) acc.
    721 cases i in p; #label #ins #p @pair_elim #new_ppc #x normalize nodelta cases x -x #old_pc #old_map
    722 @pair_elim #new_pc #ignore #Hc #Heq normalize nodelta @conj
    723 [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
    724   <(pair_eq1 ?????? Heq) >(proj1 ?? Hind) >append_length <commutative_plus normalize @refl
    725 | #Hnew <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) @conj
    726   [ >lookup_insert_hit >(pair_eq1 ?????? (pair_eq2 ?????? Heq)) @refl
    727   | #x <(pair_eq1 ?????? Heq) >append_length <commutative_plus #Hx normalize in Hx;
    728     #pi #Hpi <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) in Hnew;
    729     >append_length <commutative_plus #Hnew normalize in Hnew; >(injective_S … Hnew)
    730     elim (le_to_or_lt_eq … Hx) -Hx #Hx
    731     [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
    732       lapply (proj2 ?? ((proj2 ?? Hind) (proj1 ?? Hind)) x (le_S_S_to_le … Hx) pi Hpi)
    733       -Hind #Hind >lookup_insert_miss
    734       [2: @bitvector_of_nat_abs
    735         [3: @lt_to_not_eq @Hx
    736         |1: @(transitive_le … Hx)
    737         ]
    738         cases daemon (* XXX invariant *)
    739       ]
    740       >lookup_insert_miss
    741       [2: @bitvector_of_nat_abs
    742         [3: @lt_to_not_eq @(transitive_le … (le_S_S_to_le … Hx)) @le_S @le_n
    743         |1: @(transitive_le … (le_S_S_to_le … Hx))
    744         ]
    745         cases daemon (* XXX invariant *)
    746       ]
    747       @Hind
    748     | lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta
    749       #Hind lapply (proj1 ?? ((proj2 ?? Hind) (proj1 ?? Hind))) -Hind
    750       >(injective_S … Hnew) #Hind <(injective_S … Hx) >lookup_insert_hit >lookup_insert_miss
    751       [2: @bitvector_of_nat_abs
    752         [3: @lt_to_not_eq @le_n
    753         |1: @(transitive_le ??? (le_n (S x)))
    754         ]
    755         cases daemon (* XXX invariant *)
    756       ]
    757       >p in Hpi; whd in match (fetch_pseudo_instruction ??); >nth_append_second
    758       >nat_of_bitvector_bitvector_of_nat >(injective_S … Hx)
    759       [3: @le_n]
    760       [2,3: cases daemon (* XXX invariant *)]
    761       <minus_n_n cases (half_add ???) #x #y normalize nodelta -x -y #Heq <Heq
    762       whd in match (construct_costs ?????) in Hc; whd in match (assembly_1_pseudoinstruction ?????);
    763       cases ins in p Hc; normalize nodelta
    764       [1,2,4,5: #x #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
    765         [1,3,5,7: @refl
    766         |2,4,6,8: cases daemon (* XXX invariant *)
    767         ]
    768       |3: #c #p >Hind #H <(pair_eq1 ?????? H) >nat_of_bitvector_bitvector_of_nat
    769         [2: cases daemon (* XXX invariant *) ]
    770         whd in match (expand_pseudo_instruction ?????); normalize <plus_n_O @refl
    771       |6: #x #y #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
    772         [ @refl
    773         | cases daemon (* XXX invariant *)
    774         ]
    775       ]
    776     ]
    777   ]
    778 ]
    779 qed.
    780 
    781 definition sigma0: pseudo_assembly_program → policy_type2 → (nat × (nat × (BitVectorTrie Word 16))) ≝
    782   λprog.
    783   λjump_expansion.
    784     sigma00 jump_expansion (\snd prog)
    785     〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉.
    786  normalize nodelta @conj
    787  [ / by refl/
    788  | #H @conj
    789    [ >lookup_insert_hit @refl
    790    | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
    791    ]
    792  ]
    793 qed.
    794 
    795 definition tech_pc_sigma00: pseudo_assembly_program → policy_type2 →
    796  list labelled_instruction → (nat × nat) ≝
    797  λprogram,jump_expansion,instr_list.
    798    let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list
    799    〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub ? ?))〉〉 in
    800    (* acc copied from sigma0 *)
    801    let 〈pc,map〉 ≝ pc_sigma_map in
    802      〈ppc,pc〉.
    803  normalize nodelta @conj
    804  [ / by refl/
    805  | #H @conj
    806    [ >lookup_insert_hit @refl
    807    | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
    808    ]
    809  ]
    810 qed.
    811 
    812 definition sigma_safe: pseudo_assembly_program → policy_type2 →
    813  option (Word → Word) ≝
    814  λinstr_list,jump_expansion.
    815   let 〈ppc,pc_sigma_map〉 ≝ sigma0 instr_list jump_expansion in
    816   let 〈pc, sigma_map〉 ≝ pc_sigma_map in
    817     if gtb pc (2^16) then
    818       None ?
    819     else
    820       Some ? (λx. lookup … x sigma_map (zero …)). *)
    821 
    822 (* stuff about policy *)
    823 
    824 (*definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….*)
    825 
    826 (*definition policy ≝ λp. Σjump_expansion:policy_type2. policy_ok jump_expansion p.*)
    827 
    828 (*lemma eject_policy: ∀p. policy p → policy_type2.
    829  #p #pol @(pi1 … pol)
    830 qed.
    831 
    832 coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type2 ≝ eject_policy on _pol:(policy ?) to policy_type2.
    833 
    834 definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
    835  λp,policy.
    836   match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    837    [ None ⇒ λabs. ⊥
    838    | Some r ⇒ λ_.r] (pi2 … policy).
    839  cases abs /2 by /
    840 qed.*)
    841 
    842 (*CSC: Main axiom here, needs to be proved soon! *)
    843 (*lemma snd_assembly_1_pseudoinstruction_ok:
    844  ∀program:pseudo_assembly_program.∀pol: policy program.
    845  ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
    846   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    847   lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    848   (nat_of_bitvector 16 ppc) < |\snd program| →
    849   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    850    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
    851     sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
    852      bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    853  #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl #Hppc
    854  lapply (refl … (sigma0 program pol)) whd in match (sigma0 ??) in ⊢ (??%? → ?);
    855  cases (sigma00 ???) #x #Hpmap #EQ
    856  whd in match (sigma ???);
    857  whd in match (sigma program pol (add ???));
    858  whd in match sigma_safe; normalize nodelta
    859  (*Problem1: backtracking cases (sigma0 program pol)*)
    860  generalize in match (pi2 ???); whd in match policy_ok; normalize nodelta
    861  whd in match sigma_safe; normalize nodelta <EQ cases x in Hpmap EQ; -x #final_ppc #x
    862  cases x -x #final_pc #smap normalize nodelta #Hpmap #EQ #Heq #Hfetch cases (gtb final_pc (2^16)) in Heq;
    863  normalize nodelta
    864  [ #abs @⊥ @(absurd ?? abs) @refl
    865  | #_ lapply (proj1 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) #Hpmap1
    866    lapply ((proj2 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) (nat_of_bitvector 16 ppc) Hppc) #Hpmap2 -Hpmap
    867    <(bitvector_of_nat_nat_of_bitvector 16 ppc) >add_SO
    868    
    869    >(Hpmap2 ? (refl …)) @eq_f @eq_f2 [%]
    870    >bitvector_of_nat_nat_of_bitvector
    871    >Hfetch lapply Hfetch lapply pi
    872 
    873    
    874    whd in match assembly_1_pseudoinstruction; normalize nodelta
    875  
    876 qed.*)
    877 
    878 
    879 (*example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
    880  cases daemon.
    881 qed.*)
    882 
    883 (*CSC: FALSE!!!*)
    884 axiom fetch_pseudo_instruction_vsplit:
    885  ∀instr_list,ppc.
     674(*CSC: move elsewhere *)
     675lemma nth_safe_append:
     676 ∀A,l,n,n_ok.
     677  ∃pre,suff.
     678   (pre @ [nth_safe A n l n_ok]) @ suff = l.
     679#A #l elim l normalize
     680 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))
     681 | #hd #tl #IH #n cases n normalize
     682   [ #_ %{[]} /2/
     683   | #m #m_ok cases (IH m ?)
     684     [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]]
     685qed.
     686
     687lemma fetch_pseudo_instruction_vsplit:
     688 ∀instr_list,ppc,ppc_ok.
    886689  ∃pre,suff,lbl.
    887    (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
     690   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
     691#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
     692cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
     693lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
     694#EQ %{lbl0} @EQ
     695qed.
    888696
    889697(*lemma sigma00_append:
     
    12401048qed.
    12411049
    1242 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_safe *)
     1050
     1051(*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation
     1052  of addition. One of the two lemmas should disappear. *)
    12431053lemma nth_safe_prepend:
    12441054 ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.
    12451055  nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.
    1246  #A #l1 elim l1 normalize //
    1247 qed.
    1248 
    1249 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_prefix *)
    1250 lemma shift_nth_prefix:
    1251  ∀T,l1,i,l2,K1,K2.
    1252   nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
    1253   #T #l1 elim l1 normalize
    1254   [
    1255     #i #l1 #K1 cases(lt_to_not_zero … K1)
    1256   |
    1257     #hd #tl #IH #i #l2
    1258     cases i
    1259     [
    1260       //
    1261     |
    1262       #i' #K1 #K2 whd in ⊢ (??%%);
    1263       @IH
    1264     ]
    1265   ]
    1266 qed.
    1267 
    1268 lemma nth_cons:
    1269  ∀A,hd,tl,l2,j,d.
    1270   nth j A (tl@l2) d =nth (1+j) A (hd::tl@l2) d.
     1056 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe
     1057qed.
     1058
     1059lemma nth_safe_cons:
     1060 ∀A,hd,tl,l2,j,j_ok,Sj_ok.
     1061  nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.
    12711062//
     1063qed.
     1064
     1065lemma eq_nth_safe_proof_irrelevant:
     1066 ∀A,l,i,i_ok,i_ok'.
     1067  nth_safe A l i i_ok = nth_safe A l i i_ok'.
     1068#A #l #i #i_ok #i_ok' %
    12721069qed.
    12731070
    12741071(*CSC: move elsewhere *)
    12751072lemma fetch_pseudo_instruction_append:
    1276  ∀l1,l2,ppc.
    1277   let code_newppc ≝ fetch_pseudo_instruction l2 ppc in
    1278   fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) =
     1073 ∀l1,l2,ppc,ppc_ok,ppc_ok'.
     1074  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
     1075  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
    12791076  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
    1280  #l1 elim l1
    1281  [ #l2 #ppc >add_commutative <add_zero >add_commutative <add_zero //
    1282  | #hd #tl #IH #l2 #ppc whd whd in match fetch_pseudo_instruction in ⊢ (??%?); normalize nodelta
    1283    (*CSC: FALSE, NEED INVARIANT? *)
    1284    > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (|hd::tl|)) ppc)
    1285        = 1 + nat_of_bitvector … (add … (bitvector_of_nat … (|tl|)) ppc)) [2: cases daemon]
    1286    <nth_cons lapply (IH l2 ppc) -IH normalize nodelta cases (fetch_pseudo_instruction l2 ppc)
    1287    #i #newppc whd in match fetch_pseudo_instruction; normalize nodelta
    1288    cases (nth ? labelled_instruction ??) #i' #newppc' normalize nodelta #EQ
    1289    destruct -EQ change with (add ??? = ?) in e0;
    1290    (*CSC: TRUE, NEEDS TRIVIAL ARITHMETICS *) cases daemon
    1291  ]
     1077 #l1 #l2 #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
     1078 (*CSC: FALSE, NEED INVARIANT? *)
     1079 > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (|l1|)) ppc)
     1080     = |l1| + nat_of_bitvector … ppc) [2: cases daemon]
     1081 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
     1082 #lbl #instr normalize nodelta >add_associative %
    12921083qed.
    12931084
     
    13031094       let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
    13041095       let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    1305        ∀ppc.
    1306         nat_of_bitvector … ppc < |instr_list| →
    1307          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in
     1096       ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
     1097         let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in
    13081098         let 〈len,assembledi〉 ≝
    13091099          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     
    13271117        let 〈ppc,code〉 ≝ ppc_code in
    13281118         ppc = bitvector_of_nat … (|pre|) ∧
    1329          ∀ppc'.
     1119         ∀ppc'.∀ppc_ok'.
    13301120          nat_of_bitvector … ppc' < nat_of_bitvector … ppc →
    1331            let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
     1121           let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in
    13321122           let 〈len,assembledi〉 ≝
    13331123            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
     
    13461136      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
    13471137  [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
    1348     >EQignore_revcode in Hfold; * #_ #Hfold whd >p1 whd #ppc #LTppc @Hfold
    1349     (* CSC: ??? *) cases daemon
    1350   | % // #ppc' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
     1138    >EQignore_revcode in Hfold; * #Hfold1 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
     1139    >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     1140    (* CSC: FALSE, NEEDS ADDITIONAL ASSUMPTION *) cases daemon
     1141  | % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
    13511142  | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
    13521143    * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
    1353     whd #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2
     1144    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2
    13541145    cases (le_to_or_lt_eq … LTppc')
    13551146    [2: #S_S_eq normalize nodelta in S_S_eq;
    13561147        (*CSC: FALSE, NEEDS INVARIANT *)
    1357         cut (ppc' = ppc) [cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' #LTppc
    1358         >prf >IH1 in ⊢ match % with [_ ⇒ ?]; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ match % with [_ ⇒ ?];
    1359         @pair_elim #pi' #newppc' >fetch_pseudo_instruction_append #EQpair destruct(EQpair)
    1360         >p2
     1148        cut (ppc' = ppc) [cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
     1149        >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc #X lapply LTppc
     1150        >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
     1151        >fetch_pseudo_instruction_append
     1152        [3: @le_S_S @le_O_n |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H]
     1153        #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
    13611154        #j #LTj
    13621155        (* CSC: FALSE, NEEDS INVARIANT *)
     
    13671160        >(? : nat_of_bitvector … (sigma ppc) = |reverse … code|) [2: cases daemon]
    13681161        @nth_safe_prepend
    1369     | #LTppc' lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ]
     1162    | #LTppc' #LT_ppc_ppc lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ]
    13701163      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
    13711164      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
     
    13741167      >IH
    13751168      [2: (*CSC: FALSE, NEEDS INVARIANT? *) cases daemon
    1376       | @shift_nth_prefix
     1169      | @shift_nth_prefix
     1170      |3: >IH1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     1171          (*CSC: ALSO FALSE, NEEDS INVARIANT? *) cases daemon
    13771172      ]
    13781173    ]
  • src/ASM/CostsProof.ma

    r2001 r2055  
    457457 (λ_.0).
    458458 @tech_cost_of_label0 @codom_dom
    459 qed.
    460 
    461 lemma shift_nth_safe:
    462  ∀T,i,l2,l1,K1,K2.
    463   nth_safe T i l1 K1 = nth_safe T (i+|l2|) (l2@l1) K2.
    464  #T #i #l2 elim l2 normalize
    465   [ #l1 #K1 <plus_n_O #K2 %
    466   | #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;
    467     whd in ⊢ (???%); @IH ]
    468 qed.
    469 
    470 lemma shift_nth_prefix:
    471  ∀T,l1,i,l2,K1,K2.
    472   nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
    473   #T #l1 elim l1 normalize
    474   [
    475     #i #l1 #K1 cases(lt_to_not_zero … K1)
    476   |
    477     #hd #tl #IH #i #l2
    478     cases i
    479     [
    480       //
    481     |
    482       #i' #K1 #K2 whd in ⊢ (??%%);
    483       @IH
    484     ]
    485   ]
    486459qed.
    487460
  • src/ASM/Policy.ma

    r2034 r2055  
    625625∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
    626626 option (Σsigma:Word → Word × bool.
    627    ∀ppc: Word.
     627   ∀ppc: Word. ∀ppc_ok.
    628628   let pc ≝ \fst (sigma ppc) in
    629629   let labels ≝ \fst (create_label_cost_map (\snd program)) in
    630630   let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in
    631    let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
     631   let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
    632632   let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    633633     And (nat_of_bitvector … ppc ≤ |\snd program| →
  • src/ASM/Status.ma

    r2032 r2055  
    11141114   set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
    11151115
    1116 definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
     1116definition fetch_pseudo_instruction:
     1117 ∀code_mem:list labelled_instruction. ∀pc:Word.
     1118  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
    11171119  λcode_mem.
    11181120  λpc: Word.
    1119     let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    1120     let new_pc ≝ add ? pc (bitvector_of_nat ? 1) in
     1121  λpc_ok.
     1122    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
     1123    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
    11211124      〈instr, new_pc〉.
    1122     cases not_implemented.
    1123 qed.
    11241125
    11251126lemma snd_fetch_pseudo_instruction:
    1126  ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = add ? ppc (bitvector_of_nat ? 1).
    1127  #l #ppc whd in ⊢ (??(???%)?); @pair_elim
     1127 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
     1128 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
    11281129 #lft #rgt #_ %
    11291130qed.
  • src/ASM/Util.ma

    r2037 r2055  
    225225  ]
    226226qed.
     227
     228lemma shift_nth_safe:
     229 ∀T,i,l2,l1,K1,K2.
     230  nth_safe T i l1 K1 = nth_safe T (i+|l2|) (l2@l1) K2.
     231 #T #i #l2 elim l2 normalize
     232  [ #l1 #K1 <plus_n_O #K2 %
     233  | #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;
     234    whd in ⊢ (???%); @IH ]
     235qed.
     236
     237lemma shift_nth_prefix:
     238 ∀T,l1,i,l2,K1,K2.
     239  nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
     240  #T #l1 elim l1 normalize
     241  [
     242    #i #l1 #K1 cases(lt_to_not_zero … K1)
     243  |
     244    #hd #tl #IH #i #l2
     245    cases i
     246    [
     247      //
     248    |
     249      #i' #K1 #K2 whd in ⊢ (??%%);
     250      @IH
     251    ]
     252  ]
     253qed.
     254
    227255
    228256definition last_safe ≝
Note: See TracChangeset for help on using the changeset viewer.