Changeset 2032 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (9 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r2014 r2032  
    1313qed.
    1414   
    15 lemma eq_a_to_eq:
    16   ∀a,b.
    17     eq_a a b = true → a = b.
    18  #a #b
    19  cases a cases b
    20  #K
    21  try cases (eq_true_false K)
    22  %
    23 qed.
    24 
    25 lemma is_a_to_mem_to_is_in:
    26  ∀he,a,m,q.
    27    is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
    28  #he #a #m #q
    29  elim q
    30  [1:
    31    #_ #K assumption
    32  |2:
    33    #m' #t #q' #II #H1 #H2
    34    normalize
    35    change with (orb ??) in H2:(??%?);
    36    cases (inclusive_disjunction_true … H2)
    37    [1:
    38      #K
    39      <(eq_a_to_eq … K) >H1 %
    40    |2:
    41      #K
    42      >II
    43      try assumption
    44      cases (is_a t a)
    45      normalize
    46      %
    47    ]
    48  ]
    49 qed.
    50 
    5115lemma execute_1_technical:
    5216  ∀n, m: nat.
    … …  
    261225        | DA addr ⇒ λinstr_refl.
    262226            let s ≝ add_ticks1 s in
    263             let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     227            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
    264228              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
    265229                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    266230                let cy_flag ≝ get_index' ? O ? flags in
    267                 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     231                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    268232                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    269233                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
    … …  
    339303            let s ≝ add_ticks1 s in
    340304            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    341             let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     305            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
    342306            let new_acc ≝ nl @@ nu in
    343307              set_8051_sfr … s SFR_ACC_A new_acc
    … …  
    365329        | XCHD addr1 addr2 ⇒ λinstr_refl.
    366330            let s ≝ add_ticks1 s in
    367             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
    368             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     331            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     332            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
    369333            let new_acc ≝ acc_nu @@ arg_nl in
    370334            let new_arg ≝ arg_nu @@ acc_nl in
    … …  
    685649        | DA addr ⇒ λinstr_refl.
    686650            let s ≝ add_ticks1 s in
    687             let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     651            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
    688652              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
    689653                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    690654                let cy_flag ≝ get_index' ? O ? flags in
    691                 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     655                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    692656                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    693657                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
    … …  
    763727            let s ≝ add_ticks1 s in
    764728            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    765             let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     729            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
    766730            let new_acc ≝ nl @@ nu in
    767731              set_8051_sfr … s SFR_ACC_A new_acc
    … …  
    789753        | XCHD addr1 addr2 ⇒ λinstr_refl.
    790754            let s ≝ add_ticks1 s in
    791             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
    792             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     755            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     756            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
    793757            let new_acc ≝ acc_nu @@ arg_nl in
    794758            let new_arg ≝ arg_nu @@ acc_nl in
    … …  
    1026990        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    1027991        [ ADDR11 a ⇒ λaddr11: True.
    1028           let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in
    1029           let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     992          let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 program_counter in
     993          let 〈nu, nl〉 ≝ vsplit ? 4 4 pc_bu in
    1030994          let bit ≝ get_index' ? O ? nl in
    1031           let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
     995          let 〈relevant1, relevant2〉 ≝ vsplit ? 3 8 a in
    1032996          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    1033997          let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in
    … …  
    10491013    | _ ⇒ false
    10501014    ].
    1051 
    1052 let rec member_addressing_mode_tag
    1053   (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
    1054     on v: Prop ≝
    1055   match v with
    1056   [ VEmpty ⇒ False
    1057   | VCons n' hd tl ⇒
    1058       bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
    1059   ].
    1060 
    1061 lemma is_a_decidable:
    1062   ∀hd.
    1063   ∀element.
    1064     is_a hd element = true ∨ is_a hd element = false.
    1065   #hd #element //
    1066 qed.
    1067 
    1068 lemma mem_decidable:
    1069   ∀n: nat.
    1070   ∀v: Vector addressing_mode_tag n.
    1071   ∀element: addressing_mode_tag.
    1072     mem … eq_a n v element = true ∨
    1073       mem … eq_a … v element = false.
    1074   #n #v #element //
    1075 qed.
    1076 
    1077 lemma eq_a_elim:
    1078   ∀tag.
    1079   ∀hd.
    1080   ∀P: bool → Prop.
    1081     (tag = hd → P (true)) →
    1082       (tag ≠ hd → P (false)) →
    1083         P (eq_a tag hd).
    1084   #tag #hd #P
    1085   cases tag
    1086   cases hd
    1087   #true_hyp #false_hyp
    1088   try @false_hyp
    1089   try @true_hyp
    1090   try %
    1091   #absurd destruct(absurd)
    1092 qed.
    1093  
    1094 lemma is_a_true_to_is_in:
    1095   ∀n: nat.
    1096   ∀x: addressing_mode.
    1097   ∀tag: addressing_mode_tag.
    1098   ∀supervector: Vector addressing_mode_tag n.
    1099   mem addressing_mode_tag eq_a n supervector tag →
    1100     is_a tag x = true →
    1101       is_in … supervector x.
    1102   #n #x #tag #supervector
    1103   elim supervector
    1104   [1:
    1105     #absurd cases absurd
    1106   |2:
    1107     #n' #hd #tl #inductive_hypothesis
    1108     whd in match (mem … eq_a (S n') (hd:::tl) tag);
    1109     @eq_a_elim normalize nodelta
    1110     [1:
    1111       #tag_hd_eq #irrelevant
    1112       whd in match (is_in (S n') (hd:::tl) x);
    1113       <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
    1114       @I
    1115     |2:
    1116       #tag_hd_neq
    1117       whd in match (is_in (S n') (hd:::tl) x);
    1118       change with (
    1119         mem … eq_a n' tl tag)
    1120           in match (fold_right … n' ? false tl);
    1121       #mem_hyp #is_a_hyp
    1122       cases(is_a hd x)
    1123       [1:
    1124         normalize nodelta //
    1125       |2:
    1126         normalize nodelta
    1127         @inductive_hypothesis assumption
    1128       ]
    1129     ]
    1130   ]
    1131 qed.
    1132 
    1133 lemma is_in_subvector_is_in_supervector:
    1134   ∀m, n: nat.
    1135   ∀subvector: Vector addressing_mode_tag m.
    1136   ∀supervector: Vector addressing_mode_tag n.
    1137   ∀element: addressing_mode.
    1138     subvector_with … eq_a subvector supervector →
    1139       is_in m subvector element → is_in n supervector element.
    1140   #m #n #subvector #supervector #element
    1141   elim subvector
    1142   [1:
    1143     #subvector_with_proof #is_in_proof
    1144     cases is_in_proof
    1145   |2:
    1146     #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
    1147     whd in match (is_in … (hd':::tl') element);
    1148     cases (is_a_decidable hd' element)
    1149     [1:
    1150       #is_a_true >is_a_true
    1151       #irrelevant
    1152       whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
    1153       @(is_a_true_to_is_in … is_a_true)
    1154       lapply(subvector_with_proof)
    1155       cases(mem … eq_a n supervector hd') //
    1156     |2:
    1157       #is_a_false >is_a_false normalize nodelta
    1158       #assm
    1159       @inductive_hypothesis
    1160       [1:
    1161         generalize in match subvector_with_proof;
    1162         whd in match (subvector_with … eq_a (hd':::tl') supervector);
    1163         cases(mem_decidable n supervector hd')
    1164         [1:
    1165           #mem_true >mem_true normalize nodelta
    1166           #assm assumption
    1167         |2:
    1168           #mem_false >mem_false #absurd
    1169           cases absurd
    1170         ]
    1171       |2:
    1172         assumption
    1173       ]
    1174     ]
    1175   ]
    1176 qed.
    1177  
    1178 let rec subaddressing_mode_elim_type
    1179   (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
    1180     (Q: addressing_mode → T → Prop)
    1181       (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
    1182       (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
    1183       (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
    1184       (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
    1185       (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
    1186       (p_acc_a:                              is_in m fixed_v ACC_A             → T)
    1187       (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
    1188       (p_acc_b:                              is_in m fixed_v ACC_B             → T)
    1189       (p_dptr:                               is_in m fixed_v DPTR              → T)
    1190       (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
    1191       (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
    1192       (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
    1193       (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
    1194       (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
    1195       (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
    1196       (p_carry:                              is_in m fixed_v CARRY             → T)
    1197       (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
    1198       (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
    1199       (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
    1200         (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
    1201       on v: Prop ≝
    1202   match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
    1203   [ VEmpty         ⇒ λm_refl. λv_refl.
    1204       ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
    1205         Q addr (
    1206         match addr return λx: addressing_mode. is_in … fixed_v x → T with 
    1207         [ ADDR11 x          ⇒ p_addr11 x
    1208         | ADDR16 x          ⇒ p_addr16 x
    1209         | DIRECT x          ⇒ p_direct x
    1210         | INDIRECT x        ⇒ p_indirect x
    1211         | EXT_INDIRECT x    ⇒ p_ext_indirect x
    1212         | ACC_A             ⇒ p_acc_a
    1213         | REGISTER x        ⇒ p_register x
    1214         | ACC_B             ⇒ p_acc_b
    1215         | DPTR              ⇒ p_dptr
    1216         | DATA x            ⇒ p_data x
    1217         | DATA16 x          ⇒ p_data16 x
    1218         | ACC_DPTR          ⇒ p_acc_dptr
    1219         | ACC_PC            ⇒ p_acc_pc
    1220         | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
    1221         | INDIRECT_DPTR     ⇒ p_indirect_dptr
    1222         | CARRY             ⇒ p_carry
    1223         | BIT_ADDR x        ⇒ p_bit_addr x
    1224         | N_BIT_ADDR x      ⇒ p_n_bit_addr x
    1225         | RELATIVE x        ⇒ p_relative x
    1226         ] p)
    1227   | VCons n' hd tl ⇒ λm_refl. λv_refl.
    1228     let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
    1229       p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
    1230         p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
    1231           p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
    1232             p_bit_addr p_n_bit_addr p_relative n' tl ?
    1233     in
    1234     match hd return λa: addressing_mode_tag. a = hd → ? with
    1235     [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
    1236     | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
    1237     | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
    1238     | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
    1239     | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
    1240     | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
    1241     | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
    1242     | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
    1243     | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
    1244     | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
    1245     | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
    1246     | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
    1247     | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
    1248     | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
    1249     | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
    1250     | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
    1251     | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
    1252     | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
    1253     | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
    1254     ] (refl … hd)
    1255   ] (refl … n) (refl_jmeq … v).
    1256   [20:
    1257     generalize in match proof; destruct
    1258     whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
    1259     cases (mem … eq_a m fixed_v hd) normalize nodelta
    1260     [1:
    1261       whd in match (subvector_with … eq_a tl fixed_v);
    1262       #assm assumption
    1263     |2:
    1264       normalize in ⊢ (% → ?);
    1265       #absurd cases absurd
    1266     ]
    1267   ]
    1268   @(is_in_subvector_is_in_supervector … proof)
    1269   destruct @I
    1270 qed.
    1271 
    1272 (* XXX: todo *)
    1273 lemma subaddressing_mode_elim':
    1274   ∀T: Type[2].
    1275   ∀n: nat.
    1276   ∀o: nat.
    1277   ∀v1: Vector addressing_mode_tag n.
    1278   ∀v2: Vector addressing_mode_tag o.
    1279   ∀Q: addressing_mode → T → Prop.
    1280   ∀fixed_v: Vector addressing_mode_tag (n + o).
    1281   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    1282   ∀fixed_v_proof: fixed_v = v1 @@ v2.
    1283   ∀subaddressing_mode_proof.
    1284     subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
    1285       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
    1286   #T #n #o #v1 #v2
    1287   elim v1 cases v2
    1288   [1:
    1289     #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    1290     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    1291     #subaddressing_mode_proof destruct normalize
    1292     #addr #absurd cases absurd
    1293   |2:
    1294     #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    1295     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    1296     destruct normalize in match ([[]]@@hd:::tl);
    1297   ]
    1298   cases daemon
    1299 qed.
    1300 
    1301 (* XXX: todo *)
    1302 lemma subaddressing_mode_elim:
    1303   ∀T: Type[2].
    1304   ∀m: nat.
    1305   ∀n: nat.
    1306   ∀Q: addressing_mode → T → Prop.
    1307   ∀fixed_v: Vector addressing_mode_tag m.
    1308   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    1309   ∀v: Vector addressing_mode_tag n.
    1310   ∀proof.
    1311     subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    1312       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    1313   #T #m #n #Q #fixed_v
    1314   elim fixed_v
    1315   [1:
    1316     #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
    1317     #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
    1318     normalize
    1319   |2:
    1320   ]
    1321   cases daemon
    1322 qed.
    13231015
    13241016definition program_counter_after_other ≝
    … …  
    13971089              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    13981090              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1399               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
     1091              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    14001092              let s ≝ write_at_stack_pointer … s pc_bl in
    14011093              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    14021094              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    14031095              let s ≝ write_at_stack_pointer … s pc_bu in
    1404               let 〈thr, eig〉 ≝ split ? 3 8 a in
    1405               let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
     1096              let 〈thr, eig〉 ≝ vsplit ? 3 8 a in
     1097              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
    14061098              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    14071099                set_program_counter … s new_addr
    … …  
    14151107              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    14161108              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1417               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
     1109              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    14181110              let s ≝ write_at_stack_pointer … s pc_bl in
    14191111              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    … …  
    15151207      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    15161208      let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1517       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
     1209      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    15181210      let s ≝ write_at_stack_pointer … s pc_bl in
    15191211      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
Note: See TracChangeset for help on using the changeset viewer.