Changeset 2122


Ignore:
Timestamp:
Jun 27, 2012, 3:36:54 PM (5 years ago)
Author:
sacerdot
Message:

More stuff moved around in proper places

Location:
src/ASM
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2121 r2122  
    765765    eq_instruction i1 i2 = true → i1 ≃ i2.
    766766  #i1 #i2
    767   cases i1 cases i2 cases daemon (*
     767  cases i1 cases i2 cases daemon (* easy but tedious
    768768  [1,10,19,28,37,46:
    769769    #arg1 #arg2
     
    14401440qed.
    14411441
    1442 (*CSC: move elsewhere*)
    1443 example sub_minus_one_seven_eight:
    1444   ∀v: BitVector 7.
    1445   false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
    1446   \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
    1447  cases daemon.
    1448 qed.
    1449 
    14501442(*
    14511443lemma blah:
  • src/ASM/AssemblyProofSplit.ma

    r2121 r2122  
    409409
    410410include alias "ASM/Vector.ma".
    411 
    412 axiom sub16_with_carry_overflow:
    413   ∀left, right, result: BitVector 16.
    414   ∀flags: BitVector 3.
    415   ∀upper: BitVector 9.
    416   ∀lower: BitVector 7.
    417     sub_16_with_carry left right false = 〈result, flags〉 →
    418       vsplit bool 9 7 result = 〈upper, lower〉 →
    419         get_index_v bool 3 flags 2 ? = true →
    420           upper = [[true; true; true; true; true; true; true; true; true]].
    421   //
    422 qed.
    423411
    424412lemma main_lemma_preinstruction:
  • src/ASM/AssemblyProofSplitSplit.ma

    r2110 r2122  
    3232      instruction_has_label id (\fst i) →
    3333        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
    34 
    35 (*CSC: move elsewhere *)
    36 axiom sub_16_to_add_16_8_0:
    37  ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
    38   get_index' ? 2 0 flags = false →
    39   sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
    40    v1 = add ? v2 (sign_extension (false:::v3)).
    41 
    42 (*CSC: move elsewhere *)
    43 axiom sub_16_to_add_16_8_1:
    44  ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
    45   get_index' ? 2 0 flags = true →
    46   sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
    47    v1 = add ? v2 (sign_extension (true:::v3)).
    48 
    49 (*CSC: move elsewhere *)
    50 lemma vsplit_ok:
    51   ∀A: Type[0].
    52   ∀m, n: nat.
    53   ∀v: Vector A (m + n).
    54   ∀upper: Vector A m.
    55   ∀lower: Vector A n.
    56     〈upper, lower〉 = vsplit A m n v →
    57       upper @@ lower = v.
    58   #A #m #n #v #upper #lower
    59   cases daemon
    60 qed.
    6134
    6235lemma short_jump_cond_ok:
  • src/ASM/BitVector.ma

    r2121 r2122  
    235235  ∀b: BitVector n.
    236236    String.
     237
     238example sub_minus_one_seven_eight:
     239  ∀v: BitVector 7.
     240  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
     241  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
     242 cases daemon.
     243qed.
     244
     245axiom sub16_with_carry_overflow:
     246  ∀left, right, result: BitVector 16.
     247  ∀flags: BitVector 3.
     248  ∀upper: BitVector 9.
     249  ∀lower: BitVector 7.
     250    sub_16_with_carry left right false = 〈result, flags〉 →
     251      vsplit bool 9 7 result = 〈upper, lower〉 →
     252        get_index_v bool 3 flags 2 ? = true →
     253          upper = [[true; true; true; true; true; true; true; true; true]].
     254  //
     255qed.
     256
     257axiom sub_16_to_add_16_8_0:
     258 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
     259  get_index' ? 2 0 flags = false →
     260  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
     261   v1 = add ? v2 (sign_extension (false:::v3)).
     262
     263axiom sub_16_to_add_16_8_1:
     264 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
     265  get_index' ? 2 0 flags = true →
     266  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
     267   v1 = add ? v2 (sign_extension (true:::v3)).
  • src/ASM/Vector.ma

    r2121 r2122  
    222222let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
    223223 vsplit' A m n v.
     224
     225lemma vsplit_ok:
     226  ∀A: Type[0].
     227  ∀m, n: nat.
     228  ∀v: Vector A (m + n).
     229  ∀upper: Vector A m.
     230  ∀lower: Vector A n.
     231    〈upper, lower〉 = vsplit A m n v →
     232      upper @@ lower = v.
     233  #A #m #n #v #upper #lower
     234  cases daemon
     235qed.
    224236
    225237lemma vsplit_zero:
Note: See TracChangeset for help on using the changeset viewer.