Changeset 2221 for src/ASM


Ignore:
Timestamp:
Jul 20, 2012, 10:46:29 AM (7 years ago)
Author:
boender
Message:
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2199 r2221  
    624624    let 〈labels,costs〉 ≝ labels_costs in
    625625    ∀l.occurs_exactly_once ?? l program →
    626     bitvector_of_nat ? (lookup_def ?? labels l 0) =
    627      address_of_word_labels_code_mem program l
     626    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
     627     address_of_word_labels_code_mem program l)
     628     (lookup_def ?? labels l 0 < |program|)
    628629  ) ≝
    629630  λprogram.
     
    633634    ppc = |prefix| ∧
    634635    ∀l.occurs_exactly_once ?? l prefix →
    635     bitvector_of_nat ? (lookup_def ?? labels l 0) =
     636    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
    636637     address_of_word_labels_code_mem prefix l)
     638     (lookup_def ?? labels l 0 < |program|))
    637639  program
    638640  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
     
    656658   >occurs_exactly_once_None in Hocc; @(IH2 lbl)
    657659 | #lbl normalize nodelta inversion (eq_identifier ? lbl l)
    658    [ #Heq #Hocc >(eq_identifier_eq … Heq)
    659      >address_of_word_labels_code_mem_Some_hit
    660      [ >IH1 >lookup_def_add_hit %
    661      | <(eq_identifier_eq … Heq) in Hocc; //
     660   [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj
     661     [ >address_of_word_labels_code_mem_Some_hit
     662       [ >IH1 >lookup_def_add_hit %
     663       | <(eq_identifier_eq … Heq) in Hocc; //
     664       ]
     665     | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    662666     ]
    663    | #Hneq #Hocc
    664      <address_of_word_labels_code_mem_Some_miss
    665      [ >lookup_def_add_miss
    666        [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq //
    667        | % @neq_identifier_neq @Hneq
     667   | #Hneq #Hocc lapply (IH2 lbl ?)
     668     [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq //
     669     | #IH3 @conj
     670       [ <address_of_word_labels_code_mem_Some_miss
     671         [ >lookup_def_add_miss
     672           [ @(proj1 ?? IH3)
     673           | % @neq_identifier_neq @Hneq
     674           ] 
     675         | @Hocc
     676         | >eq_identifier_sym @Hneq
     677         ]
     678       | >lookup_def_add_miss
     679         [ @(proj2 ?? IH3)
     680         | % @neq_identifier_neq @Hneq
     681         ]
    668682       ]
    669      | @Hocc
    670      | >eq_identifier_sym @Hneq
    671683     ]
    672684   ]
     
    688700 ∀pseudo_program: pseudo_assembly_program.
    689701   let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
    690     ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
    691      bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
     702    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) → And
     703     (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id)
     704     (lookup_def ?? labels id 0 < |\snd pseudo_program|).
    692705 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
    693706qed.
  • src/ASM/PolicyFront.ma

    r2213 r2221  
    302302  (Σlabels:label_map.
    303303    ∀l.occurs_exactly_once ?? l program →
    304     bitvector_of_nat ? (lookup_def ?? labels l 0) =
    305      address_of_word_labels_code_mem program l
     304    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
     305     address_of_word_labels_code_mem program l)
     306    (lookup_def ?? labels l 0 < |program|)
    306307  ) ≝
    307308 λprogram.
     
    650651  sigma_compact_unsafe program (create_label_map program) sigma →
    651652  sigma_compact program (create_label_map program) sigma.
    652   #program #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi
     653  #program cases program -program #program #Hprogram #old_sigma #sigma #Hequal
     654  #Hsafe #Hcp_unsafe #i #Hi
    653655  lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
    654656  lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)))
     
    669671          whd in match (expand_pseudo_instruction …);
    670672          normalize nodelta whd in match (append …) in H;
    671           cases (nth i ? program 〈None ?,Comment []〉) in H;
     673          lapply (refl ? (nth i ? program 〈None ?, Comment []〉)) lapply H
     674          cases (nth i ? program 〈None ?,Comment []〉) in ⊢ (% → ???% → %);
    672675          #lbl #instr cases instr
    673           [2,3,6: #x [3: #y] normalize nodelta #H @refl
    674           |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
     676          [2,3,6: #x [3: #y] normalize nodelta #H #_ %
     677          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj #Heq
    675678            lapply (Hj x (refl ? x)) -Hj normalize nodelta
    676679            >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
     
    678681            [1,4: whd in match short_jump_cond; normalize nodelta
    679682              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    680               [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
     683              [1,3: cases (create_label_map program) #clm #Hclm
     684                @le_S_to_le @(proj2 ?? (Hclm x ?))
     685                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
     686                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
     687                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
     688                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     689                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
     690                  >nth_safe_nth
     691                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
     692                    [1,3: >Heq / by refl/
     693                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
     694                    ]
     695                  ]
     696                |3,6: / by /
     697                ]
    681698              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    682699              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     
    693710            |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
    694711              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    695               [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
     712              [1,3: cases (create_label_map program) #clm #Hclm
     713                @le_S_to_le @(proj2 ?? (Hclm x ?))
     714                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
     715                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
     716                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
     717                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     718                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
     719                  >nth_safe_nth
     720                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
     721                    [1,3: >Heq / by refl/
     722                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
     723                    ]
     724                  ]
     725                |3,6: / by /
     726                ]
    696727              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    697728              normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
     
    705736            |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    706737              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    707               [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
     738              [1,3: cases (create_label_map program) #clm #Hclm
     739                @le_S_to_le @(proj2 ?? (Hclm x ?))
     740                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
     741                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
     742                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
     743                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     744                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
     745                  >nth_safe_nth
     746                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
     747                    [1,3: >Heq / by refl/
     748                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
     749                    ]
     750                  ]
     751                |3,6: / by /
     752                ]
    708753              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    709754              cases (vsplit bool 5 11 ?) #addr1 #addr2
     
    720765              [1,2,3,6,7,24,25: #x #y
    721766              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    722               normalize nodelta #H @refl
     767              normalize nodelta #H #Heq @refl
    723768            |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
    724769              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    725               #Hj lapply (Hj x (refl ? x)) -Hj
     770              #Hj #Heq lapply (Hj x (refl ? x)) -Hj
    726771              whd in match expand_relative_jump; normalize nodelta
    727772              whd in match expand_relative_jump_internal; normalize nodelta
     
    737782                [1,3,5,7,9,11,13,15,17:
    738783                  cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    739                   [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *)
     784                  [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
     785                    @le_S_to_le @(proj2 ?? (Hclm x ?))
     786                    @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
     787                    [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
     788                      [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     789                    |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
     790                      >nth_safe_nth
     791                      [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
     792                        [1,3,5,7,9,11,13,15,17: >Heq %]
     793                        @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
     794                      ]
     795                    ]
     796                    >Heq / by /
     797                  ]
    740798                  #X >(le_to_leb_true … X) @refl
    741799                ]
     
    753811                [1,3,5,7,9,11,13,15,17:
    754812                  cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    755                   [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *)
     813                  [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
     814                    @le_S_to_le @(proj2 ?? (Hclm x ?))
     815                    @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
     816                    [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
     817                      [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     818                    |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
     819                      >nth_safe_nth
     820                      [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
     821                        [1,3,5,7,9,11,13,15,17: >Heq %]
     822                        @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
     823                      ]
     824                    ]
     825                    >Heq / by /
     826                  ]
    756827                  #X >(le_to_leb_true … X) @refl
    757828                ]
Note: See TracChangeset for help on using the changeset viewer.