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

Type of build_maps strengthened.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.