Changeset 1417 for src/ASM


Ignore:
Timestamp:
Oct 19, 2011, 5:10:27 PM (8 years ago)
Author:
boender
Message:
  • proved that jumps always increase - this should make termination easy
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1404 r1417  
    773773  ].
    774774
     775lemma jmpleq_max_length: ∀x,y.jmpleq y (max_length y x).
     776 #x #y
     777 cases y
     778 [ //
     779 | cases x //
     780 | //
     781 ]
     782qed.
     783
    775784definition is_jump' ≝
    776785  λx:preinstruction Identifier.
     
    807816  (Σpolicy.
    808817    jump_in_policy program policy ∧
    809     (jump_in_policy program policy → True)) ≝
     818    (jump_in_policy program policy →
     819     (∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
     820     jmpleq
     821       (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
     822       (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
     823    )
     824   ) ≝
    810825  let labels ≝ create_label_trie program old_policy in
    811826  let 〈final_pc, final_policy〉 ≝
     
    813828    (λprefix.ℕ × Σpolicy.
    814829      jump_in_policy prefix policy ∧
    815       (jump_in_policy prefix policy → True)
     830      (jump_in_policy prefix policy →
     831       (∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
     832       jmpleq
     833         (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
     834         (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
     835      )
    816836    )
    817837    program
     
    819839      let 〈pc, policy〉 ≝ acc in
    820840      let 〈label,instr〉 ≝ x in
    821       let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) policy in
     841      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
    822842      let add_instr ≝
    823843        match instr with
     
    828848        ] in
    829849      let 〈new_pc, new_policy〉 ≝
    830         let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, short_jump〉 in
     850        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, short_jump〉 in
    831851        match add_instr with
    832852        [ None    ⇒ (* i.e. it's not a jump *)
     
    845865      -n #n #Hn
    846866      % [ @h | % [ @n | normalize nodelta cases instr normalize nodelta
    847       [2,3: #x cases (lookup ??? policy ?) #y #z @Hn
    848       |6: #x #y cases (lookup ??? policy ?) #w #z @Hn
    849       |1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???)
     867      [2,3: #x cases (lookup ??? old_policy ?) #y #z @Hn
     868      |6: #x #y cases (lookup ??? old_policy ?) #w #z @Hn
     869      |1: #pi cases (lookup ??? old_policy ?) #x #y cases (jump_expansion_step_instruction ???)
    850870        [ @Hn
    851871        | #z normalize nodelta <Hn @lookup_opt_insert_miss
     
    855875          ] ]
    856876        ]
    857       |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hn
     877      |4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn
    858878        @lookup_opt_insert_miss @notb_elim >eq_bv_false
    859879        [1,3: //
     
    873893          |9,10,14,15: #j normalize nodelta #_
    874894            % [1,3,5,7: @pc
    875               |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
    876                 cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
     895              |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
     896                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)
    877897                #x #y #Hl normalize nodelta
    878898            % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     
    881901          |11,12,13,16,17: #x #j normalize nodelta #_
    882902            % [1,3,5,7,9: @pc
    883               |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
    884                 cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
     903              |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
     904                cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %)         
    885905                #x #y #Hl normalize nodelta
    886906            % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     
    890910        |4,5: #j normalize nodelta #_
    891911          % [1,3: @pc
    892             |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)
     912            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    893913                #x #y normalize nodelta
    894914            % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
     
    901921      ]
    902922    ]
    903   | //
     923  | #Hjip #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     924    [ #Hi >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
     925      lapply (sig2 … policy) #Hpolicy normalize nodelta cases instr normalize nodelta
     926      [2,3: #x cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #y #z
     927        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
     928      |6: #x #y cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #w #z
     929        normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
     930      |1: #pi cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
     931        cases (jump_expansion_step_instruction ???)
     932        [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
     933        | #z normalize nodelta
     934          whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss
     935          [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
     936          | @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
     937            [ @(bitvector_of_nat_ok … H)
     938            | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     939            ] ]
     940          ]
     941        ]
     942      |4,5: #id cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
     943        normalize nodelta >lookup_insert_miss
     944        [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
     945        |2,4: @notb_elim >eq_bv_false [1,3: // | 2,4: @nmk #H @(absurd (i = (|prefix|)))
     946          [1,3: @(bitvector_of_nat_ok … H)
     947          |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     948          ] ]
     949        ]
     950      ]
     951    | #Hi >nth_append_second >(injective_S … Hi)
     952      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
     953        [2,3: #x #Hj @⊥ @Hj
     954        |6: #x #y #Hj @⊥ @Hj
     955        |1: #pi cases pi
     956          [35,36,37: #Hj @⊥ @Hj
     957          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
     958          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
     959          |9,10,14,15: #j normalize nodelta #_
     960            cases (lookup ???? 〈0,short_jump〉) #x #y
     961            whd in match (snd ℕ jump_expansion_policy ?)
     962            >lookup_insert_hit normalize @jmpleq_max_length
     963          |11,12,13,16,17: #z #j normalize nodelta #_
     964            cases (lookup ???? 〈0,short_jump〉) #x #y           
     965            whd in match (snd ℕ jump_expansion_policy ?)
     966            >lookup_insert_hit normalize @jmpleq_max_length
     967          ]
     968        |4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y
     969              whd in match (snd ℕ jump_expansion_policy ?)
     970              >lookup_insert_hit normalize @jmpleq_max_length
     971        ]
     972      | @le_n
     973      ]
     974    ]
    904975  ]
    905976| @conj
    906977  [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    907   | //
     978  | #H #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    908979  ]
    909980]
Note: See TracChangeset for help on using the changeset viewer.