Changeset 1404 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Oct 18, 2011, 3:39:56 PM (8 years ago)
Author:
boender
Message:
  • reworked + added
  • added an axiom to arithmetic, but should be provable
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1393 r1404  
    797797  | _ ⇒ False
    798798  ].
    799  
    800 axiom bitvector_of_nat_ok:
    801   ∀x,y,n.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y.
    802  
     799
     800definition jump_in_policy ≝
     801  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
     802  ∀i:ℕ.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
     803  ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉.
     804   
    803805let rec jump_expansion_step (program: list labelled_instruction)
    804   (old_policy: jump_expansion_policy):
    805   (Σpolicy.∀i:ℕ.i < |program| →
    806     is_jump (nth i ? program 〈None ?, Comment [ ]〉) →
    807     ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉
    808   ) ≝
     806  (old_policy: Σpolicy.jump_in_policy program policy):
     807  (Σpolicy.
     808    jump_in_policy program policy ∧
     809    (jump_in_policy program policy → True)) ≝
    809810  let labels ≝ create_label_trie program old_policy in
    810811  let 〈final_pc, final_policy〉 ≝
    811812    foldl_strong (option Identifier × pseudo_instruction)
    812     (λprefix.ℕ × Σpolicy.∀i:ℕ.i < |prefix| →
    813       is_jump (nth i ? prefix 〈None ?, Comment [ ]〉) →
    814       ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉
     813    (λprefix.ℕ × Σpolicy.
     814      jump_in_policy prefix policy ∧
     815      (jump_in_policy prefix policy → True)
    815816    )
    816817    program
     
    838839    ) 〈0, Stub ? ?〉 in
    839840    final_policy.
    840 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    841   [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
    842     lapply (sig2 … policy) #Hacc elim (Hacc i (le_S_S_to_le … Hi) Hj) #henk #ingrid elim ingrid
    843     -ingrid #ingrid #Hingrid
    844     % [ @henk | % [ @ingrid | normalize nodelta cases instr normalize nodelta
    845     [2,3: #x cases (lookup ??? policy ?) #y #z @Hingrid
    846     |6: #x #y cases (lookup ??? policy ?) #w #z @Hingrid
    847     |1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???)
    848       [ @Hingrid
    849       | #z normalize nodelta <Hingrid @lookup_opt_insert_miss
    850         @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
    851         [ @(bitvector_of_nat_ok … H)
    852         | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    853         ] ]
     841[ @conj
     842  [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     843    [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
     844      lapply (sig2 … policy) #Hacc elim ((proj1 … Hacc) i (le_S_S_to_le … Hi) Hj) #h #n elim n
     845      -n #n #Hn
     846      % [ @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 ???)
     850        [ @Hn
     851        | #z normalize nodelta <Hn @lookup_opt_insert_miss
     852          @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
     853          [ @(bitvector_of_nat_ok … H)
     854          | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     855          ] ]
     856        ]
     857      |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hn
     858        @lookup_opt_insert_miss @notb_elim >eq_bv_false
     859        [1,3: //
     860        |2,4: @nmk #H @(absurd (i = (|prefix|)))
     861          [1,3: @(bitvector_of_nat_ok … H)
     862          |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     863          ] ]
     864      ] ] ]
     865    | #Hi >nth_append_second >(injective_S … Hi)
     866      [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
     867        [2,3: #x #Hj @⊥ @Hj
     868        |6: #x #y #Hj @⊥ @Hj
     869        |1: #pi cases pi
     870          [35,36,37: #Hj @⊥ @Hj
     871          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
     872          |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
     873          |9,10,14,15: #j normalize nodelta #_
     874            % [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 ⊢ (???% → %)         
     877                #x #y #Hl normalize nodelta
     878            % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     879              |2,4,6,8: @lookup_opt_insert_hit
     880              ] ]
     881          |11,12,13,16,17: #x #j normalize nodelta #_
     882            % [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 ⊢ (???% → %)         
     885                #x #y #Hl normalize nodelta
     886            % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
     887              |2,4,6,8,10: @lookup_opt_insert_hit
     888              ] ]
     889          ]
     890        |4,5: #j normalize nodelta #_
     891          % [1,3: @pc
     892            |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)
     893                #x #y normalize nodelta
     894            % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
     895              |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))
     896              |2,4: @lookup_opt_insert_hit
     897              ]
     898            ]
     899        ]
     900      | @le_n
    854901      ]
    855     |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hingrid
    856       @lookup_opt_insert_miss @notb_elim >eq_bv_false
    857       [1,3: //
    858       |2,4: @nmk #H @(absurd (i = (|prefix|)))
    859         [1,3: @(bitvector_of_nat_ok … H)
    860         |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    861         ] ]
    862     ] ] ]
    863   | #Hi >nth_append_second >(injective_S … Hi)
    864     [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
    865       [2,3: #x #Hj @⊥ @Hj
    866       |6: #x #y #Hj @⊥ @Hj
    867       |1: #pi cases pi
    868         [35,36,37: #Hj @⊥ @Hj
    869         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
    870         |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
    871         |9,10,14,15: #j normalize nodelta #_
    872           % [1,3,5,7: @pc
    873             |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
    874               cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
    875               #x #y #Hl normalize nodelta
    876           % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
    877             |2,4,6,8: @lookup_opt_insert_hit
    878             ] ]
    879         |11,12,13,16,17: #x #j normalize nodelta #_
    880           % [1,3,5,7,9: @pc
    881             |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉))
    882               cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %)         
    883               #x #y #Hl normalize nodelta
    884           % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))
    885             |2,4,6,8,10: @lookup_opt_insert_hit
    886             ] ]
    887         ]
    888       |4,5: #j normalize nodelta #_
    889         % [1,3: @pc
    890           |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)
    891               #x #y normalize nodelta
    892           % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))
    893             |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))
    894             |2,4: @lookup_opt_insert_hit
    895             ]
    896           ]
    897       ]
    898     | @le_n
    899902    ]
     903  | //
    900904  ]
    901 | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
     905| @conj
     906  [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
     907  | //
     908  ]
    902909]
    903910qed.
Note: See TracChangeset for help on using the changeset viewer.