Changeset 1948


Ignore:
Timestamp:
May 15, 2012, 11:13:14 AM (7 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.

Location:
src/ASM
Files:
3 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 …〉).
  • src/ASM/AssemblyProof.ma

    r1947 r1948  
    4343    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
    4444  #b #c
    45   cases b
    46   [1:
    47     normalize //
    48   |2:
    49     normalize
    50     cases c normalize //
    51   ]
     45  cases b cases c normalize nodelta
     46  try (#_ % @I)
     47  #assm destruct %
    5248qed.
    5349
     
    14161412lemma fetch_assembly_pseudo':
    14171413  ∀lookup_labels.
    1418   ∀sigma: Word → Word × bool.
     1414  ∀sigma: Word → Word.
     1415  ∀policy: Word → bool.
    14191416  ∀ppc.
    14201417  ∀lookup_datalabels.
     
    14241421  ∀assembled.
    14251422  ∀instructions.
    1426     let 〈pc, force_long_jump〉 ≝ sigma ppc in
    1427       instructions = expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi →
    1428         〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi →
     1423    let pc ≝ sigma ppc in
     1424      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
     1425        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
    14291426          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    14301427            encoding_check code_memory pc pc_plus_len assembled →
    14311428              fetch_many code_memory pc_plus_len pc instructions.
    1432   #lookup_labels #sigma #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
    1433   generalize in match (refl … (sigma ppc));
    1434   cases (sigma ?) in ⊢ (??%? → %); #pc #force_long_jump #sigma_refl normalize nodelta
    1435   #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
     1429  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
     1430  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
    14361431  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
    14371432  >len_refl >assembled_refl -len_refl
    1438   generalize in match (add 16 pc
     1433  generalize in match (add 16 (sigma ppc)
    14391434    (bitvector_of_nat 16
    14401435     (|flatten (Vector bool 8)
    14411436       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
    14421437  #final_pc
    1443   generalize in match pc; elim instructions
     1438  generalize in match (sigma ppc); elim instructions
    14441439  [1:
    14451440    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
     
    14641459lemma fetch_assembly_pseudo:
    14651460  ∀program: pseudo_assembly_program.
    1466   ∀sigma: Word → Word × bool.
    1467   let lookup_labels ≝ λx:Identifier.\fst (sigma (address_of_word_labels_code_mem (\snd  program) x)) in
    1468   ∀ppc.∀code_memory.
     1461  ∀sigma: Word → Word.
     1462  ∀policy: Word → bool.
     1463  let lookup_labels ≝ λx:Identifier. sigma (address_of_word_labels_code_mem (\snd  program) x) in
     1464  ∀ppc.
     1465  ∀code_memory.
    14691466  let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    14701467  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
    1471   let pc ≝ \fst (sigma ppc) in
    1472   let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
    1473   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
     1468  let pc ≝ sigma ppc in
     1469  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1470  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    14741471  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    14751472    encoding_check code_memory pc pc_plus_len assembled →
    14761473      fetch_many code_memory pc_plus_len pc instructions.
    1477  #program #sigma letin lookup_labels ≝ (λx.?) #ppc #code_memory
     1474 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory
    14781475 letin lookup_datalabels ≝ (λx.?)
    14791476 letin pi ≝ (fst ???)
    1480  letin pc ≝ (fst ???)
    1481  letin instructions ≝ (expand_pseudo_instruction ?????)
     1477 letin pc ≝ (sigma ?)
     1478 letin instructions ≝ (expand_pseudo_instruction ??????)
    14821479 @pair_elim #len #assembled #assembled_refl normalize nodelta
    14831480 #H
    14841481 generalize in match
    1485   (fetch_assembly_pseudo' lookup_labels sigma ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
    1486  #X destruct
    1487  cases (sigma ppc) in H X; #pc #force_long_jump normalize nodelta
    1488  #H #X @X try % <assembled_refl try % assumption
     1482  (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
     1483 #X destruct normalize nodelta @X try % <assembled_refl try % assumption
    14891484qed.
    14901485
     
    14981493*)
    14991494axiom assembly_ok:
    1500  ∀program,sigma,assembled,costs'.
     1495  ∀program.
     1496  ∀sigma: Word → Word.
     1497  ∀policy: Word → bool.
     1498  ∀assembled.
     1499  ∀costs'.
    15011500  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1502   〈assembled,costs'〉 = assembly program sigma
     1501  〈assembled,costs'〉 = assembly program sigma policy
    15031502  costs = costs' ∧
    15041503  let code_memory ≝ load_code_memory assembled in
    15051504  let datalabels ≝ construct_datalabels (\fst program) in
    1506   let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 
     1505  let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
    15071506  let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
    15081507  ∀ppc.
    15091508  let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1510   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
    1511   let pc ≝ \fst (sigma ppc) in
     1509  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1510  let pc ≝ sigma ppc in
    15121511  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    15131512   encoding_check code_memory pc pc_plus_len assembled ∧
    1514        \fst (sigma newppc) = add … pc (bitvector_of_nat … len).
     1513       sigma newppc = add … pc (bitvector_of_nat … len).
    15151514
    15161515(* XXX: should we add that costs = costs'? *)
    15171516lemma fetch_assembly_pseudo2:
    1518  ∀program,sigma,ppc.
     1517  ∀program.
     1518  ∀sigma.
     1519  ∀policy.
     1520  ∀ppc.
    15191521  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1520   let 〈assembled, costs'〉 ≝ assembly program sigma in
     1522  let 〈assembled, costs'〉 ≝ assembly program sigma policy in
    15211523  let code_memory ≝ load_code_memory assembled in
    15221524  let data_labels ≝ construct_datalabels (\fst program) in
    1523   let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 
     1525  let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
    15241526  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    15251527  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1526   let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
    1527     fetch_many code_memory (\fst (sigma newppc)) (\fst (sigma ppc)) instructions.
    1528   * #preamble #instr_list #sigma #ppc
     1528  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     1529    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
     1530  * #preamble #instr_list #sigma #policy #ppc
    15291531  @pair_elim #labels #costs #create_label_map_refl
    15301532  @pair_elim #assembled #costs' #assembled_refl
     
    15341536  letin lookup_datalabels ≝ (λx. ?)
    15351537  @pair_elim #pi #newppc #fetch_pseudo_refl
    1536   lapply (assembly_ok 〈preamble, instr_list〉 sigma assembled costs')
     1538  lapply (assembly_ok 〈preamble, instr_list〉 sigma policy assembled costs')
    15371539  @pair_elim #labels' #costs' #create_label_map_refl' #H
    15381540  cases (H (sym_eq … assembled_refl))
    15391541  #_
    1540   lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi))
    1541   cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?);
     1542  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
     1543  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
    15421544  #len #assembledi #EQ4 #H
    15431545  lapply (H ppc) >fetch_pseudo_refl #H
    1544   lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma ppc (load_code_memory assembled))
     1546  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled))
    15451547  >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
    15461548  >fetch_pseudo_refl in H1; #assm @assm assumption
     
    16951697
    16961698definition code_memory_of_pseudo_assembly_program:
    1697  ∀pap:pseudo_assembly_program. (Word → Word × bool) → BitVectorTrie Byte 16
    1698 ≝ λpap,sigma.
    1699    let p ≝ assembly pap sigma in
    1700     load_code_memory (\fst p).
     1699    ∀pap:pseudo_assembly_program.
     1700      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
     1701  λpap.
     1702  λsigma.
     1703  λpolicy.
     1704    let p ≝ assembly pap sigma policy in
     1705      load_code_memory (\fst p).
    17011706
    17021707definition status_of_pseudo_status:
    1703  internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀sigma: Word → Word × bool.
    1704   Status (code_memory_of_pseudo_assembly_program pap sigma) ≝
    1705  λM,pap,ps,sigma.
    1706   let cm ≝ code_memory_of_pseudo_assembly_program … sigma in
    1707   let pc ≝ \fst (sigma (program_counter … ps)) in
     1708    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
     1709      ∀sigma: Word → Word. ∀policy: Word → bool.
     1710        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
     1711  λM.
     1712  λpap.
     1713  λps.
     1714  λsigma.
     1715  λpolicy.
     1716  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
     1717  let pc ≝ sigma (program_counter … ps) in
    17081718  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    17091719  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     
    18331843*)
    18341844
    1835 definition ticks_of0: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → pseudo_instruction → nat × nat ≝
    1836   λprogram: pseudo_assembly_program.λsigma.
     1845definition ticks_of0:
     1846    ∀p:pseudo_assembly_program.
     1847      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
     1848  λprogram: pseudo_assembly_program.
     1849  λsigma.
     1850  λpolicy.
    18371851  λppc: Word.
    18381852  λfetched. ?.
     
    19892003*)qed.
    19902004
    1991 definition ticks_of: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → nat × nat ≝
    1992   λprogram: pseudo_assembly_program.λsigma.
     2005definition ticks_of:
     2006    ∀p:pseudo_assembly_program.
     2007      (Word → Word) → (Word → bool) → Word → nat × nat ≝
     2008  λprogram: pseudo_assembly_program.
     2009  λsigma.
     2010  λpolicy.
    19932011  λppc: Word.
    19942012    let 〈preamble, pseudo〉 ≝ program in
    19952013    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
    1996      ticks_of0 program sigma ppc fetched.
     2014     ticks_of0 program sigma policy ppc fetched.
    19972015
    19982016lemma eq_rect_Type1_r:
    19992017  ∀A: Type[1].
    2000   ∀a:A.
     2018  ∀a: A.
    20012019  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    20022020  #A #a #P #H #x #p
    20032021  generalize in match H;
    20042022  generalize in match P;
    2005   cases p
    2006   //
     2023  cases p //
    20072024qed.
    20082025
     
    21622179(*CSC: ???*)
    21632180axiom snd_assembly_1_pseudoinstruction_ok:
    2164  ∀program:pseudo_assembly_program.∀sigma.
    2165  ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
    2166   lookup_labels = (λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x))) →
    2167   lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    2168   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    2169    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma (\fst (sigma ppc)) lookup_datalabels  pi) in
    2170     \fst (sigma (add … ppc (bitvector_of_nat ? 1))) =
    2171      add … (\fst (sigma ppc)) (bitvector_of_nat ? len).
     2181  ∀program: pseudo_assembly_program.
     2182  ∀sigma: Word → Word.
     2183  ∀policy: Word → bool.
     2184  ∀ppc: Word.
     2185  ∀pi.
     2186  ∀lookup_labels.
     2187  ∀lookup_datalabels.
     2188    lookup_labels = (λx. sigma (address_of_word_labels_code_mem (\snd program) x)) →
     2189    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     2190    \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     2191    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels  pi) in
     2192      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
    21722193
    21732194lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
    2174  /2/
     2195  /2/
    21752196qed.
    21762197
    21772198(* To be moved in ProofStatus *)
    21782199lemma program_counter_set_program_counter:
    2179  ∀T,cm,s,x. program_counter T cm (set_program_counter T cm s x) = x.
    2180  //
     2200  ∀T.
     2201  ∀cm.
     2202  ∀s.
     2203  ∀x.
     2204    program_counter T cm (set_program_counter T cm s x) = x.
     2205  //
    21812206qed.
    21822207
    21832208theorem main_thm:
    2184  ∀M,M',cm,ps,sigma.
    2185   next_internal_pseudo_address_map M cm ps = Some … M' →
    2186    ∃n.
    2187       execute n … (status_of_pseudo_status M … ps sigma)
    2188     = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm sigma) cm ps) sigma.
    2189  #M #M' * #preamble #instr_list #ps #sigma
    2190  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    2191  @(pose … (program_counter ?? ps)) #ppc #EQppc
    2192  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma ppc) in ⊢ ?;
    2193  @pair_elim #labels #costs #H0 normalize nodelta
    2194  @pair_elim #assembled #costs' #EQ1 normalize nodelta
    2195  @pair_elim #pi #newppc #EQ2 normalize nodelta
    2196  @(pose … (λx. \fst (sigma (address_of_word_labels_code_mem instr_list x)))) #lookup_labels #EQlookup_labels
    2197  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    2198  whd in match execute_1_pseudo_instruction; normalize nodelta
    2199  whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
    2200  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
    2201  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    2202  [>EQ2 %]
    2203  inversion pi
    2204   [2,3: (* Comment, Cost *) #ARG #EQ
    2205    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ?????) in H3;
    2206    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    2207    whd in match (execute_1_pseudo_instruction0 ?????);
    2208    %{0} @split_eq_status
     2209  ∀M.
     2210  ∀M'.
     2211  ∀cm.
     2212  ∀ps.
     2213  ∀sigma.
     2214  ∀policy.
     2215    next_internal_pseudo_address_map M cm ps = Some … M' →
     2216      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
     2217        status_of_pseudo_status M' …
     2218          (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.
     2219  #M #M' * #preamble #instr_list #ps #sigma #policy
     2220  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
     2221  @(pose … (program_counter ?? ps)) #ppc #EQppc
     2222  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;
     2223  @pair_elim #labels #costs #H0 normalize nodelta
     2224  @pair_elim #assembled #costs' #EQ1 normalize nodelta
     2225  @pair_elim #pi #newppc #EQ2 normalize nodelta
     2226  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
     2227  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
     2228  whd in match execute_1_pseudo_instruction; normalize nodelta
     2229  whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
     2230  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
     2231  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
     2232  [>EQ2 %]
     2233  inversion pi
     2234  [2,3: (* Comment, Cost *)
     2235    #ARG #EQ
     2236    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
     2237    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
     2238    whd in match (execute_1_pseudo_instruction0 ?????);
     2239    %{0} @split_eq_status
    22092240   CSC: STOP HERE, was // but requires -H0 -H3 because of \fst and \pi1
    22102241   ⇒ CHANGE TO AVOID \fst and \pi1! (*
  • src/ASM/Interpret.ma

    r1946 r1948  
    88    let b ≝ get_index_v ? 8 c 1 ? in
    99      [[ b; b; b; b; b; b; b; b ]] @@ c.
    10   normalize;
    11   repeat (@ (le_S_S ?));
    12   @ (le_O_n);
     10  normalize
     11  repeat (@le_S_S)
     12  @le_O_n
    1313qed.
    1414   
    15 lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
    16  # a
    17  # b
    18  cases a
    19  cases b
     15lemma eq_a_to_eq:
     16  ∀a,b.
     17    eq_a a b = true → a = b.
     18 #a #b
     19 cases a cases b
    2020 normalize
    21  # K
     21 #K
    2222 try %
    2323 cases (eq_true_false K)
     
    2525
    2626lemma is_a_to_mem_to_is_in:
    27  ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
    28  # he
    29  # a
    30  # m
    31  # q
     27 ∀he,a,m,q.
     28   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
     29 #he #a #m #q
    3230 elim q
    33  [ normalize
    34    # _
    35    # K
    36    assumption
    37  | # m'
    38    # t
    39    # q'
    40    # II
    41    # H1
    42    # H2
     31 [1:
     32   #_ #K assumption
     33 |2:
     34   #m' #t #q' #II #H1 #H2
    4335   normalize
    44    change with (orb ??) in H2: (??%?);
     36   change with (orb ??) in H2:(??%?);
    4537   cases (inclusive_disjunction_true … H2)
    46    [ # K
    47      < (eq_a_to_eq … K)
    48      > H1
    49      %
    50    | # K
    51      > II
     38   [1:
     39     #K
     40     <(eq_a_to_eq … K) >H1 %
     41   |2:
     42     #K
     43     >II
    5244     try assumption
    5345     cases (is_a t a)
Note: See TracChangeset for help on using the changeset viewer.