Changeset 1940 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 14, 2012, 4:05:55 PM (8 years ago)
Author:
boender
Message:
  • committed new version of final invariant
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1937 r1940  
    66include "ASM/Assembly.ma".
    77
    8 (*include alias "common/Identifiers.ma".
    9 include alias "ASM/BitVector.ma".*)
    108include alias "basics/lists/list.ma".
    119include alias "arithmetics/nat.ma".
     
    166164  match jmp_len with
    167165  [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ]
    168   | medium_jump ⇒ [ ] (* XXX this should not happen *)
     166  | medium_jump ⇒ [ ] (* this should not happen *)
    169167  | long_jump ⇒
    170168    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
     
    228226  | Call call ⇒
    229227    match jmp_len with
    230     [ short_jump ⇒ [ ] (* XXX this should not happen *)
     228    [ short_jump ⇒ [ ] (* this should not happen *)
    231229    | medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]
    232230    | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]
     
    406404qed.
    407405
     406lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
     407  #a #b / by refl/
     408qed.
     409
    408410(*lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    409411 ∀policy:(Σp:ppc_pc_map.
     
    431433  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    432434  ∀labels:label_map.
    433   Σpolicy:ppc_pc_map.
    434     And (out_of_program_none (pi1 ?? program) policy)
    435     (policy_isize_sum (pi1 ?? program) labels policy) ≝
     435  Σpolicy:option ppc_pc_map.
     436    match policy with
     437    [ None ⇒ True
     438    | Some p ⇒
     439       And (And (out_of_program_none (pi1 ?? program) p)
     440       (policy_isize_sum (pi1 ?? program) labels p))
     441       (\fst p < 2^16)
     442    ] ≝
    436443  λprogram.λlabels.
    437   foldl_strong (option Identifier × pseudo_instruction)
    438   (λprefix.Σpolicy:ppc_pc_map. 
     444  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
     445  (λprefix.Σpolicy:ppc_pc_map.
    439446    And (out_of_program_none prefix policy)
    440447    (policy_isize_sum prefix labels policy))
     
    462469   | _      ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    463470   ]〉
    464   ) 〈0, Stub ? ?〉.
    465 [ @conj
    466   [ #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
     471  ) 〈0, Stub ? ?〉 in
     472  if geb (\fst final_policy) 2^16 then
     473    None ?
     474  else
     475    Some ? (pi1 ?? final_policy).
     476[ / by I/
     477| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
     478  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
     479| @conj
     480  [ (* out_of_program_none *)
     481    #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
    467482    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    468483    cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi
     
    545560        ]
    546561      ]
    547 (*    | cases (le_to_or_lt_eq … Hi) -Hi #Hi
    548       [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj
    549         [ #Hj cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
    550           [1: #pi cases pi normalize nodelta
    551             [1,2,3,6,7,33,34,35,36,37: [1,2,3,4,5,6,7: #x #y] >lookup_insert_miss
    552               [2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs
    553                [1,4,7,10,13,16,19,22,25,28: @(transitive_lt … (pi2 ?? program)) >prf
    554                  >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    555                  @le_S_S_to_le @le_plus_n_r
    556                |2,5,8,11,14,17,20,23,26,29: @(transitive_lt … (pi2 ?? program)) >prf
    557                  >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    558                |3,6,9,12,15,18,21,24,27,30: @lt_to_not_eq @(le_S_S_to_le … Hi)
    559                ]
    560               ]
    561             |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x >lookup_insert_miss
    562               [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36: @bitvector_of_nat_abs
    563                [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52:
    564                  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    565                  @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r
    566                |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53:
    567                  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    568                  @le_S_S_to_le @le_plus_n_r
    569                |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54:
    570                  @lt_to_not_eq @(le_S_S_to_le … Hi)
    571                ]
    572               ]
    573             |9,10,11,12,13,14,15,16,17:
    574               [1,2,6,7: #x | 3,4,5,8,9: #x #id] >lookup_insert_miss
    575               [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    576                [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    577                  >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    578                  @le_S_S_to_le @le_plus_n_r
    579                |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    580                  >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    581                |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
    582                ]
    583               ]
    584              ]
    585           |2,3: #x >lookup_insert_miss
    586             [2,4: @bitvector_of_nat_abs
    587               [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    588                 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    589                 @le_S_S_to_le @le_plus_n_r
    590               |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    591                  >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    592               |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    593               ]
    594             ]
    595           |4,5: #id >lookup_insert_miss
    596             [2,4: @bitvector_of_nat_abs
    597               [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    598                  >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    599                  @le_S_S_to_le @le_plus_n_r
    600               |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    601                  >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    602               |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    603               ]
    604             ]
    605           |6: #x #id >lookup_insert_miss
    606             [2: @bitvector_of_nat_abs
    607               [ @(transitive_lt … (pi2 ?? program)) >prf
    608                 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    609                 @le_S_S_to_le @le_plus_n_r
    610               | @(transitive_lt … (pi2 ?? program)) >prf
    611                 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    612               | @lt_to_not_eq @(le_S_S_to_le … Hi)
    613               ]
    614             ]
    615           ]
    616           @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj)
    617         | #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i (le_S_S_to_le … Hi)))
    618           cases p in H; -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
    619           [1: #id cases id
    620             [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    621               [1,2,3,6,7,24,25: #x #y
    622               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    623               normalize nodelta >lookup_insert_miss
    624               [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    625                 @bitvector_of_nat_abs
    626                 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    627                  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    628                  @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r
    629                |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    630                  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    631                  @le_S_S_to_le @le_plus_n_r
    632                |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    633                  @lt_to_not_eq @(le_S_S_to_le … Hi)
    634                ]
    635              ] / by /
    636             |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #x #id]
    637               normalize nodelta >lookup_insert_miss
    638               [1,3,5,7,9,11,13,15,17: / by /
    639               |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    640                 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    641                   >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    642                   @le_S_S_to_le @le_plus_n_r
    643                 |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    644                   >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 
    645                 |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
    646                 ]
    647               ]
    648             ]
    649           |2,3: #x >lookup_insert_miss
    650             [2,4: @bitvector_of_nat_abs
    651               [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    652                  >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    653                  @le_S_S_to_le @le_plus_n_r
    654               |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    655                  >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    656               |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    657               ]
    658               |1,3: / by /
    659             ]
    660           |4,5: #id >lookup_insert_miss
    661             [2,4: @bitvector_of_nat_abs
    662               [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    663                  >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    664                  @le_S_S_to_le @le_plus_n_r
    665               |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    666                  >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    667               |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    668               ]
    669             |1,3: / by /
    670             ]
    671           |6: #x #id >lookup_insert_miss
    672             [2: @bitvector_of_nat_abs
    673               [@(transitive_lt … (pi2 ?? program)) >prf
    674                >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    675                @le_S_S_to_le @le_plus_n_r
    676               |@(transitive_lt … (pi2 ?? program)) >prf
    677                >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    678               |@lt_to_not_eq @(le_S_S_to_le … Hi)
    679               ]
    680             ]
    681             / by /
    682           ]
    683         ]
    684     | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
    685       <minus_n_n whd in match (nth ????); cases x #l #ins cases ins
    686       [1: #pi cases pi
    687         [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    688           [1,2,3,6,7,24,25: #x #y
    689           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    690           @conj
    691           [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    692             #H cases H in ⊢ ?;
    693           |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    694             cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p
    695             normalize nodelta >lookup_insert_hit #H destruct (H)
    696           ]
    697         |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
    698           @conj normalize nodelta
    699           [(*1: #_ @(ex_intro ?? (zero ?) (ex_intro ?? (bitvector_of_nat ? (lookup_def … labels x 0)) ?))*)
    700           1,3,5,7,9,11,13,15,17: #_ @(ex_intro ?? short_jump ?)
    701           |2,4,6,8,10,12,14,16,18: #_ / by I/
    702           ]
    703           cases p -p #p cases p -p #pc #pol #Hp >lookup_insert_hit @refl
    704         ]
    705       |2,3,6: #x [3: #id] @conj
    706         [1,3,5: #H cases H
    707         |2,4,6:
    708           cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p
    709           normalize nodelta >lookup_insert_hit #H destruct (H)
    710         ]
    711       |4,5: #x @conj
    712         [1,3: #_ @(ex_intro ?? (short_jump) ?)
    713           cases p -p #p cases p -p #pc #pol #Hp normalize nodelta >lookup_insert_hit @refl
    714         |2,4: #_ / by I/
    715         ]
    716       ]
    717     ]
    718   ] *)
    719562| cases daemon
    720563]
     
    739582  ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). *)
    740583 
    741 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
    742   #a #b / by refl/
    743 qed.
    744 
    745 include alias "common/Identifiers.ma".
     584(*include alias "common/Identifiers.ma".*)
    746585include alias "ASM/BitVector.ma".
    747586include alias "basics/lists/list.ma".
     
    763602    match y with
    764603    [ None ⇒ (* nec_plus_ultra program old_policy *) True
    765     | Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*)
     604    | Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p)
    766605       (policy_isize_sum program labels p))
    767606       (policy_increase program old_policy p))
     
    828667| lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
    829668  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
    830   #old_pc #old_length normalize nodelta
    831 (* XXX complicated proof *) cases daemon 
     669  #old_pc #old_length #Hpolicy @pair_elim #added #policy normalize nodelta
     670  @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
     671  @conj [ @conj [ @conj [ @conj
     672  [ (* out_of_program_none *) #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
     673    cases instr in Heq2; normalize nodelta
     674    #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
     675    [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i ? Hi2)
     676      @le_S_to_le @Hi
     677    |2,4,6,8,10,12: @bitvector_of_nat_abs
     678      [1,4,7,10,13,16: @Hi2
     679      |2,5,8,11,14,17: @(transitive_lt … Hi2) @Hi
     680      |3,6,9,12,15,18: @sym_neq @lt_to_not_eq @Hi
     681      ]
     682    ]
     683  | cases daemon (* XXX *)
     684  ]
     685  | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
     686    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     687    [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
     688      <(proj2 ?? (pair_destruct ?????? Heq2))     
     689      @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     690      [ @pair_elim #pc #j #EQ2 / by /
     691      | @bitvector_of_nat_abs
     692        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a
     693          @(le_S_S_to_le … Hi)
     694        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     695        | @lt_to_not_eq @(le_S_S_to_le … Hi)
     696        ]
     697      ]
     698    | <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi) >lookup_insert_hit
     699      cases instr in Heq1 Heq2;
     700      [2,3,6: #x [3: #y] normalize nodelta #Heq1 #Heq2 <(proj1 ?? (pair_destruct ?????? Heq1))
     701      cases daemon
     702      |1,4,5: cases daemon
     703      ]
     704    ]
     705  ]
     706  | (* policy_compact *) cases daemon
     707  ]
     708  | (* added = 0 → policy_equal *) cases daemon
     709  ]
    832710| normalize nodelta @conj [ @conj [ @conj [ @conj
    833711  [ #i #Hi / by refl/
     
    12631141  let labels ≝ create_label_map program in
    12641142  match n with
    1265   [ O   ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program labels))〉
     1143  [ O   ⇒ 〈true,pi1 ?? (jump_expansion_start program labels)〉
    12661144  | S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    12671145          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
     
    12721150          ] (refl … z)
    12731151  ].
    1274 [ normalize nodelta @conj
    1275   [ @(pi2 ?? (jump_expansion_start program (create_label_map program)))
    1276   | (* XXX *) cases daemon
     1152[ normalize nodelta cases (jump_expansion_start program (create_label_map program))
     1153  #p cases p
     1154  [ / by I/
     1155  | #pm / by I/
    12771156  ]
    12781157| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
     
    14481327qed.
    14491328
     1329(* uses the second part of policy_increase *)
    14501330lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
    14511331  ∀policy:Σp:ppc_pc_map.
     
    15291409qed.
    15301410
     1411(* uses second part of policy_increase *)
    15311412lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    15321413  ∀policy:Σp:ppc_pc_map.
     
    15731454     whd in match (measure_int ? p ?) in Hm;
    15741455     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp)
    1575      (* XXX *) cases daemon
    1576      (* change proof for not_jump
    1577      cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
     1456     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in   
    15781457Hm;
    1579      #x cases x -x #x1 #x2 #x3
    1580      cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
    1581      #y cases y -y #y1 #y2 #y3
    1582      normalize nodelta cases x3 cases y3 normalize nodelta
    1583      [1,5,9: #_ #_ //
     1458     #x1 #x2
     1459     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
     1460     #y1 #y2
     1461     normalize nodelta cases x2 cases y2 normalize nodelta
     1462     cases daemon
     1463     (* [1,5,9: #_ #_ //
    15841464     |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
    15851465     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
     
    16111491qed.
    16121492
     1493(* probably needs some kind of not_jump → short *)
    16131494lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
    1614   |l| ≤ |program| → measure_int l (jump_expansion_start program (create_label_map program)) 0 = 0.
    1615  #l #program elim l
    1616  [ //
    1617  | #h #t #Hind #Hp cases daemon
    1618  
    1619  (* old proof whd in match (measure_int ???);
    1620    cases daemo
    1621    cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    1622    [ lapply
    1623        (proj1 ?? (pi2 ??
    1624           (jump_expansion_start program (create_label_map program))))) 〈0,None ?〉)
     1495  match jump_expansion_start program (create_label_map program) with
     1496  [ None ⇒ True
     1497  | Some p ⇒ |l| ≤ |program| → measure_int l p 0 = 0
     1498  ].
     1499 #l #program lapply (refl ? (jump_expansion_start program (create_label_map program)))
     1500 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); #p #Hp #EQ
     1501 cases p in Hp EQ;
     1502 [ / by I/
     1503 | #pl normalize nodelta #Hpl #EQ elim l
     1504   [ / by refl/
     1505   | #h #t #Hind #Hp
     1506     cases daemon (*
     1507    cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    16251508     [ normalize nodelta @Hind @le_S_to_le ]
    16261509     @Hp
     
    17861669 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    17871670  option (Σsigma:Word → Word × bool.
    1788    ∀ppc.
     1671   ∀ppc:ℕ.
     1672    And (ppc ≤ (|\snd program|) →
    17891673    \snd
    17901674     (half_add ?
    1791       (\fst (sigma ppc))
     1675      (\fst (sigma (bitvector_of_nat 16 ppc)))
    17921676      (bitvector_of_nat ?
    17931677       (instruction_size
    17941678        (λid. bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) id 0))
    1795         sigma ppc (\fst (fetch_pseudo_instruction (\snd program) ppc)))))
    1796     = \fst (sigma (\snd (half_add ? ppc (bitvector_of_nat ? 1)))))
    1797 ≝ λprogram.
     1679        sigma (bitvector_of_nat ? ppc)
     1680         (\fst (fetch_pseudo_instruction (\snd program) (bitvector_of_nat ? ppc))))))
     1681    = (* \fst (sigma (\snd (half_add ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? 1)))) *)
     1682      \fst (sigma (bitvector_of_nat ? (S ppc))))
     1683    (ppc < (|\snd program|) →
     1684      Or (lt_u ? (\fst (sigma (bitvector_of_nat ? ppc))) (\fst (sigma (bitvector_of_nat ? (S ppc)))) = true)
     1685       (And (S ppc = (|\snd program|)) (\fst (sigma (bitvector_of_nat ? (S ppc))) = (zero 16))))
     1686  )
     1687≝ λprogram.? (*
    17981688  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
    17991689  match policy with
     
    18021692      «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
    18031693        〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
    1804   ].
     1694  ]*).
    18051695 cases daemon
    18061696qed.
Note: See TracChangeset for help on using the changeset viewer.