Changeset 1592 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Dec 7, 2011, 2:50:59 PM (8 years ago)
Author:
boender
Message:
  • updated definitions to work with programs of maximum 216 instructions
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1578 r1592  
    553553  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
    554554  let bv: list (BitVector 8) ≝ match ilist with
    555     [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
     555    [ None   ⇒ (* this shouldn't happen *) [ ]
    556556    | Some l ⇒ flatten … (map … assembly1 l)
    557557    ] in
     
    777777   ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).
    778778 
    779 axiom bitvector_of_nat_abs:
    780   ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).
    781 
    782779lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
    783780 /2/ qed.
     781 
     782lemma bitvector_of_nat_ok:
     783  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
     784 #n elim n -n
     785 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
     786 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
     787 ]
     788qed.
     789
     790lemma bitvector_of_nat_abs:
     791  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
     792 #n #x #y #Hx #Hy #Heq @notb_elim
     793 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
     794 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
     795 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H //
     796 | #H //
     797 ]
     798qed.
     799
    784800
    785801lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    786802 ∀policy:(Σp:jump_expansion_policy.
    787  (∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     803 (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    788804 jump_in_policy prefix p).
    789805  ∀i:ℕ.i < |prefix| →
     
    802818qed.
    803819 
    804 definition jump_expansion_start: ∀program:list labelled_instruction.
     820definition jump_expansion_start:
     821  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    805822  Σpolicy:jump_expansion_policy.
    806     (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     823    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    807824    jump_in_policy program policy ∧
    808825    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
     
    811828  foldl_strong (option Identifier × pseudo_instruction)
    812829  (λprefix.Σpolicy:jump_expansion_policy.
    813     (∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     830    (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    814831    jump_in_policy prefix policy ∧
    815832    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
     
    842859  #i >append_length <commutative_plus #Hi normalize in Hi;
    843860  [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,57,59,61:
    844    cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i)
    845    [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,58,60,62:
    846     <Hi @le_n_Sn
    847    ]
    848    @le_S_to_le @le_S_to_le @Hi
     861   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i)
     862   [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
     863     @le_S_to_le @le_S_to_le @Hi
     864   |2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122:
     865     @Hi2
     866   |3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123:
     867     <Hi @le_n_Sn
     868   |4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124:
     869     @Hi2
     870   ]
    849871  ]
    850872  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     
    858880   ]
    859881   #H elim H; -H; #t1 #H elim H; -H #t2 #H
    860    lapply (proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)))
    861    #H2 >H2 in H; #H destruct (H)
     882   >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
     883   [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,57,59,61:
     884     #H destruct (H)
     885   ]
     886   @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
     887   @le_plus_n_r
    862888 ]
    863889 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
     
    872898 [1,3,5,7,9,11,13,15,17,19,21: @conj
    873899  [1,3,5,7,9,11,13,15,17,19,21:
    874     #i >append_length <commutative_plus #Hi normalize in Hi; >lookup_opt_insert_miss
     900    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
    875901   [1,3,5,7,9,11,13,15,17,19,21:
    876      @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
    877    ]
    878    >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
     902     @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     903   ]
     904   >eq_bv_sym @bitvector_of_nat_abs
     905   [1,4,7,10,13,16,19,22,25,28,31:
     906     @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
     907     @le_plus_n_r
     908   |2,5,8,11,14,17,20,23,26,29,32: @Hi2
     909   |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
     910   ]
    879911  ]
    880912  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
     
    885917    @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
    886918   ]
    887    @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi))
     919   @bitvector_of_nat_abs
     920   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
     921   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     922   ]
     923   @(transitive_lt … (sig2 ?? program))
     924   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    888925  ]
    889926  @conj >(injective_S … Hi) #H
     
    900937   @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi) Hj)
    901938  ]
    902   @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi))
     939  @bitvector_of_nat_abs
     940  [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
     941  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     942  ]
     943  @(transitive_lt … (sig2 ?? program))
     944  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    903945 ]
    904946 #_ >(injective_S … Hi) @lookup_opt_insert_hit
     
    915957  jump_expansion_policy → Prop ≝
    916958 λprogram.λop.λp.
    917   (* (∀i:ℕ.i < |program| →
    918     lookup_opt … (bitvector_of_nat ? i) op = lookup_opt … (bitvector_of_nat ? i) p) ∨ *)
    919959  (∀i:ℕ.i < |program| →
    920960    jmpleq
     
    922962      (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))).
    923963   
    924 definition jump_expansion_step: ∀program:list labelled_instruction.
     964definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    925965  ∀old_policy:(Σpolicy.
    926     (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     966    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    927967    jump_in_policy program policy).
    928968  (Σpolicy.
    929     (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     969    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    930970    jump_in_policy program policy ∧
    931971    policy_increase program old_policy policy)
     
    936976    foldl_strong (option Identifier × pseudo_instruction)
    937977    (λprefix.ℕ × Σpolicy.
    938       (∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     978      (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    939979      jump_in_policy prefix policy ∧
    940980      policy_increase prefix old_policy policy
     
    9651005    final_policy.
    9661006[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
    967 [ cases (lookup ??? old_policy ?) #h #n cases add_instr
    968   [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
     1007[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
     1008  [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    9691009  | #z normalize nodelta >lookup_opt_insert_miss
    970     [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
    971     | >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
     1010    [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     1011    | >eq_bv_sym @bitvector_of_nat_abs
     1012      [ @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1013        @le_S_S @le_plus_n_r
     1014      | @Hi2
     1015      | @lt_to_not_eq @Hi
     1016      ]
    9721017    ]
    9731018  ]
     
    9791024      | #z elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #Hn
    9801025        % [ @h | % [ @n | <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs
    981             @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) ] ]
     1026        [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     1027        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     1028        ]
     1029        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1030        @le_S_S @le_plus_n_r
     1031        ] ]
    9821032      ]
    9831033    | lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
     
    9851035      normalize nodelta #x #y [2: #z]
    9861036      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?))
    987       [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
     1037      [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
     1038        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
     1039        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     1040        ]
     1041        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1042        @le_S_S @le_plus_n_r
    9881043      | @Hl
    9891044      ]
     
    9941049     [3,5,11: #H @⊥ @H (* instr is not a jump *)
    9951050     |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    996        #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)))
    997        #H destruct (H)
     1051       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1052       [1,3,5: #H destruct (H)]
     1053       @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1054       @le_S_S @le_plus_n_r
    9981055     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n
    9991056       whd in match (snd ???); @(ex_intro ?? pc)
     
    10161073       |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    10171074        #x #y normalize nodelta
    1018         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
     1075        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1076        [1,3,5: #H destruct (H)]
     1077        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1078        @le_S_S @le_plus_n_r     
    10191079       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
    10201080        #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    10211081        #x #y normalize nodelta
    1022         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
     1082        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1083        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
     1084        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1085        @le_S_S @le_plus_n_r
    10231086       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
    10241087        cases (lookup ??? old_policy ?) #x #y normalize nodelta
    1025         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
     1088        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1089        [1,3,5,7,9,11,13: #H destruct (H)]
     1090        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1091        @le_S_S @le_plus_n_r             
    10261092       |46,47,51,52: #id #_ //
    10271093       |48,49,50,53,54: #x #id #_ //
     
    10411107        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    10421108          #x #y normalize nodelta
    1043           >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) //
     1109          >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1110          [ //
     1111          | @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1112            @le_S_S @le_plus_n_r
     1113          ]
    10441114        ]
    1045       | >(proj1 ?? (jump_not_in_policy program old_policy (|prefix|) ?))
     1115      | >(proj1 ?? (jump_not_in_policy (eject … program) old_policy (|prefix|) ?))
    10461116        [ //
    10471117        | >prf >p1 >nth_append_second [ <minus_n_n
     
    10691139      #y #z normalize nodelta normalize nodelta >lookup_insert_miss
    10701140      [ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
    1071       | @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
     1141      | @bitvector_of_nat_abs
     1142        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
     1143        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
     1144        ]
     1145        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1146        @le_S_S @le_plus_n_r
    10721147      ]
    10731148    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (|prefix|) ?) ?)
     
    11011176qed.
    11021177 
    1103 let rec jump_expansion_internal (program: list labelled_instruction)
     1178let rec jump_expansion_internal (program: Σl:list labelled_instruction.|l| < 2^16)
    11041179  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
    11051180    And
    1106     (∀i:ℕ.i ≥ |program| → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
     1181    (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
    11071182    (jump_in_policy program policy)) ≝
    11081183  match n with
     
    11521227#n (elim n) normalize /2 by S_pred/ qed.
    11531228
    1154 lemma pe_step: ∀program:list labelled_instruction.
     1229lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    11551230 ∀p1,p2:Σpolicy.
    1156  (∀i:ℕ.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
     1231 (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
    11571232 ∧jump_in_policy program policy.
    11581233  policy_equal program p1 p2 →
     
    11791254qed.
    11801255   
    1181 lemma equal_remains_equal: ∀program:list labelled_instruction.∀n:ℕ.
     1256lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
    11821257  policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
    11831258  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
     
    12501325qed.
    12511326
    1252 (* lemma de_morgan1:
    1253  ∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B.
    1254  #A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA | @H ] | @Hnot ]
    1255 qed. *)
    1256 
    12571327lemma thingie:
    12581328  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
     
    12681338qed.
    12691339
    1270 (* lemma incr_or_equal: ∀program:list labelled_instruction.
    1271   ∀policy:(Σp:jump_expansion_policy.
    1272     (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    1273     jump_in_policy program p).
    1274   policy_equal program policy (jump_expansion_step program policy) ∨
    1275   ∃n:ℕ.n < (|program|) ∧ jmple
    1276     (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
    1277     (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
    1278  #program #policy cases (dec_bounded_exists
    1279    (λk.
    1280      \snd (bvt_lookup ?? (bitvector_of_nat ? k) policy 〈0,short_jump〉) ≠
    1281      \snd (bvt_lookup ?? (bitvector_of_nat ? k) (jump_expansion_step program policy) 〈0,short_jump〉))
    1282    ? (|program|))
    1283    [ #H %2 elim H -H; #i #Hi
    1284      cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) i (proj1 ?? Hi))
    1285      [ #H @(ex_intro ?? i (conj ?? (proj1 ?? Hi) H))
    1286      | #H @⊥ @(absurd ? H (proj2 ?? Hi))
    1287      ]
    1288    | #H %1 whd #i #Hi @(thingie ? (dec_eq_jump_length ??)) elim H -H #H; @nmk #H2 @H
    1289      @(ex_intro … i) @conj [ @Hi | @H2 ]
    1290    | #n cases (dec_eq_jump_length (\snd (lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉))
    1291      (\snd (lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)))
    1292      [ #H %2 @nmk #H1 elim H1 #H2 @H2 @H
    1293      | #H %1 @H
    1294      ]
    1295    ]
    1296 qed. *)
    1297 
    1298 lemma policy_not_equal_incr: ∀program:list labelled_instruction.
     1340lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
    12991341 ∀policy:(Σp:jump_expansion_policy.
    1300     (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     1342    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    13011343    jump_in_policy program p).
    13021344  ¬policy_equal program policy (jump_expansion_step program policy) →
     
    13381380  λprogram.λpolicy.measure_int program policy 0.
    13391381 
    1340 (* lemma measure_le: ∀program.∀policy.∀x,y:ℕ.
    1341   x ≤ y → measure_int program policy x ≤ measure_int program policy y.
    1342  #program #policy
    1343  elim program
    1344  [ //
    1345  | #h #t #Hind #x #y #Hxy whd in match (measure_int ??x); whd in match (measure_int ??y);
    1346    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
    1347    [ @Hind @Hxy
    1348    |2,3: @Hind @monotonic_le_plus_l @Hxy
    1349    ]
    1350  ]
    1351 qed. *)
    1352 
    13531382lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
    13541383  measure_int program policy (x+d) = measure_int program policy x + d.
     
    13671396qed.
    13681397   
    1369 lemma measure_incr_or_equal: ∀program.∀policy:Σp:jump_expansion_policy.
    1370     (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     1398lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
     1399  ∀policy:Σp:jump_expansion_policy.
     1400    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    13711401    jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
    13721402  measure_int l policy acc ≤ measure_int l (jump_expansion_step program policy) acc.
    1373 #program #policy #l (* lapply (le_n (|program|)) *) elim l -l;
     1403#program #policy #l elim l -l;
    13741404  [ #Hp #acc normalize @le_n
    13751405  | #h #t #Hind #Hp #acc
     
    14611491qed.
    14621492
    1463 lemma measure_special: ∀program.∀policy:Σp:jump_expansion_policy.
    1464     (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     1493(* how to do this with a sigma-type and elimination? *)
     1494lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     1495  ∀policy:Σp:jump_expansion_policy.
     1496    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    14651497    jump_in_policy program p.
    14661498  measure_int program policy 0 = measure_int program (jump_expansion_step program policy) 0 →
    14671499  policy_equal program policy (jump_expansion_step program policy).
    1468  #program lapply (le_n (|program|)) elim program in ⊢ (?%? → ∀policy.??(?%??)(?%??) → ?%??);
    1469  [ #_ #policy #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
    1470  | #h #t #Hind #Hp #policy #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
     1500#program #policy lapply (le_n (|program|)) @(list_ind ?
     1501  (λx.|x| ≤ |program| → measure_int x (eject … policy) 0 = measure_int x (eject … (jump_expansion_step program policy)) 0 →
     1502      policy_equal x (eject … policy) (eject … (jump_expansion_step program policy)))
     1503   ?? program)
     1504 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
     1505 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    14711506   [ #Hi @Hind
    14721507     [ @(transitive_le … Hp) //
     
    15311566qed.
    15321567 
    1533 lemma measure_zero: ∀l.∀program.
     1568lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
    15341569  |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 0 = 0.
    1535  #l #program elim l (* lapply (le_n (|program|)) elim program in ⊢ (?%? → ?%(?%??)?); *)
     1570 #l #program elim l
    15361571 [ //
    15371572 | #h #t #Hind #Hp whd in match (measure_int ???);
     
    15471582qed.
    15481583 
    1549 definition je_fixpoint: ∀program:list labelled_instruction.
     1584definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    15501585  Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
    15511586 #program @(dp … (jump_expansion_internal program (2*|program|)))
     
    15991634qed.
    16001635
     1636let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
     1637  BitVectorTrie jump_length 16 ≝
     1638  match n with
     1639  [ O    ⇒ acc
     1640  | S n' ⇒
     1641    match lookup_opt … (bitvector_of_nat 16 n') policy with
     1642    [ None   ⇒ transform_policy n' policy acc
     1643    | Some x ⇒ let 〈pc,length〉 ≝ x in
     1644      transform_policy n' policy (insert … pc length acc)
     1645    ]
     1646  ].
     1647
    16011648(**************************************** START OF POLICY ABSTRACTION ********************)
    16021649
    1603 definition policy_type≝ Word → jump_length.
    1604 
    1605 definition jump_expansion': pseudo_assembly_program → policy_type ≝
     1650definition policy_type ≝ Word → jump_length.
     1651
     1652definition jump_expansion':
     1653 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
     1654 policy_type ≝
    16061655 λprogram.λpc.
    1607   let policy ≝ jump_expansion_internal (\snd program) (|\snd program|) in
    1608   let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in
    1609     j.
    1610  
     1656  let policy ≝
     1657    transform_policy (|\snd program|) (eject … (je_fixpoint (\snd program))) (Stub ??) in
     1658  lookup ? ? pc policy long_jump.
     1659/2 by Stub, dp/
     1660qed.
     1661
    16111662definition assembly_1_pseudoinstruction_safe ≝
    16121663  λprogram: pseudo_assembly_program.
Note: See TracChangeset for help on using the changeset viewer.