Changeset 1985


Ignore:
Timestamp:
May 22, 2012, 6:12:13 PM (6 years ago)
Author:
mulligan
Message:

A single `false' case for unconditional jumps completed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1984 r1985  
    838838  (* XXX: finally, prove the equality using sigma commutation *)
    839839  cases daemon
    840 |16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases) *)
     840|17,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases) *)
    841841  (* XXX: work on the right hand side *)
    842842  >p normalize nodelta
     
    851851  @pair_elim #upper #lower #split_refl
    852852  cases (eq_bv ???) normalize nodelta
    853   [1,3,5,7,9,11,13:
     853  [1,3,5,7,9,11,13,15:
    854854    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    855855    whd in ⊢ (??%?);
     
    857857    (* XXX: work on the left hand side *)
    858858    @(if_then_else_replace ???????? p) normalize nodelta
    859     [1,3,5,7,9,11,13:
     859    [1,3,5,7,9,11,13,15:
    860860      cases daemon
    861861    ]
     
    866866    @split_eq_status try %
    867867    cases daemon
    868   |2,4,6,8,10,12,14:
     868  |2,4,6,8,10,12,14,16:
    869869    >EQppc
    870870    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     
    876876    #status_after_1 #EQstatus_after_1
    877877    <(?: ? = status_after_1)
    878     [3,6,9,12,15,18,21:
     878    [3,6,9,12,15,18,21,24:
    879879      >EQstatus_after_1 in ⊢ (???%);
    880880      whd in ⊢ (???%);
     
    886886      |6: <fetch_refl in ⊢ (???%);
    887887      |7: <fetch_refl in ⊢ (???%);
     888      |8: <fetch_refl in ⊢ (???%);
    888889      ]
    889890      whd in ⊢ (???%);
    890891      @(if_then_else_replace ???????? p)
    891       [1,3,5,7,9,11,13:
     892      [1,3,5,7,9,11,13,15:
    892893        cases daemon
    893       |2,4,6,8,10,12,14:
     894      |2,4,6,8,10,12,14,16:
    894895        normalize nodelta
    895896        whd in match (addr_of_relative ????);
    896897        >set_clock_mk_Status_commutation
    897         [5:
     898        [6:
    898899          (* XXX: demodulation not working in this case *)
    899900          >program_counter_set_arg_1 in ⊢ (???%);
     
    905906        change with (add ???) in match (\snd (half_add ???));
    906907        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    907         [2,4,6,8,10,12,14:
     908        [2,4,6,8,10,12,14,16:
    908909          >bitvector_of_nat_sign_extension_equivalence
    909           [1,3,5,7,9,11,13:
     910          [1,3,5,7,9,11,13,15:
    910911            >EQintermediate_pc' %
    911912          |*:
     
    915916        %
    916917      ]
    917     |1,4,7,10,13,16,19:
     918    |1,4,7,10,13,16,19,22:
    918919      skip
    919920    ]
     
    922923    #status_after_1 #EQstatus_after_1
    923924    <(?: ? = status_after_1)
    924     [3,6,9,12,15,18,21:
     925    [3,6,9,12,15,18,21,24:
    925926      >EQstatus_after_1 in ⊢ (???%);
    926927      whd in ⊢ (???%);
    927928      (* XXX: matita bug with patterns across multiple goals *)
    928929      [1: <fetch_refl'' in ⊢ (???%);
    929       |2: <fetch_refl'' in ⊢ (???%);
     930      |2: <fetch_refl' in ⊢ (???%);
    930931      |3: <fetch_refl'' in ⊢ (???%);
    931932      |4: <fetch_refl'' in ⊢ (???%);
     
    933934      |6: <fetch_refl'' in ⊢ (???%);
    934935      |7: <fetch_refl'' in ⊢ (???%);
     936      |8: <fetch_refl'' in ⊢ (???%);
    935937      ]
    936938      whd in ⊢ (???%);
    937       [5:
     939      [6:
    938940      |*:
    939941        /demod/
    940942      ] %
    941     |1,4,7,10,13,16,19:
     943    |1,4,7,10,13,16,19,22:
    942944      skip
    943945    ]
     
    948950    (* XXX: finally, prove the equality using sigma commutation *)
    949951    @split_eq_status try %
    950     [3,7,11,15,20,28,32:
     952    [3,11,15,19,24,32,36:
    951953      >program_counter_set_program_counter >set_clock_mk_Status_commutation
    952954      [5: >program_counter_set_program_counter ]
     
    954956      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
    955957      >EQcm %
     958    |7:
     959      >set_clock_mk_Status_commutation >program_counter_set_program_counter
     960      whd in ⊢ (??%?); normalize nodelta
     961      >EQppc in fetch_many_assm; #fetch_many_assm
     962      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
     963      <bitvector_of_nat_sign_extension_equivalence
     964      [1:
     965        whd in ⊢ (???%); cases (half_add ???) normalize //
     966      |2:
     967        @assembly1_lt_128
     968      ]
    956969    |*:
    957970      cases daemon
    958971    ]
     972  ]
    959973]
    960974qed.
Note: See TracChangeset for help on using the changeset viewer.