Ignore:
Timestamp:
Jun 28, 2012, 8:08:58 PM (8 years ago)
Author:
boender
Message:
  • committed working version
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2102 r2141  
    253253 ∀dest.is_jump_to instr dest →
    254254   let paddr ≝ lookup_def … labels dest 0 in
    255    let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)
    256    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    257    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in
     255   let addr ≝ bitvector_of_nat ? (if leb paddr (|prefix|) (* jump to address already known *)
     256   then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)
     257   else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    258258   match j with
    259259   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
     
    265265       \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
    266266   ].
    267 
    268267 
    269268(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
     
    324323  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    325324  let paddr ≝ lookup_def … labels lbl 0 in
    326   let addr ≝ bitvector_of_nat ? (if leb ppc paddr (* forward jump *)
    327   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    328   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
     325  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
     326  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
     327  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    329328  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
    330329  if sj_possible
     
    339338  let paddr ≝ lookup_def ? ? labels lbl 0 in
    340339  let addr ≝ bitvector_of_nat ?
    341     (if leb ppc paddr (* forward jump *)
    342     then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)
    343             + added
    344     else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
     340    (if leb paddr ppc (* jump to address already known *)
     341    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)
     342    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    345343  let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in   
    346344  if aj_possible
     
    354352  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    355353  let paddr ≝ lookup_def … labels lbl 0 in
    356   let addr ≝ bitvector_of_nat ? (if leb ppc paddr (* forward jump *)
    357   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    358   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
     354  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
     355  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
     356  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    359357  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
    360358  if sj_possible
     
    395393qed.
    396394
    397 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
    398   #a #b / by refl/
    399 qed.
    400 
    401 lemma nth_last: ∀A,a,l.
    402   nth (|l|) A l a = a.
    403  #A #a #l elim l
    404  [ / by /
    405  | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind
    406  ]
    407 qed.
    408 
    409395(* The first step of the jump expansion: everything to short. *)
    410396definition jump_expansion_start:
    411   ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
     397  ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    412398  ∀labels:label_map.
    413399  Σpolicy:option ppc_pc_map.
    414400    match policy with
    415401    [ None ⇒ True
    416     | Some p ⇒ And (And (And (And (And (And (And
     402    | Some p ⇒ And (And (And (And (And (And
    417403       (out_of_program_none (pi1 ?? program) p)
    418404       (not_jump_default (pi1 ?? program) p))
    419        (sigma_compact_unsafe program labels p))
    420405       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    421406       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
     407       (sigma_compact_unsafe program labels p))
    422408       (∀i.i ≤ |program| → ∃pc.
    423409         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
    424        (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) = Some ? 〈\fst p,short_jump〉))
    425        (\fst p < 2^16)
     410       (\fst p < 2^16)         
    426411    ] ≝
    427412  λprogram.λlabels.
    428413  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    429   (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And
     414  (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And
    430415    (out_of_program_none prefix policy)
    431416    (not_jump_default prefix policy))
    432     (sigma_compact_unsafe prefix labels policy))
    433417    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    434418    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
     419    (sigma_compact_unsafe prefix labels policy))
    435420    (∀i.i ≤ |prefix| → ∃pc.
    436421      bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
    437     (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd policy) =
    438       Some ? 〈\fst policy,short_jump〉))
    439422  program
    440423  (λprefix.λx.λtl.λprf.λp.
     
    451434| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    452435  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    453 | @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     436| @conj [ @conj [ @conj [ @conj [ @conj
    454437  [ (* out_of_program_none *)
    455438    #i #Hi2 >append_length <commutative_plus @conj
     
    457440      cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
    458441      [ >lookup_opt_insert_miss
    459         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2))
     442        [ (* USE[pass]: out_of_program_none → *)
     443          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))
    460444          @le_S_to_le @le_S_to_le @Hi
    461445        | @bitvector_of_nat_abs
     
    467451      | >lookup_opt_insert_miss
    468452        [ <Hi
    469           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (|prefix|))) ?))
     453          (* USE[pass]: out_of_program_none → *)
     454          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?))
    470455          [ >Hi @Hi2
    471456          | @le_S @le_n
     
    483468      | #Hi >lookup_opt_insert_miss
    484469        [ #Hl
    485           elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl))
     470          (* USE[pass]: out_of_program_none ← *)
     471          elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))
    486472          [ #Hi3 @Hi3
    487473          | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi
     
    489475        | @bitvector_of_nat_abs
    490476          [ @Hi2
    491           | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length
     477          | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length
    492478            <plus_n_Sm @le_S_S @le_plus_n_r
    493479          | @Hi
     
    500486    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    501487    [ >lookup_insert_miss
    502       [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi)
     488      [ (* USE[pass]: not_jump_default *)
     489        lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)
    503490        >nth_append_first
    504491        [ #H #H2 @H @H2
     
    506493        ]
    507494      | @bitvector_of_nat_abs
    508         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length <commutative_plus >plus_n_Sm
    509           @le_plus_a @le_S @Hi
    510         | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S
    511           @le_plus_n_r
     495        [ @(transitive_lt ??? Hi) @le_S_to_le]
     496        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
     497          <plus_n_Sm @le_S_S @le_plus_n_r
    512498        | @lt_to_not_eq @le_S @Hi
    513499        ]
    514500      ]
    515501    | >Hi >lookup_insert_miss
    516       [ #_ elim (proj2 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
     502      [ #_ (* USE: everything is short *)
     503        elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
    517504        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl
    518505      | @bitvector_of_nat_abs
    519         [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r
    520         | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
     506        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r
     507        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
    521508          @le_plus_n_r
    522509        | @lt_to_not_eq @le_n
     
    524511      ]
    525512    ]
     513  ]
     514  | (* 0 ↦ 0 *)
     515    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     516    >lookup_insert_miss
     517    [ (* USE[pass]: 0 ↦ 0 *)
     518      @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
     519    | @bitvector_of_nat_abs
     520      [ / by /
     521      | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm
     522        @le_S_S @le_plus_n_r
     523      | @lt_to_not_eq / by /
     524      ]
     525    ]
     526  ]
     527  | (* fst p = pc *)
     528    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     529    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    526530  ]
    527531  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
     
    530534    [ >lookup_opt_insert_miss
    531535      [ >lookup_opt_insert_miss
    532         [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi)
     536        [ (* USE[pass]: policy_compact_unsafe *)
     537          lapply (proj2 ?? (proj1 ?? Hp) i Hi)
    533538          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
    534539          cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
     
    548553      [2: lapply (le_S_to_le … Hi) -Hi #Hi]
    549554      @bitvector_of_nat_abs
    550       [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus
     555      [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus
    551556        @le_plus_a @Hi
    552       |2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
     557      |2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
    553558        @le_S_S @le_plus_n_r
    554559      |3,6: @lt_to_not_eq @le_S_S @Hi
     
    556561    | >lookup_opt_insert_miss
    557562      [ >Hi >lookup_opt_insert_hit normalize nodelta
    558         >(proj2 ?? Hp) normalize nodelta >nth_append_second
    559         [ <minus_n_n whd in match (nth ????); @refl
     563        (* USE: everything is short, fst p = pc *)
     564        elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl
     565        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl
     566        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second
     567        [ <minus_n_n whd in match (nth ????); >EQ @refl
    560568        | @le_n
    561569        ]
    562570      | @bitvector_of_nat_abs
    563         [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus
     571        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus
    564572          @le_plus_a @le_n
    565         | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
     573        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
    566574          @le_S_S @le_plus_n_r
    567575        | @lt_to_not_eq @le_S_S >Hi @le_n
     
    570578    ]
    571579  ]
    572   | (* 0 ↦ 0 *)
    573     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    574     >lookup_insert_miss
    575     [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
    576     | @bitvector_of_nat_abs
    577       [ / by /
    578       | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    579         @le_S_S @le_plus_n_r
    580       | @lt_to_not_eq / by /
    581       ]
    582     ]
    583   ]
    584   | (* fst p = pc *)
    585     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    586     >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    587   ]
    588   | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
     580  | (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi;
    589581    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    590582    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    591583    [ >lookup_opt_insert_miss
    592       [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi))
     584      [ (* USE[pass]: everything is short *)
     585        @((proj2 ?? Hp) i (le_S_S_to_le … Hi))
    593586      | @bitvector_of_nat_abs
    594         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus
    595           @le_plus_a @le_S_S_to_le @Hi
    596         | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    597           @le_S_S @le_plus_n_r
     587        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     588          >commutative_plus @le_plus_a @le_S_S_to_le @Hi
     589        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm
     590          @le_S_S @le_S_S @le_plus_n_r
    598591        | @lt_to_not_eq @Hi
    599592        ]
     
    603596    ]
    604597  ]
    605   | (* lookup at the end *) cases p -p #p cases p -p #pc #sigma #Hp cases x
    606     #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit
    607     / by refl/
    608   ]
    609 | @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     598| @conj [ @conj [ @conj [ @conj [ @conj
    610599  [ #i cases i
    611600    [ #Hi2 @conj
     
    629618    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    630619    ]
    631   ]
     620  ] ] ]
     621  >lookup_insert_hit @refl
    632622  | #i cases i
    633623    [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n
    634624    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    635625    ]
    636   ]
    637   | >lookup_insert_hit @refl
    638   ]
    639   | >lookup_insert_hit @refl
    640626  ]
    641627  | #i cases i
     
    643629    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    644630    ]
    645   ]
    646   | >lookup_opt_insert_hit @refl
    647631  ]
    648632]
     
    676660include alias "basics/logic.ma".
    677661
    678 lemma blerpque: ∀a,b,i.
     662lemma jump_length_equal_max: ∀a,b,i.
    679663  is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
    680664  (max_length a b) = a.
     
    699683qed.
    700684
    701 lemma etblorp: ∀a,b,i.is_jump i →
     685lemma jump_length_le_max: ∀a,b,i.is_jump i →
    702686  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
    703687 #a #b #i cases i
     
    706690 |1: #pi cases pi
    707691   [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:
    708      [1,2,3,6,7,24,25: #x #y
    709      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    710      #H cases H
     692     try (#x #y #H) try (#x #H) try (#H) cases H
    711693   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    712694     #_ cases a cases b
    713      [2,3: cases x #ad cases ad
    714        [15,34: #b #Hb / by le_n/
    715        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
    716      |1,4,5,6,7,8,9: / by le_n/
    717      |11,12: cases x #ad cases ad
    718        [15,34: #b #Hb / by le_n/
    719        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
     695     [1,4,5,6,7,8,9: / by le_n/
    720696     |10,13,14,15,16,17,18: / by le_n/
    721      |20,21: cases x #ad cases ad
    722        [15,34: #b #Hb / by le_n/
    723        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
    724697     |19,22,23,24,25,26,27: / by le_n/
    725      |29,30: cases x #ad cases ad #a1 #a2
    726        [1,3: cases a2 #ad2 cases ad2
    727          [1,8,20,27: #b #Hb / by le_n/
    728          |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb
    729        |2,4: cases a1 #ad1 cases ad1
    730          [2,4,21,23: #b #Hb / by le_n/
    731          |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    732        ]
    733698     |28,31,32,33,34,35,36: / by le_n/
    734      |38,39: cases x #ad cases ad
    735        [1,4,20,23: #b #Hb / by le_n/
    736        |2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    737699     |37,40,41,42,43,44,45: / by le_n/
    738700     |46,47,48,49,50,51,52,53,54: / by le_n/
     
    741703     |73,74,75,76,77,78,79,80,81: / by le_n/
    742704     ]
     705     try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n)
     706     cases x * #ad   
     707     try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n)
     708     #z @(subaddressing_mode_elim … z) #w normalize / by /
    743709   ]
    744710 ]
    745711qed.
    746712
    747 lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
    748  #n
    749  elim n
    750  [ #m #_ @le_O_n
    751  | #n' #Hind #m cases m
    752    [ #H -n whd in match (minus ??) in H; >H @le_n
    753    | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
    754    ]
    755  ]
    756 qed.
    757 
    758 lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
    759  #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
    760 qed.
    761 
    762 lemma not_true_is_false:
    763   ∀b:bool.b ≠ true → b = false.
    764  #b cases b
    765  [ #H @⊥ @(absurd ?? H) @refl
    766  | #H @refl
    767  ]
    768 qed.
    769 
    770 lemma occurs_does_not: ∀tag,A,id,list_instr.
    771   does_not_occur tag A id list_instr = true →
    772   occurs_exactly_once tag A id list_instr = true →
    773   False.
    774  #tag #A #id #list_instr elim list_instr
    775  [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS)
    776  | #h #t #Hind whd in match (does_not_occur ????);
    777    whd in match (occurs_exactly_once ????);
    778    cases (instruction_matches_identifier ?? id h) normalize nodelta
    779    [ #ABS destruct (ABS)
    780    | @Hind
    781    ]
    782  ]
    783 qed.
    784  
    785 lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16).∀labels:(Σlm.
     713lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm.
    786714   ∀l.occurs_exactly_once ?? l program →
    787715    bitvector_of_nat ? (lookup_def ?? lm l 0) =
     
    789717 occurs_exactly_once ?? x program →   
    790718 lookup_def ASMTag ℕ labels x O≤|program|.
    791  #program cases program -program #program #Hprogram #labels #x cases labels
    792  -labels #labels #H lapply (H x) -H
    793  generalize in match (lookup_def … labels x 0);
    794  whd in match address_of_word_labels_code_mem;
    795  whd in match index_of; normalize nodelta elim program in Hprogram;
    796  [ #Hprogram #n cases not_implemented
    797  | #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv
    798    whd in match (occurs_exactly_once ????) in Hocc;
    799    whd in match (index_of_internal ????) in Hbv;
    800    lapply (refl ? (instruction_matches_identifier … x h))
    801    lapply Hocc; lapply Hbv; -Hocc -Hbv
    802    cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);
    803    normalize nodelta #Hbv #Hocc #EQ
    804    [ >(bitvector_of_nat_ok 16 n 0)
    805      [ @le_O_n
    806      | >(eq_eq_bv … Hbv) @I
    807      | / by /
    808      | cases daemon
    809      ]
    810    | cases n in Hbv;
    811      [ #_ @le_O_n
    812      | -n #n #Hbv @le_S_S @(Hind … Hocc)
    813        [ @(transitive_lt … Hprogram) @le_n
    814        | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)
    815          [ >Hbv >eq_bv_refl @I
    816          | @(transitive_lt … Hprogram) cases daemon
    817          | cases daemon
    818          | #H >(index_of_label_from_internal … Hocc)
    819            <plus_O_n >(index_of_label_from_internal … Hocc) in H;
    820            #H >(injective_S … H) <plus_O_n @refl
    821          ]
    822        ]
    823      ]
    824    ]
    825  ]
    826 qed.
     719#program cases program -program #program #Hprogram #labels #x cases labels
     720-labels #labels #H lapply (H x) -H
     721generalize in match (lookup_def … labels x 0);
     722whd in match address_of_word_labels_code_mem;
     723whd in match index_of; normalize nodelta elim program in Hprogram;
     724[ #Hprogram #n cases not_implemented
     725| #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv
     726  whd in match (occurs_exactly_once ????) in Hocc;
     727  whd in match (index_of_internal ????) in Hbv;
     728  lapply (refl ? (instruction_matches_identifier … x h))
     729  lapply Hocc; lapply Hbv; -Hocc -Hbv
     730  cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);
     731  normalize nodelta #Hbv #Hocc #EQ
     732  [ >(bitvector_of_nat_ok 16 n 0)
     733    [ @le_O_n
     734    | >(eq_eq_bv … Hbv) @I
     735    | / by /
     736    | cases daemon
     737    ]
     738  | cases n in Hbv;
     739    [ #_ @le_O_n
     740    | -n #n #Hbv @le_S_S @(Hind … Hocc)
     741      [ @conj
     742        [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n
     743        | cases daemon (* axiomatize this *)
     744        ]
     745      | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)
     746        [ >Hbv >eq_bv_refl @I
     747        | @(transitive_lt … (proj1 ?? Hprogram)) cases daemon
     748        | cases daemon
     749        | #H >(index_of_label_from_internal … Hocc)
     750          <plus_O_n >(index_of_label_from_internal … Hocc) in H;
     751          #H >(injective_S … H) <plus_O_n @refl
     752        ]
     753      ]
     754    ]
     755  ]
     756]
     757qed.
     758
     759lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l).
     760  ∀labels.∀old_sigma.∀sigma.
     761  sigma_pc_equal program old_sigma sigma →
     762  sigma_safe program labels 0 old_sigma sigma →
     763  sigma_compact_unsafe program labels sigma →
     764  sigma_compact program labels sigma.
     765  #program #labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi
     766  lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
     767  lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)))
     768  cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %);
     769  [ / by /
     770  | #x cases x -x #x1 #x2 #EQ
     771    cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma))
     772    [ / by /
     773    | #y cases y -y #y1 #y2 normalize nodelta #H #H2
     774      cut (instruction_size_jmplen x2
     775       (\snd (nth i ? program 〈None ?, Comment []〉)) =
     776       instruction_size … (bitvector_of_nat ? i)
     777       (\snd (nth i ? program 〈None ?, Comment []〉)))
     778      [5: #H3 <H3 @H2
     779      |4: whd in match (instruction_size_jmplen ??);
     780          whd in match (instruction_size …);
     781          whd in match (assembly_1_pseudoinstruction …);
     782          whd in match (expand_pseudo_instruction …);
     783          normalize nodelta whd in match (append …) in H;
     784          cases (nth i ? program 〈None ?,Comment []〉) in H;
     785          #lbl #instr cases instr
     786          [2,3,6: #x [3: #y] normalize nodelta #H @refl
     787          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
     788            lapply (Hj x (refl ? x)) -Hj normalize nodelta
     789            >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
     790            cases x2 normalize nodelta
     791            [1,4: whd in match short_jump_cond; normalize nodelta
     792              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
     793              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
     794              normalize nodelta
     795              >(Hequal (lookup_def ?? labels x 0) ?)
     796              [2,4,6,8: @(label_in_program program labels x)
     797                cases daemon (* XXX this has to come from somewhere else *)
     798              ]
     799              <plus_n_O
     800              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     801              #result #flags normalize nodelta
     802              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     803              cases (get_index' bool 2 0 flags) normalize nodelta
     804              [5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
     805              |1,2,3,4: cases (eq_bv 9 upper ?)
     806                [2,4,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3)
     807                |1,3,5,7: #_ normalize nodelta @refl
     808                ]
     809              ]
     810            |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
     811              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
     812              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
     813              normalize nodelta
     814              (* USE: added = 0 → policy_pc_equal (from fold) *)
     815              >(Hequal (lookup_def ?? labels x 0) ?)
     816              [2,4,6,8: @(label_in_program program labels x)
     817                cases daemon (* XXX this has to come from somewhere else *)]
     818              <plus_n_O
     819              normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
     820              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     821              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     822              #result #flags normalize nodelta
     823              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     824              cases (get_index' bool 2 0 flags) normalize nodelta
     825              #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
     826            |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
     827              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
     828              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
     829              normalize nodelta
     830              (* USE: added = 0 → policy_pc_equal (from fold) *)
     831              >(Hequal (lookup_def ?? labels x 0) ?)
     832              [2,4,6,8: @(label_in_program program labels x)
     833                cases daemon (* XXX this has to come from somewhere else *)]
     834              <plus_n_O normalize nodelta
     835              cases (vsplit bool 5 11 ?) #addr1 #addr2
     836              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     837              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     838              #result #flags normalize nodelta
     839              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     840              cases (get_index' bool 2 0 flags) normalize nodelta
     841              #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
     842            ]
     843          |1: #pi cases pi
     844            [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:
     845              [1,2,3,6,7,24,25: #x #y
     846              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     847              normalize nodelta #H @refl
     848            |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
     849              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     850              #Hj lapply (Hj x (refl ? x)) -Hj
     851              whd in match expand_relative_jump; normalize nodelta
     852              whd in match expand_relative_jump_internal; normalize nodelta
     853              whd in match expand_relative_jump_unsafe; normalize nodelta
     854              whd in match expand_relative_jump_internal_unsafe;
     855              normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
     856              <(plus_n_Sm i 0) <plus_n_O
     857              cases daemon (* XXX this needs subadressing mode magic, see above *)
     858            ]
     859          ]
     860        ]
     861      ]
     862    ]
     863qed.
Note: See TracChangeset for help on using the changeset viewer.