Changeset 1941


Ignore:
Timestamp:
May 14, 2012, 4:33:20 PM (8 years ago)
Author:
mulligan
Message:

Changes to the AssemblyProof? with a few more (large) axioms closed.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1939 r1941  
    2121  |2:
    2222    letin res ≝ (bit ::: prefix)
    23     <minus_S_S
    24     >minus_Sn_m
    25     [1:
    26       @res
    27     |2:
    28       assumption
    29     ]
     23    <minus_S_S >minus_Sn_m
     24    try assumption @res
    3025  |3:
    3126    @le_S_to_le
     
    5348  |2:
    5449    normalize
    55     cases c
    56     [1:
    57       normalize //
    58     |2:
    59       normalize //
    60     ]
     50    cases c normalize //
    6151  ]
    6252qed.
     
    7868  |2:
    7969    letin res ≝ (bit ::: prefix)
    80     <(minus_S_S ? ?)
    81     >(minus_Sn_m ? ?)
    82     [1:
    83       @res
    84     |2:
    85       @prf2
    86     ]
     70    <(minus_S_S ? ?) >(minus_Sn_m ? ?)
     71    try @prf2 @res
    8772  |3:
    8873    /2/
     
    9479  λP: BitVector n → bool.
    9580    bitvector_elim_internal n P n ? ?.
    96   [ @(le_n ?)
    97   | <(minus_n_n ?)
    98     @[[ ]]
    99   ]
     81  try @le_n
     82  <minus_n_n @[[]]
    10083qed.
    10184
     
    943926lemma eq_instruction_refl:
    944927  ∀i. eq_instruction i i = true.
    945   #i cases i
    946   [1,2,3,4,5,6:
    947     #arg1 @eq_addressing_mode_refl
    948   |7:
    949     #arg1 #arg2
    950     whd in ⊢ (??%?);
    951     >eq_addressing_mode_refl
    952     >eq_addressing_mode_refl %
    953   |8:
    954     #arg @eq_preinstruction_refl
    955   ]
     928  #i cases i [*: #arg1 ]
     929  try @eq_addressing_mode_refl
     930  try @eq_preinstruction_refl
     931  #arg2 whd in ⊢ (??%?);
     932  >eq_addressing_mode_refl >eq_addressing_mode_refl %
    956933qed.
    957934
     
    11501127    p = q → 〈p, r〉 = 〈q, r〉.
    11511128  #A #p #q #r #hyp
    1152   >hyp %
     1129  destruct %
    11531130qed.
    11541131
     
    11581135    p = q → 〈r, p〉 = 〈r, q〉.
    11591136  #A #p #q #r #hyp
    1160   >hyp %
     1137  destruct %
    11611138qed.
    11621139
     
    11681145  #A #n #q #r
    11691146  generalize in match (Vector_O A q …);
    1170   #hyp >hyp in ⊢ (??%?); %
     1147  #hyp destruct %
    11711148qed.
    11721149
     
    12051182  [1:
    12061183    #n #l #r #v #hd #eq #hyp
    1207     destruct
    1208     >(Vector_O … l) %
     1184    destruct >(Vector_O … l) %
    12091185  |2:
    12101186    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
     
    12141190    >tail_head
    12151191    <(? : split A (S m') n (l@@r) = split' A (S m') n (l@@r))
    1216     [1:
    1217       <hyp <head_head' %
    1218     |2:
    1219       elim l normalize //
    1220     ]
     1192    try (<hyp <head_head' %)
     1193    elim l normalize //
    12211194  ]
    12221195qed.
     
    12401213    cases (Vector_Sn A r v) #hd #exists
    12411214    cases exists #tl #jmeq
    1242     >jmeq
    1243     @split_succ try %
     1215    >jmeq @split_succ try %
    12441216    @ih %
    12451217  ]
     
    12751247  λl, m: nat.
    12761248  λv: Vector a (l + m).
    1277   λP.
    1278   match v return λn: nat. λv: Vector a (n + m).
    1279     (∀vl: Vector a ?.
    1280      ∀vm: Vector a m.
    1281       v = vl@@vm → P 〈vl,vm〉) → P (split a ? m v) with
    1282   [ VEmpty ⇒ ?
    1283   | VCons v' hd tl ⇒ ?
    1284   ] ?.
     1249  λP. ?.
     1250  cases daemon
     1251qed.
    12851252
    12861253(* XXX: this looks almost certainly wrong *)
     
    13281295  ].
    13291296
     1297axiom add_bitvector_of_nat_Sm:
     1298  ∀n, m: nat.
     1299    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
     1300      bitvector_of_nat n (S m).
     1301
    13301302lemma encoding_check_append:
    13311303  ∀code_memory: BitVectorTrie Byte 16.
    1332   ∀final_pc: nat.
     1304  ∀final_pc: Word.
    13331305  ∀l1: list Byte.
    1334   ∀pc: nat.
     1306  ∀pc: Word.
    13351307  ∀l2: list Byte.
    1336     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
    1337       let intermediate_pc ≝ pc + length … l1 in
    1338         encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
    1339           encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
     1308    encoding_check code_memory pc final_pc (l1@l2) →
     1309      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
     1310        encoding_check code_memory pc pc_plus_len l1 ∧
     1311          encoding_check code_memory pc_plus_len final_pc l2.
    13401312  #code_memory #final_pc #l1 elim l1
    13411313  [1:
    13421314    #pc #l2
    13431315    whd in ⊢ (????% → ?); #H
    1344     <plus_n_O
     1316    <add_zero
    13451317    whd whd in ⊢ (?%?); /2/
    13461318  |2:
    13471319    #hd #tl #IH #pc #l2 * #H1 #H2
    1348     >half_add_SO in H2; #H2
    1349     cases (IH … H2) <plus_n_Sm
    1350     #K1 #K2 % [2: @K2 ] whd % //
    1351     >half_add_SO @K1
     1320(*    >half_add_SO in H2; #H2 *)
     1321    cases (IH … H2) #E1 #E2 %
     1322    [1:
     1323      % try @H1
     1324      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
     1325      <add_associative #assm assumption
     1326    |2:
     1327      <add_associative in E2;
     1328      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
     1329      assumption
     1330    ]
    13521331  ]
    13531332qed.
    13541333
    1355 axiom bitvector_3_elim_prop:
     1334axiom bitvector_3_cases:
     1335  ∀b: BitVector 3.
     1336  ∃l, c, r: bool.
     1337    b = [[l; c; r]].
     1338
     1339lemma bitvector_3_elim_prop:
    13561340  ∀P: BitVector 3 → Prop.
    13571341    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
    13581342    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
    13591343    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
     1344  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     1345  cases (bitvector_3_cases … H9) #l #assm cases assm
     1346  -assm #c #assm cases assm
     1347  -assm #r #assm cases assm destruct
     1348  cases l cases c cases r //
     1349qed.
    13601350
    13611351definition ticks_of_instruction ≝
     
    13661356
    13671357lemma fetch_assembly:
    1368   ∀pc: nat.
     1358  ∀pc: Word.
    13691359  ∀i: instruction.
    13701360  ∀code_memory: BitVectorTrie Byte 16.
     
    13721362    assembled = assembly1 i →
    13731363      let len ≝ length … assembled in
    1374         encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    1375         let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
    1376         let 〈instr_pc, ticks〉 ≝ fetched in
    1377         let 〈instr,pc'〉 ≝ instr_pc in
    1378          (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
     1364      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
     1365        encoding_check code_memory pc pc_plus_len assembled →
     1366          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
     1367           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
    13791368  #pc #i #code_memory #assembled cases i [8: *]
    13801369 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
     
    14301419axiom eq_instruction_to_eq:
    14311420  ∀i1, i2: instruction.
    1432     eq_instruction i1 i2 = true → i1 = i2.
     1421    eq_instruction i1 i2 = true → i1 i2.
    14331422         
    1434 (*     
    14351423lemma fetch_assembly_pseudo':
    14361424  ∀lookup_labels.
    1437   ∀pol: policy_type lookup_labels.
     1425  ∀sigma: Word → Word × bool.
    14381426  ∀ppc.
    14391427  ∀lookup_datalabels.
     
    14431431  ∀assembled.
    14441432  ∀instructions.
    1445   ∀pc.
    1446     let expansion ≝ pol ppc in
    1447       instructions = expand_pseudo_instruction lookup_labels ppc expansion lookup_datalabels pi →
    1448         〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels pol ppc lookup_datalabels pi →
    1449         encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    1450           fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
    1451   #lookup_labels #pol #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
    1452   #EQ1 whd in ⊢ (???% → ?); <EQ1 whd in ⊢ (???% → ?); #EQ2
    1453   cases (pair_destruct ?????? EQ2) -EQ2; #EQ2a #EQ2b
    1454   >EQ2a >EQ2b -EQ2a -EQ2b;
    1455   generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
     1433    let 〈pc, force_long_jump〉 ≝ sigma ppc in
     1434      instructions = expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi →
     1435        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi →
     1436          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
     1437            encoding_check code_memory pc pc_plus_len assembled →
     1438              fetch_many code_memory pc_plus_len pc instructions.
     1439  #lookup_labels #sigma #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
     1440  generalize in match (refl … (sigma ppc));
     1441  cases (sigma ?) in ⊢ (??%? → %); #pc #force_long_jump #sigma_refl normalize nodelta
     1442  #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
     1443  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
     1444  >len_refl >assembled_refl -len_refl
     1445  generalize in match (add 16 pc
     1446    (bitvector_of_nat 16
     1447     (|flatten (Vector bool 8)
     1448       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
     1449  #final_pc
    14561450  generalize in match pc; elim instructions
    14571451  [1:
    14581452    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
    14591453  |2:
    1460     #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
    1461     generalize in match (fetch_assembly pc i code_memory … (refl …) H1);
    1462     cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %);
    1463     cases newi_pc #newi #newpc whd in ⊢ (% → %); #K cases (conjunction_true … K) -K; #K1
    1464     cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
     1454    #i #tl #IH #pc #H whd
     1455    cases (encoding_check_append ????? H) -H #H1 #H2
     1456    @pair_elim #instr_pc #ticks #fetch_refl normalize nodelta
     1457    @pair_elim #instr #pc' #instr_pc_refl normalize nodelta
     1458    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);
     1459    #H3 lapply (H3 H1) -H3 >fetch_refl >instr_pc_refl normalize nodelta
     1460    #H3 lapply (conjunction_true ?? H3) * #H4 #H5 %
    14651461    [1:
    1466       @K1
     1462      lapply (conjunction_true … H4) * #B1 #B2
     1463      % try assumption @eqb_true_to_eq
     1464      <(eq_instruction_to_eq … B1) assumption
    14671465    |2:
    1468       @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2
    1469     |3:
    1470       >(eq_bv_eq … K3) @IH @H2
     1466      >(eq_bv_eq … H5) @IH @H2
    14711467    ]
    14721468  ]
    14731469qed.
    1474 *)
    1475 
    1476 axiom bitvector_of_nat_nat_of_bitvector:
    1477   ∀n,v.
    1478     bitvector_of_nat n (nat_of_bitvector n v) = v.
    1479 
    1480 (* CSC: soo long next one; can we merge with previous one now? *)
     1470
    14811471lemma fetch_assembly_pseudo:
    14821472  ∀program: pseudo_assembly_program.
    1483   ∀pol: policy program.
    1484   let lookup_labels ≝ λx:Identifier.sigma … pol (address_of_word_labels_code_mem (\snd  program) x) in
     1473  ∀sigma: Word → Word × bool.
     1474  let lookup_labels ≝ λx:Identifier.\fst (sigma (address_of_word_labels_code_mem (\snd  program) x)) in
    14851475  ∀ppc.∀code_memory.
    14861476  let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    1487   let pc ≝ sigma program pol ppc in
    14881477  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
    1489   let instructions ≝ expand_pseudo_instruction lookup_labels ppc (pol lookup_labels ppc) lookup_datalabels pi in
    1490   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels pi in
    1491     encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
    1492      fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
    1493  #program #pol letin lookup_labels ≝ (λx.?) #ppc #code_memory
     1478  let pc ≝ \fst (sigma ppc) in
     1479  let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
     1480  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
     1481  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
     1482    encoding_check code_memory pc pc_plus_len assembled →
     1483      fetch_many code_memory pc_plus_len pc instructions.
     1484 #program #sigma letin lookup_labels ≝ (λx.?) #ppc #code_memory
    14941485 letin lookup_datalabels ≝ (λx.?)
    1495  letin pc ≝ (sigma ???) letin pi ≝ (fst ???) 
     1486 letin pi ≝ (fst ???)
     1487 letin pc ≝ (fst ???)
    14961488 letin instructions ≝ (expand_pseudo_instruction ?????)
    1497  @pair_elim #len #assembled #EQ1 #H
     1489 @pair_elim #len #assembled #assembled_refl normalize nodelta
     1490 #H
    14981491 generalize in match
    1499   (fetch_assembly_pseudo' lookup_labels ((pi1 ?? pol) lookup_labels) ppc lookup_datalabels pi code_memory len
    1500    assembled instructions (nat_of_bitvector ? pc)) in ⊢ ?;
    1501   >bitvector_of_nat_nat_of_bitvector >EQ1 normalize nodelta
    1502   #X @X //
    1503 qed.
    1504 
    1505 (* This is a trivial consequence of fetch_assembly + the proof that the
     1492  (fetch_assembly_pseudo' lookup_labels sigma ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
     1493 #X destruct
     1494 cases (sigma ppc) in H X; #pc #force_long_jump normalize nodelta
     1495 #H #X @X try % <assembled_refl try % assumption
     1496qed.
     1497
     1498(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
    15061499   function that load the code in memory is correct. The latter is based
    15071500   on missing properties from the standard library on the BitVectorTrie
    1508    data structrure. *)
     1501   data structrure.
     1502   
     1503   Wrong at the moment, requires Jaap's precondition to ensure that the program
     1504   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
     1505*)
    15091506axiom assembly_ok:
    1510  ∀program,pol,assembled,costs'.
    1511   let 〈labels,costs〉 ≝ build_maps program pol in
    1512   〈assembled,costs'〉 = assembly program pol
     1507 ∀program,sigma,assembled,costs'.
     1508  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     1509  〈assembled,costs'〉 = assembly program sigma
    15131510  costs = costs' ∧
    15141511  let code_memory ≝ load_code_memory assembled in
    1515   let preamble ≝ \fst program in
    1516   let datalabels ≝ construct_datalabels preamble in
    1517   let lookup_labels ≝ λx.sigma … pol (address_of_word_labels_code_mem (\snd program) x) in 
     1512  let datalabels ≝ construct_datalabels (\fst program) in
     1513  let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 
    15181514  let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
    15191515  ∀ppc.
    1520   let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in
    1521    ∀len,assembledi.
    1522      〈len,assembledi〉 = assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels (\fst pi_newppc) →
    1523       encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
    1524        sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    1525 
     1516  let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     1517  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
     1518  let pc ≝ \fst (sigma ppc) in
     1519  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
     1520   encoding_check code_memory pc pc_plus_len assembled ∧
     1521       \fst (sigma newppc) = add … pc (bitvector_of_nat … len).
     1522
     1523(* XXX: should we add that costs = costs'? *)
    15261524lemma fetch_assembly_pseudo2:
    1527  ∀program,pol,ppc.
    1528 (*  let 〈labels,costs〉 ≝ build_maps program pol in *)
    1529   let assembled ≝ \fst (assembly program pol) in
     1525 ∀program,sigma,ppc.
     1526  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     1527  let 〈assembled, costs'〉 ≝ assembly program sigma in
    15301528  let code_memory ≝ load_code_memory assembled in
    15311529  let data_labels ≝ construct_datalabels (\fst program) in
    1532   let lookup_labels ≝ λx.sigma … pol (address_of_word_labels_code_mem (\snd program) x) in
     1530  let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 
    15331531  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    15341532  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1535   let instructions ≝ expand_pseudo_instruction lookup_labels ppc (pol lookup_labels ppc) lookup_datalabels pi in
    1536    fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
    1537  * #preamble #instr_list #pol #ppc
    1538  letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol))
    1539  letin code_memory ≝ (load_code_memory assembled)
    1540  letin data_labels ≝ (construct_datalabels preamble)
    1541  letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
    1542  letin lookup_datalabels ≝ (λx. lookup_def ? ? data_labels x (zero ?))
    1543  @pair_elim #pi #newppc #EQ1 change with (fetch_pseudo_instruction instr_list ? = ?) in EQ1;
    1544  generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)));
    1545  @pair_elim #labels #costs #EQ2 <eq_pair_fst_snd
    1546  #H cases (H (refl \ldots)) -H; #EQ3
    1547  generalize in match (refl … (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels ?));
    1548  [ cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?); #len #assembledi #EQ4
    1549    #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
    1550    (* XXX JPB: attention to lookup_labels *)
    1551    generalize in match (fetch_assembly_pseudo 〈preamble,instr_list〉 pol ppc (load_code_memory assembled)) in ⊢ ?;
    1552    >EQ4; #H generalize in match (H H1) in ⊢ ?; -H >(pair_destruct_2 ????? (sym_eq … EQ1))
    1553    >H2 >EQ1 #K @K
     1533  let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
     1534    fetch_many code_memory (\fst (sigma newppc)) (\fst (sigma ppc)) instructions.
     1535  * #preamble #instr_list #sigma #ppc
     1536  @pair_elim #labels #costs #create_label_map_refl
     1537  @pair_elim #assembled #costs' #assembled_refl
     1538  letin code_memory ≝ (load_code_memory ?)
     1539  letin data_labels ≝ (construct_datalabels ?)
     1540  letin lookup_labels ≝ (λx. ?)
     1541  letin lookup_datalabels ≝ (λx. ?)
     1542  @pair_elim #pi #newppc #fetch_pseudo_refl
     1543  lapply (assembly_ok 〈preamble, instr_list〉 sigma assembled costs')
     1544  @pair_elim #labels' #costs' #create_label_map_refl' #H
     1545  cases (H (sym_eq … assembled_refl))
     1546  #_
     1547  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi))
     1548  cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?);
     1549  #len #assembledi #EQ4 #H
     1550  lapply (H ppc) >fetch_pseudo_refl #H
     1551  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma ppc (load_code_memory assembled))
     1552  >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
     1553  >fetch_pseudo_refl in H1; #assm @assm assumption
    15541554qed.
    15551555
  • src/ASM/Fetch.ma

    r1642 r1941  
    1010definition code_memory_size ≝ bitvector_max_nat 16.
    1111
     12definition add ≝
     13  λn: nat.
     14  λl, r: BitVector n.
     15    \snd (half_add n l r).
     16
     17axiom add_zero:
     18  ∀n: nat.
     19  ∀l: BitVector n.
     20    l = add n l (zero …).
     21
     22axiom add_associative:
     23  ∀n: nat.
     24  ∀l, c, r: BitVector n.
     25    add … l (add … c r) = add … (add … l c) r.
     26
     27include alias "ASM/BitVectorTrie.ma".
     28
    1229definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
    1330  λpmem: BitVectorTrie Byte 16.
    1431  λpc: Word.
    15     〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
     32    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
    1633
    1734lemma Prod_inv_rect_Type0:
Note: See TracChangeset for help on using the changeset viewer.