Changeset 2020


Ignore:
Timestamp:
Jun 6, 2012, 6:27:56 PM (5 years ago)
Author:
mulligan
Message:

CJNE case complete, DJNZ case almost complete

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2018 r2020  
    860860  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    861861  whd in match execute_1_preinstruction; normalize nodelta
    862   [30: (* CJNE *)
     862  [31: (* DJNZ *)
     863  (* XXX: work on the right hand side *)
     864  >p normalize nodelta
     865  (* XXX: switch to the left hand side *)
     866  -instr_refl >EQP -P normalize nodelta
     867  #sigma_increment_commutation #maps_assm #fetch_many_assm
     868  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     869  whd in match (expand_relative_jump ????);
     870  <EQppc in fetch_many_assm;
     871  @pair_elim #result #flags #sub16_refl
     872  @pair_elim #upper #lower #split_refl
     873  cases (eq_bv ???) normalize nodelta
     874  [1:
     875    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     876    whd in ⊢ (??%?);
     877    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     878    (* XXX: work on the left hand side *)
     879    check pair_replace
     880    @(pair_replace ?????????? p) normalize nodelta
     881    [1:
     882      cases daemon
     883    ]
     884    (* XXX: switch to the right hand side *)
     885    normalize nodelta >EQs -s >EQticks -ticks
     886    cases (¬ eq_bv ???) normalize nodelta
     887    whd in ⊢ (??%%);
     888    (* XXX: finally, prove the equality using sigma commutation *)
     889    @split_eq_status try %
     890    cases daemon
     891  |2:
     892    >EQppc
     893    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     894    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     895    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     896    #fetch_many_assm whd in fetch_many_assm; %{2}
     897    change with (execute_1 ?? = ?)
     898    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     899    #status_after_1 #EQstatus_after_1
     900    <(?: ? = status_after_1)
     901    [3:
     902      >EQstatus_after_1 in ⊢ (???%);
     903      whd in ⊢ (???%);
     904      <fetch_refl in ⊢ (???%);
     905      whd in ⊢ (???%);
     906      @(pair_replace ?????????? p)
     907      [1:
     908        cases daemon
     909      |2:
     910        normalize nodelta
     911        whd in match (addr_of_relative ????);
     912        cases (¬ eq_bv ???) normalize nodelta
     913        >set_clock_mk_Status_commutation
     914        whd in ⊢ (???%);
     915        change with (add ???) in match (\snd (half_add ???));
     916        >set_arg_8_set_program_counter in ⊢ (???%);
     917        [2,4: cases daemon ]
     918        >program_counter_set_program_counter in ⊢ (???%);
     919        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     920        [2,4:
     921          >bitvector_of_nat_sign_extension_equivalence
     922          [1,3:
     923            >EQintermediate_pc' %
     924          |*:
     925            repeat @le_S_S @le_O_n
     926          ]
     927        ]
     928        [1: % ]
     929      ]
     930    |1:
     931      skip
     932    ]
     933    [2:
     934      -status_after_1
     935      @(pose … (execute_1 ? (mk_PreStatus …)))
     936      #status_after_1 #EQstatus_after_1
     937      <(?: ? = status_after_1)
     938      [3:
     939        >EQstatus_after_1 in ⊢ (???%);
     940        whd in ⊢ (???%);
     941        (* XXX: matita bug with patterns across multiple goals *)
     942        <fetch_refl'' in ⊢ (???%);
     943        whd in ⊢ (???%); %
     944    |1:
     945      skip
     946    ]
     947    -status_after_1 whd in ⊢ (??%?);
     948    (* XXX: switch to the right hand side *)
     949    normalize nodelta >EQs -s >EQticks -ticks
     950    cases (¬ eq_bv ???) normalize nodelta
     951    whd in ⊢ (??%%);
     952  ]
     953  (* XXX: finally, prove the equality using sigma commutation *)
     954  @split_eq_status XXX try %
     955  cases daemon
     956  |30: (* CJNE *)
    863957  (* XXX: work on the right hand side *)
    864958  cases addr1 -addr1 #addr1 normalize nodelta
     
    9091003    #status_after_1 #EQstatus_after_1
    9101004    <(?: ? = status_after_1)
    911     [3,6:
     1005    [2,5:
     1006      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
     1007    |3,6:
    9121008      >EQstatus_after_1 in ⊢ (???%);
    9131009      whd in ⊢ (???%);
     
    9301026          repeat @le_S_S @le_O_n
    9311027        ]
     1028      |1,5:
     1029        %
    9321030      ]
    933       [1,3: % ]
     1031    |1,4: skip
     1032    ]
     1033    [1,2,3,4:
     1034      -status_after_1
     1035      @(pose … (execute_1 ? (mk_PreStatus …)))
     1036      #status_after_1 #EQstatus_after_1
     1037      <(?: ? = status_after_1)
     1038      [3,6,9,12:
     1039        >EQstatus_after_1 in ⊢ (???%);
     1040        whd in ⊢ (???%);
     1041        (* XXX: matita bug with patterns across multiple goals *)
     1042        [1: <fetch_refl'' in ⊢ (???%);
     1043        |2: <fetch_refl'' in ⊢ (???%);
     1044        |3: <fetch_refl'' in ⊢ (???%);
     1045        |4: <fetch_refl'' in ⊢ (???%);
     1046        ] %
     1047      |1,4,7,10:
     1048        skip
     1049      ]
     1050      -status_after_1 whd in ⊢ (??%?);
     1051      (* XXX: switch to the right hand side *)
     1052      normalize nodelta >EQs -s >EQticks -ticks
     1053      whd in ⊢ (??%%);
     1054    ]
     1055    (* XXX: finally, prove the equality using sigma commutation *)
     1056    @split_eq_status try %
     1057    [3:
     1058      whd in ⊢ (??%?);
     1059      cases daemon
     1060    |*:
     1061      cases daemon
    9341062    ]
    9351063  ]
Note: See TracChangeset for help on using the changeset viewer.