Changeset 2017


Ignore:
Timestamp:
Jun 4, 2012, 5:38:43 PM (5 years ago)
Author:
mulligan
Message:

Large swathes of proof of main lemma added.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1985 r2017  
    7777qed.
    7878
     79lemma get_8051_sfr_set_program_counter:
     80  ∀M: Type[0].
     81  ∀cm: M.
     82  ∀s: PreStatus M cm.
     83  ∀sfr: SFR8051.
     84  ∀pc: Word.
     85    get_8051_sfr M cm (set_program_counter M cm s pc) =
     86      get_8051_sfr M cm s.
     87  #M #cm #s #sfr #pc %
     88qed.
     89
    7990lemma special_function_registers_8051_set_arg_16:
    8091  ∀M, M': Type[0].
     
    119130qed.
    120131
     132lemma get_ov_flag_set_program_counter:
     133  ∀M: Type[0].
     134  ∀cm: M.
     135  ∀s: PreStatus M cm.
     136  ∀pc: Word.
     137    get_ov_flag M cm (set_program_counter M cm s pc) =
     138      get_ov_flag M cm s.
     139  #M #cm #s #pc %
     140qed.
     141
     142lemma external_ram_set_program_counter:
     143  ∀M: Type[0].
     144  ∀cm: M.
     145  ∀s: PreStatus M cm.
     146  ∀pc: Word.
     147    external_ram M cm (set_program_counter M cm s pc) =
     148      external_ram M cm s.
     149  #M #cm #s #pc %
     150qed.
     151
     152lemma low_internal_ram_set_program_counter:
     153  ∀M: Type[0].
     154  ∀cm: M.
     155  ∀s: PreStatus M cm.
     156  ∀pc: Word.
     157    low_internal_ram M cm (set_program_counter M cm s pc) =
     158      low_internal_ram M cm s.
     159  #M #cm #s #pc %
     160qed.
     161
     162lemma high_internal_ram_set_program_counter:
     163  ∀M: Type[0].
     164  ∀cm: M.
     165  ∀s: PreStatus M cm.
     166  ∀pc: Word.
     167    high_internal_ram M cm (set_program_counter M cm s pc) =
     168      high_internal_ram M cm s.
     169  #M #cm #s #pc %
     170qed.
     171
     172lemma get_arg_8_set_program_counter:
     173  ∀M: Type[0].
     174  ∀cm: M.
     175  ∀s: PreStatus M cm.
     176  ∀flag: bool.
     177  ∀addr.
     178  ∀pc: Word.
     179    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
     180      get_arg_8 M cm s flag addr.
     181  #M #cm #s #flag #addr #pc
     182  whd in match get_arg_8; normalize nodelta
     183  cases addr *
     184  try (#addr1 #addr2 #absurd normalize in absurd; cases absurd @I)
     185  try (#addr1 #absurd normalize in absurd; cases absurd @I)
     186  try (#absurd normalize in absurd; cases absurd @I)
     187  try (#addr1 #addr2) try #addr1
     188  normalize nodelta try %
     189  >external_ram_set_program_counter
     190  >program_counter_set_program_counter
     191  cases daemon (* XXX: rewrite not working but provable *)
     192qed.
     193
     194lemma external_ram_set_flags:
     195  ∀M: Type[0].
     196  ∀cm: M.
     197  ∀s: PreStatus M cm.
     198  ∀opt: option Bit.
     199  ∀bit1, bit2: Bit.
     200    external_ram M cm (set_flags M cm s bit1 opt bit2) =
     201      external_ram M cm s.
     202  #M #cm #s #opt #bit1 #bit2 %
     203qed.
     204
     205lemma low_internal_ram_set_flags:
     206  ∀M: Type[0].
     207  ∀cm: M.
     208  ∀s: PreStatus M cm.
     209  ∀opt: option Bit.
     210  ∀bit1, bit2: Bit.
     211    low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
     212      low_internal_ram M cm s.
     213  #M #cm #s #opt #bit1 #bit2 %
     214qed.
     215
     216lemma high_internal_ram_set_flags:
     217  ∀M: Type[0].
     218  ∀cm: M.
     219  ∀s: PreStatus M cm.
     220  ∀opt: option Bit.
     221  ∀bit1, bit2: Bit.
     222    high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
     223      high_internal_ram M cm s.
     224  #M #cm #s #opt #bit1 #bit2 %
     225qed.
     226
     227lemma low_internal_ram_set_clock:
     228  ∀M: Type[0].
     229  ∀cm: M.
     230  ∀s: PreStatus M cm.
     231  ∀t: Time.
     232    low_internal_ram M cm (set_clock M cm s t) =
     233      low_internal_ram M cm s.
     234  #M #cm #s #t %
     235qed.
     236
     237lemma high_internal_ram_set_clock:
     238  ∀M: Type[0].
     239  ∀cm: M.
     240  ∀s: PreStatus M cm.
     241  ∀t: Time.
     242    high_internal_ram M cm (set_clock M cm s t) =
     243      high_internal_ram M cm s.
     244  #M #cm #s #t %
     245qed.
     246
     247lemma external_ram_set_clock:
     248  ∀M: Type[0].
     249  ∀cm: M.
     250  ∀s: PreStatus M cm.
     251  ∀t: Time.
     252    external_ram M cm (set_clock M cm s t) =
     253      external_ram M cm s.
     254  #M #cm #s #t %
     255qed.
     256
     257lemma set_8051_sfr_set_program_counter:
     258  ∀M: Type[0].
     259  ∀cm: M.
     260  ∀s: PreStatus M cm.
     261  ∀pc: Word.
     262  ∀sfr: SFR8051.
     263  ∀v: Byte.
     264    set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
     265      set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
     266  #M #cm #s #pc #sfr #v %
     267qed.
     268
     269lemma low_internal_ram_set_8051_sfr:
     270  ∀M: Type[0].
     271  ∀cm: M.
     272  ∀s: PreStatus M cm.
     273  ∀sfr: SFR8051.
     274  ∀v: Byte.
     275    low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
     276      low_internal_ram M cm s.
     277  #M #cm #s #sfr #v %
     278qed.
     279
     280lemma high_internal_ram_set_8051_sfr:
     281  ∀M: Type[0].
     282  ∀cm: M.
     283  ∀s: PreStatus M cm.
     284  ∀sfr: SFR8051.
     285  ∀v: Byte.
     286    high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
     287      high_internal_ram M cm s.
     288  #M #cm #s #sfr #v %
     289qed.
     290
     291lemma external_ram_set_8051_sfr:
     292  ∀M: Type[0].
     293  ∀cm: M.
     294  ∀s: PreStatus M cm.
     295  ∀sfr: SFR8051.
     296  ∀v: Byte.
     297    external_ram M cm (set_8051_sfr M cm s sfr v) =
     298      external_ram M cm s.
     299  #M #cm #s #sfr #v %
     300qed.
     301
     302lemma get_arg_8_set_clock:
     303  ∀M: Type[0].
     304  ∀cm: M.
     305  ∀s: PreStatus M cm.
     306  ∀addr.
     307  ∀t: Time.
     308    get_arg_8 M cm (set_clock M cm s t) addr =
     309      get_arg_8 M cm s addr.
     310  #M #cm #s #addr #t %
     311qed.
     312
    121313lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
    122314 #P #A #a #abs destruct
     
    194386  cases (eq_bv_eq … fetch_many_assm) assumption
    195387qed.
     388
     389lemma refl_to_jmrefl:
     390  ∀a: Type[0].
     391  ∀l, r: a.
     392    l = r → l ≃ r.
     393  #a #l #r #refl destruct %
     394qed.
     395
     396include alias "ASM/Vector.ma".
    196397
    197398lemma main_lemma_preinstruction:
     
    654855                  s
    655856           ] (refl … instr))
    656  try (cases(other))
    657  try assumption (*20s*)
    658  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    659  try (
    660    @(execute_1_technical … (subaddressing_modein …))
    661    @I
    662  ) (*66s*)
    663 whd in match execute_1_preinstruction; normalize nodelta
    664 [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
     857  try (cases(other))
     858  try assumption (*20s*)
     859  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
     860  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
     861  whd in match execute_1_preinstruction; normalize nodelta
     862  [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
    665863  (* XXX: work on the right hand side *)
    666864  lapply (subaddressing_modein ???)
     
    669867  try (>p1 normalize nodelta)
    670868  (* XXX: switch to the left hand side *)
    671   -instr_refl >EQP -P normalize nodelta
     869  >EQP -P normalize nodelta
    672870  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    673871  whd in ⊢ (??%?);
     
    688886  whd in ⊢ (??%%);
    689887  (* XXX: finally, prove the equality using sigma commutation *)
    690   cases daemon
    691   (* XXX: work on both sides *)
    692 |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
     888  try @split_eq_status try % whd in ⊢ (??%%);
     889  [1:
     890    >low_internal_ram_set_8051_sfr >low_internal_ram_set_clock
     891    >low_internal_ram_set_program_counter @eq_f2 try %
     892    whd in maps_assm:(??%?); destruct %
     893  |2:
     894    >high_internal_ram_set_8051_sfr >high_internal_ram_set_clock
     895    >high_internal_ram_set_program_counter @eq_f2 try %
     896    whd in maps_assm:(??%?); destruct %
     897  |3:
     898    >clock_set_program_counter >clock_set_program_counter <instr_refl %
     899  |4,6:
     900    >set_clock_set_program_counter >get_arg_8_set_program_counter
     901    >clock_set_program_counter >set_clock_mk_Status_commutation
     902    >set_clock_mk_Status_commutation >clock_set_program_counter <instr_refl
     903  |8:
     904    cases daemon
     905  ]
     906  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
    693907  (* XXX: work on the right hand side *)
    694908  >p normalize nodelta
     
    702916  @(pair_replace ?????????? p)
    703917  [1,3,5,7,9,11,13,15,17:
     918    >set_clock_set_program_counter >set_clock_mk_Status_commutation
     919    >set_program_counter_mk_Status_commutation >clock_set_program_counter
    704920    cases daemon
    705921  |14,16,18:
    706922    normalize nodelta
    707923    @(pair_replace ?????????? p1)
    708        [1,3,5:
    709          cases daemon
    710        ]
     924    [1,3,5:
     925      >set_clock_mk_Status_commutation
     926      cases daemon
     927    ]
    711928  ]
    712929  (* XXX: switch to the right hand side *)
     
    714931  whd in ⊢ (??%%);
    715932  (* XXX: finally, prove the equality using sigma commutation *)
     933  try @split_eq_status try %
     934  >set_clock_mk_Status_commutation
    716935  cases daemon (*
    717936       @split_eq_status try %
     
    720939           (* CSC: TO BE COMPLETED *)
    721940       ] *)
    722 |10,42,43,44,45,49,52,56: (* MUL *)
     941  |10,42,43,44,45,49,52,56: (* MUL *)
    723942  (* XXX: work on the right hand side *)
    724943  (* XXX: switch to the left hand side *)
     
    733952  (* XXX: finally, prove the equality using sigma commutation *)
    734953  cases daemon
    735 |11,12: (* DIV *)
     954  |11,12: (* DIV *)
    736955  (* XXX: work on the right hand side *)
    737956  normalize nodelta in p;
     
    755974    cases daemon
    756975  ]
    757 |13,14,15: (* DA *)
     976  |13,14,15: (* DA *)
    758977  (* XXX: work on the right hand side *)
    759978  >p normalize nodelta
     
    771990  @(pair_replace ?????????? p)
    772991  [1,3,5:
     992    /demod/
    773993    cases daemon
    774994  |2,4,6:
     
    7931013  cases daemon
    7941014  ]
    795 |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
     1015  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
    7961016  (* XXX: work on the right hand side *)
    7971017  cases addr #addr' normalize nodelta
     
    8111031  (* XXX: finally, prove the equality using sigma commutation *)
    8121032  cases daemon
    813 |47: (* MOV *)
     1033  |47: (* MOV *)
    8141034  (* XXX: work on the right hand side *)
    8151035  cases addr -addr #addr normalize nodelta
     
    8381058  (* XXX: finally, prove the equality using sigma commutation *)
    8391059  cases daemon
    840 |17,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases) *)
     1060  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
    8411061  (* XXX: work on the right hand side *)
    8421062  >p normalize nodelta
     
    8511071  @pair_elim #upper #lower #split_refl
    8521072  cases (eq_bv ???) normalize nodelta
    853   [1,3,5,7,9,11,13,15:
     1073  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    8541074    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    8551075    whd in ⊢ (??%?);
     
    8571077    (* XXX: work on the left hand side *)
    8581078    @(if_then_else_replace ???????? p) normalize nodelta
    859     [1,3,5,7,9,11,13,15:
     1079    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    8601080      cases daemon
    8611081    ]
     
    8661086    @split_eq_status try %
    8671087    cases daemon
    868   |2,4,6,8,10,12,14,16:
     1088  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    8691089    >EQppc
    8701090    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     
    8761096    #status_after_1 #EQstatus_after_1
    8771097    <(?: ? = status_after_1)
    878     [3,6,9,12,15,18,21,24:
     1098    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
    8791099      >EQstatus_after_1 in ⊢ (???%);
    8801100      whd in ⊢ (???%);
     
    8871107      |7: <fetch_refl in ⊢ (???%);
    8881108      |8: <fetch_refl in ⊢ (???%);
     1109      |9: <fetch_refl in ⊢ (???%);
     1110      |10: <fetch_refl in ⊢ (???%);
     1111      |11: <fetch_refl in ⊢ (???%);
     1112      |12: <fetch_refl in ⊢ (???%);
     1113      |13: <fetch_refl in ⊢ (???%);
     1114      |14: <fetch_refl in ⊢ (???%);
    8891115      ]
    8901116      whd in ⊢ (???%);
    8911117      @(if_then_else_replace ???????? p)
    892       [1,3,5,7,9,11,13,15:
     1118      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    8931119        cases daemon
    894       |2,4,6,8,10,12,14,16:
     1120      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    8951121        normalize nodelta
    8961122        whd in match (addr_of_relative ????);
    8971123        >set_clock_mk_Status_commutation
    898         [6:
     1124        [9,10:
    8991125          (* XXX: demodulation not working in this case *)
    9001126          >program_counter_set_arg_1 in ⊢ (???%);
     
    9061132        change with (add ???) in match (\snd (half_add ???));
    9071133        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    908         [2,4,6,8,10,12,14,16:
     1134        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    9091135          >bitvector_of_nat_sign_extension_equivalence
    910           [1,3,5,7,9,11,13,15:
     1136          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    9111137            >EQintermediate_pc' %
    9121138          |*:
     
    9161142        %
    9171143      ]
    918     |1,4,7,10,13,16,19,22:
     1144    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
    9191145      skip
    9201146    ]
     
    9231149    #status_after_1 #EQstatus_after_1
    9241150    <(?: ? = status_after_1)
    925     [3,6,9,12,15,18,21,24:
     1151    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
    9261152      >EQstatus_after_1 in ⊢ (???%);
    9271153      whd in ⊢ (???%);
     
    9301156      |2: <fetch_refl' in ⊢ (???%);
    9311157      |3: <fetch_refl'' in ⊢ (???%);
    932       |4: <fetch_refl'' in ⊢ (???%);
     1158      |4: <fetch_refl' in ⊢ (???%);
    9331159      |5: <fetch_refl'' in ⊢ (???%);
    934       |6: <fetch_refl'' in ⊢ (???%);
     1160      |6: <fetch_refl' in ⊢ (???%);
    9351161      |7: <fetch_refl'' in ⊢ (???%);
    936       |8: <fetch_refl'' in ⊢ (???%);
     1162      |8: <fetch_refl' in ⊢ (???%);
     1163      |9: <fetch_refl'' in ⊢ (???%);
     1164      |10: <fetch_refl' in ⊢ (???%);
     1165      |11: <fetch_refl'' in ⊢ (???%);
     1166      |12: <fetch_refl' in ⊢ (???%);
     1167      |13: <fetch_refl'' in ⊢ (???%);
     1168      |14: <fetch_refl' in ⊢ (???%);
    9371169      ]
    9381170      whd in ⊢ (???%);
    939       [6:
     1171      [9,10:
    9401172      |*:
    9411173        /demod/
    9421174      ] %
    943     |1,4,7,10,13,16,19,22:
     1175    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
    9441176      skip
    9451177    ]
     
    9501182    (* XXX: finally, prove the equality using sigma commutation *)
    9511183    @split_eq_status try %
    952     [3,11,15,19,24,32,36:
     1184    [3,11,19,27,36,53,61:
    9531185      >program_counter_set_program_counter >set_clock_mk_Status_commutation
    9541186      [5: >program_counter_set_program_counter ]
     
    9561188      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
    9571189      >EQcm %
    958     |7:
     1190    |7,15,23,31,45,57,65:
    9591191      >set_clock_mk_Status_commutation >program_counter_set_program_counter
    9601192      whd in ⊢ (??%?); normalize nodelta
    9611193      >EQppc in fetch_many_assm; #fetch_many_assm
     1194      [5:
     1195        >program_counter_set_arg_1 >program_counter_set_program_counter
     1196      ]
    9621197      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
    9631198      <bitvector_of_nat_sign_extension_equivalence
    964       [1:
     1199      [1,3,5,7,9,11,13:
    9651200        whd in ⊢ (???%); cases (half_add ???) normalize //
    966       |2:
     1201      |2,4,6,8,10,12,14:
    9671202        @assembly1_lt_128
     1203        @le_S_S @le_O_n
    9681204      ]
    9691205    |*:
     
    9711207    ]
    9721208  ]
     1209  |30: (* CJNE *)
     1210  cases addr1 * #addr1_l #addr1_r normalize nodelta
     1211  (* XXX: work on the right hand side *)
     1212  (* XXX: switch to the left hand side *)
     1213  -instr_refl >EQP -P normalize nodelta
     1214  #sigma_increment_commutation #maps_assm #fetch_many_assm
     1215
     1216  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     1217  whd in match (expand_relative_jump ????);
     1218  <EQppc in fetch_many_assm;
     1219  @pair_elim #result #flags #sub16_refl
     1220  @pair_elim #upper #lower #split_refl
     1221  cases (eq_bv ???) normalize nodelta
     1222  [1,3:
     1223    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     1224    whd in ⊢ (??%?);
     1225    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1226    (* XXX: work on the left hand side *)
     1227    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
     1228    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
     1229    @(if_then_else_replace ???????? eq_bv_refl)
     1230    [1,3,5,7:
     1231      cases daemon
     1232    |*:
     1233      (* XXX: switch to the right hand side *)
     1234      normalize nodelta >EQs -s >EQticks -ticks
     1235      whd in ⊢ (??%%);
     1236      (* XXX: finally, prove the equality using sigma commutation *)
     1237      @split_eq_status try %
     1238      cases daemon
     1239    ]
     1240  |2,4:
     1241    >EQppc
     1242    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     1243    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     1244    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     1245    #fetch_many_assm whd in fetch_many_assm; %{2}
     1246    change with (execute_1 ?? = ?)
     1247    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     1248    #status_after_1 #EQstatus_after_1
     1249    <(?: ? = status_after_1)
     1250    [3,6:
     1251      >EQstatus_after_1 in ⊢ (???%);
     1252      whd in ⊢ (???%);
     1253      [1:
     1254        <fetch_refl in ⊢ (???%);
     1255      |2:
     1256        <fetch_refl in ⊢ (???%);
     1257      ]
     1258      whd in ⊢ (???%);
     1259      cases (¬ eq_bv ???) normalize nodelta
     1260      whd in match (addr_of_relative ????);
     1261      >set_clock_mk_Status_commutation
     1262      whd in ⊢ (???%);
     1263        [9,10:
     1264          (* XXX: demodulation not working in this case *)
     1265          >program_counter_set_arg_1 in ⊢ (???%);
     1266          >program_counter_set_program_counter in ⊢ (???%);
     1267        |*:
     1268          /demod/
     1269        ]
     1270        whd in ⊢ (???%);
     1271        change with (add ???) in match (\snd (half_add ???));
     1272        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     1273        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     1274          >bitvector_of_nat_sign_extension_equivalence
     1275          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     1276            >EQintermediate_pc' %
     1277          |*:
     1278            repeat @le_S_S @le_O_n
     1279          ]
     1280        ]
     1281        %
     1282    ]
     1283     
     1284  ]
    9731285]
     1286cases daemon (* XXX: CJNE and DJNZ cases *)
    9741287qed.
    9751288(*   
     
    10801393    whd in fetch_many_assm;
    10811394    >EQassembled in fetch_many_assm;
    1082     cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
     1395    cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
    10831396    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
    10841397    #fetch_many_assm whd in fetch_many_assm;
Note: See TracChangeset for help on using the changeset viewer.