Changeset 989


Ignore:
Timestamp:
Jun 17, 2011, 10:28:19 AM (8 years ago)
Author:
sacerdot
Message:

Type of build_maps strengthened.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r987 r989  
    657657    jump_expansion_internal n' program new_labels new_policy ].
    658658
     659(**************************************** START OF POLICY ABSTRACTION ********************)
     660
    659661definition policy_type ≝ Word → jump_length.
    660662
     
    798800    → False.
    799801
    800 definition build_maps ≝
     802definition build_maps:
     803 ∀pseudo_program.∀pol:policy pseudo_program.
     804  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
     805   let 〈labels,costs〉 ≝ res in
     806    ∀id. occurs_exactly_once id (\snd pseudo_program) →
     807     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
     808 ≝
    801809  λpseudo_program.λpol:policy pseudo_program.
    802810  let result ≝
     
    838846   let 〈pc, costs〉 ≝ pc_costs in
    839847    〈labels, costs〉.
    840  [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
    841  | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     848 [4: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
     849 |2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    842850   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
    843851   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
     
    852860        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
    853861          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
    854  | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
    855    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
     862 |3: (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
     863   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4))
     864 | generalize in match (sig2 … result) >p normalize nodelta; >p1 normalize nodelta;
     865   >p2; normalize nodelta; * #_; #H @H]
    856866qed.
    857 
    858 (*
    859 lemma build_maps_ok:
    860  ∀p:pseudo_assembly_program.
    861   let 〈labels,costs〉 ≝ build_maps' p in
    862    ∀pc.
    863     (nat_of_bitvector … pc) < length … (\snd p) →
    864      lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
    865  #p cases p #preamble #instr_list
    866   elim instr_list
    867    [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
    868    | #hd #tl #IH
    869     whd in ⊢ (match % with [ _ ⇒ ?])
    870    ]
    871 qed.
    872 *)
    873867
    874868definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
  • src/ASM/AssemblyProof.ma

    r988 r989  
    16701670qed.
    16711671
     1672axiom get_arg_8_set_low_internal_ram:
     1673 ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.
     1674
    16721675lemma eq_rect_Type1_r:
    16731676  ∀A: Type[1].
     
    18721875       #result #flags
    18731876       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)
    1874   |5: (* Call *) #label #MAP
     1877(*  |5: (* Call *) #label #MAP
    18751878      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
    18761879      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
     
    20602063            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    20612064              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    2062   | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
     2065*)  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    20632066    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
    20642067       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    20652068       change in ⊢ (? → ??%?) with (execute_1_0 ??)
    2066        cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2069       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    20672070       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    20682071       >H2b >(eq_instruction_to_eq … H2a)
     
    20702073       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
    20712074       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
    2072        normalize nodelta; #MAP;
     2075       normalize nodelta; #MAP; (*
    20732076       [1: change in ⊢ (? → %) with
    20742077        ((let 〈result,flags〉 ≝
     
    20782081             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
    20792082             false (DIRECT ARG2))
    2080            ? in ?) = ?) //
    2081        [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
    2082         [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
    2083        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
     2083           ? in ?) = ?)
     2084        [2,3: %]
     2085        change in ⊢ (???% → ?) with
     2086         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
     2087        >get_arg_8_set_clock *)
     2088       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
     2089         [2,4: #abs @⊥ normalize in abs; destruct (abs)
     2090         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
     2091       [ change in ⊢ (? → %) with
     2092        ((let 〈result,flags〉 ≝
     2093          add_8_with_carry
     2094           (get_arg_8 ? ps false ACC_A)
     2095           (get_arg_8 ?
     2096             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
     2097             false (DIRECT ARG2))
     2098           ? in ?) = ?)
     2099          >get_arg_8_set_low_internal_ram
     2100       
     2101        cases (add_8_with_carry ???)
     2102         
     2103        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    20842104       #result #flags
    20852105       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
Note: See TracChangeset for help on using the changeset viewer.