Changeset 2899


Ignore:
Timestamp:
Mar 19, 2013, 12:33:13 AM (4 years ago)
Author:
sacerdot
Message:
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
Location:
src
Files:
11 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2832 r2899  
    99(*include "common/StructuredTraces.ma". (* included by ASM/AbstractStatus.ma *) *)
    1010
    11 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     11definition OC_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    1212  λcode_memory.
    1313  λcost_labels.
     
    1717      word_deqset
    1818      (program_counter …)
    19       (ASM_classify …)
     19      (OC_classify …)
    2020      (λpc.lookup_opt … pc cost_labels)
    2121      (next_instruction_properly_relates_program_counters code_memory)
     
    3232  λstart_status: Status code_memory.
    3333  λfinal_status: Status code_memory.
    34   λthe_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     34  λthe_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    3535    as_trace_any_label_length' … the_trace.
    3636
     
    137137  ∀code_memory: BitVectorTrie Byte 16.
    138138  ∀start_status: Status code_memory.
    139     ASM_classify … start_status = cl_other →
     139    OC_classify … start_status = cl_other →
    140140      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    141141        program_counter ? ? (execute_1 … start_status) =
     
    153153  ∀cost_labels: BitVectorTrie costlabel 16.
    154154  ∀start_status: Status code_memory.
    155     as_classifier (ASM_abstract_status code_memory cost_labels) start_status cl_other →
     155    as_classifier (OC_abstract_status code_memory cost_labels) start_status cl_other →
    156156      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    157157        program_counter ? ? (execute_1 … start_status) =
     
    168168  ∀start, final: Status code_memory.
    169169  ∀trace_ends_flag.
    170   ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start final.
     170  ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
    171171    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
    172172  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace
     
    181181  ∀start, final: Status code_memory.
    182182  ∀trace_ends_flag.
    183   ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start final.
     183  ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
    184184  ∀unrepeating_witness: tal_unrepeating … the_trace.
    185185    |tal_pc_list … the_trace| ≤ 2^16.
     
    200200    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    201201      (final_status: Status code_memory)
    202         (the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status)
     202        (the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status)
    203203       on the_trace: nat ≝
    204204  match the_trace with
     
    227227  λstart_status: Status code_memory.
    228228  λfinal_status: Status code_memory.
    229   λthe_trace: (trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     229  λthe_trace: (trace_label_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
    230230  match the_trace with
    231231  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    246246  ∀final_status : (Status code_memory').
    247247  ∀trace_ends_flag : trace_ends_with_ret.
    248   ∀the_trace : (trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     248  ∀the_trace : (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
    249249  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    250250  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
     
    259259      ∀final_status0:Status code_memory'.
    260260      ∀trace_ends_flag0:trace_ends_with_ret.
    261       ∀the_trace0:trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag0 start_status0 final_status0.
     261      ∀the_trace0:trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag0 start_status0 final_status0.
    262262        trace_any_label_length … the_trace0 ≤ program_size' →
    263263        program_counter''' = program_counter … start_status0 →
     
    366366          ]
    367367        |1:
    368                 (* JHM: wicked failure because Some prevent previous unfolding of ASM_classify here *)
     368                (* JHM: wicked failure because Some prevent previous unfolding of OC_classify here *)
    369369                @⊥
    370370                (* *** (* previously: unnecessary case analysis on instruction *)
     
    404404  ∀final_status: (Status code_memory').
    405405  ∀trace_ends_flag: trace_ends_with_ret.
    406   ∀the_trace: (trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     406  ∀the_trace: (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
    407407  ∀program_counter_refl: (program_counter' = program_counter … start_status).
    408408  ∀classify_assm: ASM_classify0 instruction = cl_jump.
     
    462462  ∀final_status : (Status code_memory').
    463463  ∀trace_ends_flag : trace_ends_with_ret.
    464   ∀the_trace : trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     464  ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    465465  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    466466  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
     
    473473              .∀trace_ends_flag0:trace_ends_with_ret
    474474               .∀the_trace0:trace_any_label
    475                                         (ASM_abstract_status … cost_labels)
     475                                        (OC_abstract_status … cost_labels)
    476476                                        trace_ends_flag0 start_status0 final_status0.
    477477                trace_any_label_length … the_trace0
     
    601601  ∀final_status : (Status code_memory').
    602602  ∀trace_ends_flag : trace_ends_with_ret.
    603   ∀the_trace : trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     603  ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    604604  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    605605  ∀classify_assm: ASM_classify0 instruction = cl_return.
     
    663663  ∀start_status: Status code_memory.
    664664  ∀final_status: Status code_memory.
    665   ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     665  ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    666666   trace_any_label_length … the_trace ≤ 0 → False.
    667667  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
     
    680680            ∀final_status: Status code_memory'.
    681681            ∀trace_ends_flag.
    682             ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     682            ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    683683              trace_any_label_length … the_trace ≤ program_size →
    684684              program_counter' = program_counter … start_status →
     
    704704            ∀final_status: Status code_memory'.
    705705            ∀trace_ends_flag.
    706             ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
     706            ∀the_trace: trace_any_label (OC_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
    707707              trace_any_label_length … the_trace ≤ S program_size' →
    708708              program_counter' = program_counter … start_status →
     
    748748            ∀final_status: Status code_memory'.
    749749            ∀trace_ends_flag.
    750             ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     750            ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    751751              trace_any_label_length … the_trace ≤ S program_size' →
    752752              program_counter' = program_counter … start_status →
     
    811811        ∀final_status: Status code_memory'.
    812812        ∀trace_ends_flag.
    813         ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     813        ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    814814        ∀unrepeating_witness: tal_unrepeating … the_trace.
    815815          program_counter' = program_counter … start_status →
  • src/ASM/ASMCostsSplit.ma

    r2760 r2899  
    331331  ∀p: labelled_object_code.
    332332  let code_memory ≝ load_code_memory (oc p) in
    333   let a_s ≝ ASM_abstract_status code_memory (costlabels p) in
     333  let a_s ≝ OC_abstract_status code_memory (costlabels p) in
    334334  as_cost_map a_s ≝
    335335  λp.
  • src/ASM/AbstractStatus.ma

    r2770 r2899  
    6464qed.
    6565   
    66 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
     66definition OC_classify: ∀code_memory. Status code_memory → status_class ≝
    6767  λcode_memory.
    6868  λs: Status code_memory.
  • src/ASM/Assembly.ma

    r2781 r2899  
    10441044     (foldr … (λi,l. assembly1 i @ l) [ ] p) 〈Stub …, Stub …〉〉).
    10451045*)
     1046
     1047definition ticks_of_instruction ≝
     1048  λi.
     1049    let trivial_code_memory ≝ assembly1 i in
     1050    let trivial_status ≝ load_code_memory trivial_code_memory in
     1051      \snd (fetch trivial_status (zero ?)).
     1052
     1053definition ticks_of0:
     1054    ∀p:pseudo_assembly_program.
     1055      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
     1056  λprogram: pseudo_assembly_program.
     1057  λlookup_labels: Identifier → Word.
     1058  λsigma.
     1059  λpolicy.
     1060  λppc: Word.
     1061  λfetched.
     1062    match fetched with
     1063    [ Instruction instr ⇒
     1064      match instr with
     1065      [ JC lbl ⇒
     1066        let lookup_address ≝ sigma (lookup_labels lbl) in
     1067        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1068        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1069          if sj_possible then
     1070            〈2, 2〉
     1071          else
     1072            〈4, 4〉
     1073      | JMP _ ⇒ ? (*CSC: To be implemented*)
     1074      | JNC lbl ⇒
     1075        let lookup_address ≝ sigma (lookup_labels lbl) in
     1076        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1077        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1078          if sj_possible then
     1079            〈2, 2〉
     1080          else
     1081            〈4, 4〉
     1082      | JB bit lbl ⇒
     1083        let lookup_address ≝ sigma (lookup_labels lbl) in
     1084        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1085        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1086          if sj_possible then
     1087            〈2, 2〉
     1088          else
     1089            〈4, 4〉
     1090      | JNB bit lbl ⇒
     1091        let lookup_address ≝ sigma (lookup_labels lbl) in
     1092        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1093        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1094          if sj_possible then
     1095            〈2, 2〉
     1096          else
     1097            〈4, 4〉
     1098      | JBC bit lbl ⇒
     1099        let lookup_address ≝ sigma (lookup_labels lbl) in
     1100        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1101        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1102          if sj_possible then
     1103            〈2, 2〉
     1104          else
     1105            〈4, 4〉
     1106      | JZ lbl ⇒
     1107        let lookup_address ≝ sigma (lookup_labels lbl) in
     1108        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1109        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1110          if sj_possible then
     1111            〈2, 2〉
     1112          else
     1113            〈4, 4〉
     1114      | JNZ lbl ⇒
     1115        let lookup_address ≝ sigma (lookup_labels lbl) in
     1116        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1117        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1118          if sj_possible then
     1119            〈2, 2〉
     1120          else
     1121            〈4, 4〉
     1122      | CJNE arg lbl ⇒
     1123        let lookup_address ≝ sigma (lookup_labels lbl) in
     1124        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1125        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1126          if sj_possible then
     1127            〈2, 2〉
     1128          else
     1129            〈4, 4〉
     1130      | DJNZ arg lbl ⇒
     1131        let lookup_address ≝ sigma (lookup_labels lbl) in
     1132        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1133        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1134          if sj_possible then
     1135            〈2, 2〉
     1136          else
     1137            〈4, 4〉
     1138      | ADD arg1 arg2 ⇒
     1139        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     1140         〈ticks, ticks〉
     1141      | ADDC arg1 arg2 ⇒
     1142        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
     1143         〈ticks, ticks〉
     1144      | SUBB arg1 arg2 ⇒
     1145        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
     1146         〈ticks, ticks〉
     1147      | INC arg ⇒
     1148        let ticks ≝ ticks_of_instruction (INC ? arg) in
     1149         〈ticks, ticks〉
     1150      | DEC arg ⇒
     1151        let ticks ≝ ticks_of_instruction (DEC ? arg) in
     1152         〈ticks, ticks〉
     1153      | MUL arg1 arg2 ⇒
     1154        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
     1155         〈ticks, ticks〉
     1156      | DIV arg1 arg2 ⇒
     1157        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
     1158         〈ticks, ticks〉
     1159      | DA arg ⇒
     1160        let ticks ≝ ticks_of_instruction (DA ? arg) in
     1161         〈ticks, ticks〉
     1162      | ANL arg ⇒
     1163        let ticks ≝ ticks_of_instruction (ANL ? arg) in
     1164         〈ticks, ticks〉
     1165      | ORL arg ⇒
     1166        let ticks ≝ ticks_of_instruction (ORL ? arg) in
     1167         〈ticks, ticks〉
     1168      | XRL arg ⇒
     1169        let ticks ≝ ticks_of_instruction (XRL ? arg) in
     1170         〈ticks, ticks〉
     1171      | CLR arg ⇒
     1172        let ticks ≝ ticks_of_instruction (CLR ? arg) in
     1173         〈ticks, ticks〉
     1174      | CPL arg ⇒
     1175        let ticks ≝ ticks_of_instruction (CPL ? arg) in
     1176         〈ticks, ticks〉
     1177      | RL arg ⇒
     1178        let ticks ≝ ticks_of_instruction (RL ? arg) in
     1179         〈ticks, ticks〉
     1180      | RLC arg ⇒
     1181        let ticks ≝ ticks_of_instruction (RLC ? arg) in
     1182         〈ticks, ticks〉
     1183      | RR arg ⇒
     1184        let ticks ≝ ticks_of_instruction (RR ? arg) in
     1185         〈ticks, ticks〉
     1186      | RRC arg ⇒
     1187        let ticks ≝ ticks_of_instruction (RRC ? arg) in
     1188         〈ticks, ticks〉
     1189      | SWAP arg ⇒
     1190        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
     1191         〈ticks, ticks〉
     1192      | MOV arg ⇒
     1193        let ticks ≝ ticks_of_instruction (MOV ? arg) in
     1194         〈ticks, ticks〉
     1195      | MOVX arg ⇒
     1196        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
     1197         〈ticks, ticks〉
     1198      | SETB arg ⇒
     1199        let ticks ≝ ticks_of_instruction (SETB ? arg) in
     1200         〈ticks, ticks〉
     1201      | PUSH arg ⇒
     1202        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
     1203         〈ticks, ticks〉
     1204      | POP arg ⇒
     1205        let ticks ≝ ticks_of_instruction (POP ? arg) in
     1206         〈ticks, ticks〉
     1207      | XCH arg1 arg2 ⇒
     1208        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
     1209         〈ticks, ticks〉
     1210      | XCHD arg1 arg2 ⇒
     1211        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
     1212         〈ticks, ticks〉
     1213      | RET ⇒
     1214        let ticks ≝ ticks_of_instruction (RET ?) in
     1215         〈ticks, ticks〉
     1216      | RETI ⇒
     1217        let ticks ≝ ticks_of_instruction (RETI ?) in
     1218         〈ticks, ticks〉
     1219      | NOP ⇒
     1220        let ticks ≝ ticks_of_instruction (NOP ?) in
     1221         〈ticks, ticks〉
     1222      ]
     1223    | Comment comment ⇒ 〈0, 0〉
     1224    | Cost cost ⇒ 〈0, 0〉
     1225    | Jnz _ _ _ ⇒ ? (*CSC: To be implemented*)
     1226    | MovSuccessor _ _ _ ⇒ ? (*CSC: To be implemented *)
     1227    | Jmp jmp ⇒
     1228      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1229      let do_a_long ≝ policy ppc in
     1230      let lookup_address ≝ sigma (lookup_labels jmp) in
     1231      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1232        if sj_possible ∧ ¬ do_a_long then
     1233          〈2, 2〉 (* XXX: SJMP *)
     1234        else
     1235        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1236          if mj_possible ∧ ¬ do_a_long then
     1237            〈2, 2〉 (* XXX: AJMP *)
     1238          else
     1239            〈2, 2〉 (* XXX: LJMP *)
     1240    | Call call ⇒
     1241      (* XXX: collapse the branches as they are identical? *)
     1242      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1243      let lookup_address ≝ sigma (lookup_labels call) in
     1244      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1245      let do_a_long ≝ policy ppc in
     1246      if mj_possible ∧ ¬ do_a_long then
     1247        〈2, 2〉 (* ACALL *)
     1248      else
     1249        〈2, 2〉 (* LCALL *)
     1250    | Mov dptr tgt ⇒ 〈2, 2〉
     1251    ].
     1252cases daemon (*CSC: The three new pseudoinstruction cases*)
     1253qed.
     1254
     1255definition ticks_of:
     1256    ∀p:pseudo_assembly_program.
     1257    ∀sigma:Word → Word. ∀policy:Word → bool.
     1258     ∀ppc:Word.
     1259      nat_of_bitvector … ppc < |code p| → nat × nat ≝
     1260  λprogram: pseudo_assembly_program.
     1261  λsigma.
     1262  λpolicy.
     1263  λppc: Word. λppc_ok.
     1264    let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
     1265    let addr_of ≝ λid.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
     1266    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in
     1267     ticks_of0 program addr_of sigma policy ppc fetched.
  • src/ASM/AssemblyProof.ma

    r2516 r2899  
    4646  ]
    4747qed.
    48 
    49 definition ticks_of_instruction ≝
    50   λi.
    51     let trivial_code_memory ≝ assembly1 i in
    52     let trivial_status ≝ load_code_memory trivial_code_memory in
    53       \snd (fetch trivial_status (zero ?)).
    5448
    5549lemma fetch_assembly:
     
    146140  ∀sigma: Word → Word.
    147141  ∀policy: Word → bool.
    148   let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     142  let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
    149143  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    150144  ∀ppc.∀ppc_ok.
    151145  ∀code_memory.
    152   let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    153   let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
     146  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (preamble program)) x (zero 16) in
     147  let pi ≝  \fst  (fetch_pseudo_instruction (code program) ppc ppc_ok) in
    154148  let pc ≝ sigma ppc in
    155149  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     
    186180   sigma in the out-of-bounds region too. *)     
    187181lemma assembly_ok:
    188   ∀program.
    189   ∀length_proof: |\snd program| ≤ 2^16.
     182  ∀program: pseudo_assembly_program.
     183  ∀length_proof: |code program| ≤ 2^16.
    190184  ∀sigma: Word → Word.
    191185  ∀policy: Word → bool.
    192186  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    193   ∀assembled.
     187  ∀assembled: object_code.
    194188  ∀costs': BitVectorTrie costlabel 16.
    195   let 〈preamble, instr_list〉 ≝ program in
     189  let preamble ≝ preamble program in
     190  let instr_list ≝ code program in
    196191  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
    197192  let datalabels ≝ construct_datalabels preamble in
    198193  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
    199     〈assembled,costs'〉 = assembly program sigma policy →
     194    let loc ≝ pi1 … (assembly program sigma policy) in
     195    let assembled ≝ oc loc in
     196    let costs' ≝ costlabels loc in
    200197      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    201198        let code_memory ≝ load_code_memory assembled in
    202199        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    203200          ∀ppc.∀ppc_ok.
    204             let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
     201            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in     
    205202            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    206203            let pc ≝ sigma ppc in
     
    209206                  sigma newppc = add … pc (bitvector_of_nat … len).
    210207  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
    211   cases (assembly program sigma policy) * #assembled' #costs''
    212   @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
    213   cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
     208  cases (assembly program sigma policy) * #assembled' #costs'' #symbol_table #fpc #inj
     209  cut (|code program| ≤ 2^16) [ // ] #instr_list_ok
    214210  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
    215211  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
    216   * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
     212  * * #assembly_ok1 #assembly_ok3 #assembly_ok2
    217213  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
    218214  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     
    225221  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
    226222      >snd_fetch_pseudo_instruction
    227       cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
     223      cases sigma_policy_witness #_ #H cases (H ? ppc_ok) -H
    228224      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
    229225      >eq_fetch_pseudo_instruction whd in match instruction_size;
     
    261257lemma fetch_assembly_pseudo2:
    262258  ∀program.
    263   ∀length_proof: |\snd program| ≤ 2^16.
     259  ∀length_proof: |code program| ≤ 2^16.
    264260  ∀sigma.
    265261  ∀policy.
    266262  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    267263  ∀ppc.∀ppc_ok.
    268   let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    269   let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
     264  let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
     265  let res ≝ pi1 … (assembly program sigma policy) in
     266  let assembled ≝ oc res in
     267  let cost' ≝ costlabels res in
    270268  let code_memory ≝ load_code_memory assembled in
    271   let data_labels ≝ construct_datalabels (\fst program) in
     269  let data_labels ≝ construct_datalabels (preamble program) in
    272270  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    273271  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    274   let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
     272  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in
    275273  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    276274    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
    277   * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
     275  * #preamble #instr_list #code_size_ok #renamed_symbol #final_label
     276  #inj #well_labelled #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
    278277  @pair_elim #labels #costs #create_label_map_refl
    279   @pair_elim #assembled #costs' #assembled_refl
     278  letin res ≝ (assembly ???)
     279  letin assembled ≝ (oc ?)
     280  letin costs' ≝ (costlabels ?)
    280281  letin code_memory ≝ (load_code_memory ?)
    281282  letin data_labels ≝ (construct_datalabels ?)
    282283  letin lookup_labels ≝ (λx. ?)
    283284  letin lookup_datalabels ≝ (λx. ?)
    284   @pair_elim #pi #newppc #fetch_pseudo_refl
    285   lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
     285  lapply (assembly_ok ?? sigma policy sigma_policy_specification_witness assembled costs')
    286286  normalize nodelta try assumption
    287287  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
    288   lapply (H (sym_eq … assembled_refl)) -H
     288  lapply (H … ppc_ok) -H
     289  @pair_elim #pi #newppc #EQpi_neqppc
     290(*CSC: was working, to be repaired after change in datatypes representation
    289291  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
    290292  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
     
    295297  >EQ4 #H1 cases (H ppc_ok)
    296298  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
    297   >fetch_pseudo_refl in H1; #assm @assm assumption
     299  >fetch_pseudo_refl in H1; #assm @assm assumption *) cases daemon
    298300qed.
    299301
     
    740742    | Cost _ ⇒ Some … M
    741743    | Jmp _ ⇒ Some … M
     744    | Jnz _ _ _ ⇒ Some … M
     745    | MovSuccessor _ _ _ ⇒ ? (*CSC: TO BE IMPLEMENTED*)
    742746    | Call a ⇒
    743747      let a' ≝ addr_of a s in
     
    789793           None ?
    790794       | JC addr1 ⇒ Some ? M
     795       | JMP _ ⇒ ? (*CSC: TO BE IMPLEMENTED*)
    791796       | JNC addr1 ⇒ Some ? M
    792797       | JB addr1 addr2 ⇒ Some ? M
     
    12631268(* XXX: check values returned for conditional jumps below! They are wrong,
    12641269        find correct values *)
    1265 definition ticks_of0:
    1266     ∀p:pseudo_assembly_program.
    1267       (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
    1268   λprogram: pseudo_assembly_program.
    1269   λlookup_labels: Identifier → Word.
    1270   λsigma.
    1271   λpolicy.
    1272   λppc: Word.
    1273   λfetched.
    1274     match fetched with
    1275     [ Instruction instr ⇒
    1276       match instr with
    1277       [ JC lbl ⇒
    1278         let lookup_address ≝ sigma (lookup_labels lbl) in
    1279         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1280         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1281           if sj_possible then
    1282             〈2, 2〉
    1283           else
    1284             〈4, 4〉
    1285       | JNC lbl ⇒
    1286         let lookup_address ≝ sigma (lookup_labels lbl) in
    1287         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1288         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1289           if sj_possible then
    1290             〈2, 2〉
    1291           else
    1292             〈4, 4〉
    1293       | JB bit lbl ⇒
    1294         let lookup_address ≝ sigma (lookup_labels lbl) in
    1295         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1296         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1297           if sj_possible then
    1298             〈2, 2〉
    1299           else
    1300             〈4, 4〉
    1301       | JNB bit lbl ⇒
    1302         let lookup_address ≝ sigma (lookup_labels lbl) in
    1303         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1304         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1305           if sj_possible then
    1306             〈2, 2〉
    1307           else
    1308             〈4, 4〉
    1309       | JBC bit lbl ⇒
    1310         let lookup_address ≝ sigma (lookup_labels lbl) in
    1311         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1312         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1313           if sj_possible then
    1314             〈2, 2〉
    1315           else
    1316             〈4, 4〉
    1317       | JZ lbl ⇒
    1318         let lookup_address ≝ sigma (lookup_labels lbl) in
    1319         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1320         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1321           if sj_possible then
    1322             〈2, 2〉
    1323           else
    1324             〈4, 4〉
    1325       | JNZ lbl ⇒
    1326         let lookup_address ≝ sigma (lookup_labels lbl) in
    1327         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1328         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1329           if sj_possible then
    1330             〈2, 2〉
    1331           else
    1332             〈4, 4〉
    1333       | CJNE arg lbl ⇒
    1334         let lookup_address ≝ sigma (lookup_labels lbl) in
    1335         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1336         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1337           if sj_possible then
    1338             〈2, 2〉
    1339           else
    1340             〈4, 4〉
    1341       | DJNZ arg lbl ⇒
    1342         let lookup_address ≝ sigma (lookup_labels lbl) in
    1343         let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1344         let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1345           if sj_possible then
    1346             〈2, 2〉
    1347           else
    1348             〈4, 4〉
    1349       | ADD arg1 arg2 ⇒
    1350         let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
    1351          〈ticks, ticks〉
    1352       | ADDC arg1 arg2 ⇒
    1353         let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
    1354          〈ticks, ticks〉
    1355       | SUBB arg1 arg2 ⇒
    1356         let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
    1357          〈ticks, ticks〉
    1358       | INC arg ⇒
    1359         let ticks ≝ ticks_of_instruction (INC ? arg) in
    1360          〈ticks, ticks〉
    1361       | DEC arg ⇒
    1362         let ticks ≝ ticks_of_instruction (DEC ? arg) in
    1363          〈ticks, ticks〉
    1364       | MUL arg1 arg2 ⇒
    1365         let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
    1366          〈ticks, ticks〉
    1367       | DIV arg1 arg2 ⇒
    1368         let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
    1369          〈ticks, ticks〉
    1370       | DA arg ⇒
    1371         let ticks ≝ ticks_of_instruction (DA ? arg) in
    1372          〈ticks, ticks〉
    1373       | ANL arg ⇒
    1374         let ticks ≝ ticks_of_instruction (ANL ? arg) in
    1375          〈ticks, ticks〉
    1376       | ORL arg ⇒
    1377         let ticks ≝ ticks_of_instruction (ORL ? arg) in
    1378          〈ticks, ticks〉
    1379       | XRL arg ⇒
    1380         let ticks ≝ ticks_of_instruction (XRL ? arg) in
    1381          〈ticks, ticks〉
    1382       | CLR arg ⇒
    1383         let ticks ≝ ticks_of_instruction (CLR ? arg) in
    1384          〈ticks, ticks〉
    1385       | CPL arg ⇒
    1386         let ticks ≝ ticks_of_instruction (CPL ? arg) in
    1387          〈ticks, ticks〉
    1388       | RL arg ⇒
    1389         let ticks ≝ ticks_of_instruction (RL ? arg) in
    1390          〈ticks, ticks〉
    1391       | RLC arg ⇒
    1392         let ticks ≝ ticks_of_instruction (RLC ? arg) in
    1393          〈ticks, ticks〉
    1394       | RR arg ⇒
    1395         let ticks ≝ ticks_of_instruction (RR ? arg) in
    1396          〈ticks, ticks〉
    1397       | RRC arg ⇒
    1398         let ticks ≝ ticks_of_instruction (RRC ? arg) in
    1399          〈ticks, ticks〉
    1400       | SWAP arg ⇒
    1401         let ticks ≝ ticks_of_instruction (SWAP ? arg) in
    1402          〈ticks, ticks〉
    1403       | MOV arg ⇒
    1404         let ticks ≝ ticks_of_instruction (MOV ? arg) in
    1405          〈ticks, ticks〉
    1406       | MOVX arg ⇒
    1407         let ticks ≝ ticks_of_instruction (MOVX ? arg) in
    1408          〈ticks, ticks〉
    1409       | SETB arg ⇒
    1410         let ticks ≝ ticks_of_instruction (SETB ? arg) in
    1411          〈ticks, ticks〉
    1412       | PUSH arg ⇒
    1413         let ticks ≝ ticks_of_instruction (PUSH ? arg) in
    1414          〈ticks, ticks〉
    1415       | POP arg ⇒
    1416         let ticks ≝ ticks_of_instruction (POP ? arg) in
    1417          〈ticks, ticks〉
    1418       | XCH arg1 arg2 ⇒
    1419         let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
    1420          〈ticks, ticks〉
    1421       | XCHD arg1 arg2 ⇒
    1422         let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
    1423          〈ticks, ticks〉
    1424       | RET ⇒
    1425         let ticks ≝ ticks_of_instruction (RET ?) in
    1426          〈ticks, ticks〉
    1427       | RETI ⇒
    1428         let ticks ≝ ticks_of_instruction (RETI ?) in
    1429          〈ticks, ticks〉
    1430       | NOP ⇒
    1431         let ticks ≝ ticks_of_instruction (NOP ?) in
    1432          〈ticks, ticks〉
    1433       ]
    1434     | Comment comment ⇒ 〈0, 0〉
    1435     | Cost cost ⇒ 〈0, 0〉
    1436     | Jmp jmp ⇒
    1437       let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1438       let do_a_long ≝ policy ppc in
    1439       let lookup_address ≝ sigma (lookup_labels jmp) in
    1440       let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    1441         if sj_possible ∧ ¬ do_a_long then
    1442           〈2, 2〉 (* XXX: SJMP *)
    1443         else
    1444         let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    1445           if mj_possible ∧ ¬ do_a_long then
    1446             〈2, 2〉 (* XXX: AJMP *)
    1447           else
    1448             〈2, 2〉 (* XXX: LJMP *)
    1449     | Call call ⇒
    1450       (* XXX: collapse the branches as they are identical? *)
    1451       let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    1452       let lookup_address ≝ sigma (lookup_labels call) in
    1453       let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    1454       let do_a_long ≝ policy ppc in
    1455       if mj_possible ∧ ¬ do_a_long then
    1456         〈2, 2〉 (* ACALL *)
    1457       else
    1458         〈2, 2〉 (* LCALL *)
    1459     | Mov dptr tgt ⇒ 〈2, 2〉
    1460     ].
    1461 
    1462 definition ticks_of:
    1463     ∀p:pseudo_assembly_program.
    1464       (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
    1465        nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
    1466   λprogram: pseudo_assembly_program.
    1467   λlookup_labels.
    1468   λsigma.
    1469   λpolicy.
    1470   λppc: Word. λppc_ok.
    1471     let pseudo ≝ \snd program in
    1472     let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
    1473      ticks_of0 program lookup_labels sigma policy ppc fetched.
    14741270
    14751271(*
  • src/ASM/AssemblyProofSplitSplit.ma

    r2278 r2899  
    4545      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    4646        status_of_pseudo_status M' …
    47           (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
     47          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
    4848    #M #M' * #preamble #instr_list #program_in_bounds
    4949    @pair_elim #labels #cost #create_label_cost_refl
  • src/ASM/CostsProof.ma

    r2760 r2899  
    1313   (trace_ends_flag: trace_ends_with_ret)
    1414    (start_status: Status cm) (final_status: Status cm)
    15       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     15      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    1616        start_status final_status) on the_trace: nat ≝
    1717  match the_trace with
     
    2424  (trace_ends_flag: trace_ends_with_ret)
    2525   (start_status: Status cm) (final_status: Status cm)
    26      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     26     (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    2727       on the_trace: nat ≝
    2828  match the_trace with
     
    5555  (cost_labels: BitVectorTrie costlabel 16)
    5656  (start_status: Status cm) (final_status: Status cm)
    57     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     57    (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
    5858      on the_trace: nat ≝
    5959  match the_trace with
     
    7272   (trace_ends_flag: trace_ends_with_ret)
    7373    (start_status: Status cm) (final_status: Status cm)
    74       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     74      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    7575        start_status final_status) on the_trace:
    7676          clock … cm … final_status = (compute_max_trace_label_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ?
     
    8080  (trace_ends_flag: trace_ends_with_ret)
    8181   (start_status: Status cm) (final_status: Status cm)
    82      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     82     (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    8383       on the_trace:
    8484         clock … cm … final_status = (compute_max_trace_any_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ?
     
    8787  (cost_labels: BitVectorTrie costlabel 16)
    8888  (start_status: Status cm) (final_status: Status cm)
    89     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     89    (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
    9090      on the_trace:
    9191        clock … cm … final_status = (compute_max_trace_label_return_cost cm cost_labels start_status final_status the_trace) + clock … cm … start_status ≝ ?.
     
    178178   (trace_ends_flag: trace_ends_with_ret)
    179179    (start_status: Status cm) (final_status: Status cm)
    180       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     180      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    181181        start_status final_status) on the_trace: nat ≝
    182182  match the_trace with
     
    190190  (trace_ends_flag: trace_ends_with_ret)
    191191   (start_status: Status cm) (final_status: Status cm)
    192      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     192     (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    193193       on the_trace: nat ≝
    194194  match the_trace with
     
    212212  (cost_labels: BitVectorTrie costlabel 16)
    213213  (start_status: Status cm) (final_status: Status cm)
    214     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     214    (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
    215215      on the_trace: nat ≝
    216216  match the_trace with
     
    227227   (trace_ends_flag: trace_ends_with_ret)
    228228    (start_status: Status cm) (final_status: Status cm)
    229       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     229      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    230230        start_status final_status) on the_trace:
    231231 compute_trace_label_label_cost_using_paid cm cost_labels … the_trace =
     
    236236  (trace_ends_flag: trace_ends_with_ret)
    237237   (start_status: Status cm) (final_status: Status cm)
    238      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels)
     238     (the_trace: trace_any_label (OC_abstract_status cm cost_labels)
    239239      trace_ends_flag start_status final_status) on the_trace:     
    240240  compute_paid_trace_any_label cm cost_labels trace_ends_flag … the_trace
     
    245245  (cost_labels: BitVectorTrie costlabel 16)
    246246  (start_status: Status cm) (final_status: Status cm)
    247     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels)
     247    (the_trace: trace_label_return (OC_abstract_status cm cost_labels)
    248248     start_status final_status) on the_trace:
    249249 compute_trace_label_return_cost_using_paid cm cost_labels … the_trace =
     
    456456 (cost_map: identifier_map CostTag nat)
    457457 (initial: Status cm) (final: Status cm)
    458  (trace: trace_label_return (ASM_abstract_status cm cost_labels) initial final)
     458 (trace: trace_label_return (OC_abstract_status cm cost_labels) initial final)
    459459 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    460460 on trace:
     
    462462 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    463463   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    464   let ctrace ≝ flatten_trace_label_return (ASM_abstract_status cm cost_labels) … trace in
     464  let ctrace ≝ flatten_trace_label_return (OC_abstract_status cm cost_labels) … trace in
    465465  compute_trace_label_return_cost_using_paid cm … trace =
    466466   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     
    471471 (cost_map: identifier_map CostTag nat)
    472472 (initial: Status cm) (final: Status cm)
    473  (trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
     473 (trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
    474474 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    475475 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
     
    477477 on trace:
    478478  ∀unrepeating_witness: tal_unrepeating … trace.
    479   let ctrace ≝ flatten_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in
     479  let ctrace ≝ flatten_trace_any_label (OC_abstract_status cm cost_labels) … trace_ends_flag … trace in
    480480  compute_trace_any_label_cost_using_paid … trace =
    481481   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     
    486486 (cost_map: identifier_map CostTag nat)
    487487 (initial: Status cm) (final: Status cm)
    488  (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
     488 (trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
    489489 (unrepeating_witness: tll_unrepeating … trace)
    490490 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
     
    493493 on trace:
    494494 ∀unrepeating_witness: tll_unrepeating … trace.
    495   let ctrace ≝ flatten_trace_label_label (ASM_abstract_status cm cost_labels) … trace in
     495  let ctrace ≝ flatten_trace_label_label (OC_abstract_status cm cost_labels) … trace in
    496496  compute_trace_label_label_cost_using_paid … trace =
    497497   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     
    631631  ∀initial: Status code_memory.
    632632  ∀final: Status code_memory.
    633   ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     633  ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
    634634  ∀unrepeating_witness: tlr_unrepeating … trace.
    635635  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     
    654654  ∀initial: Status code_memory.
    655655  ∀final: Status code_memory.
    656   ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     656  ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
    657657  ∀unrepeating_witness: tlr_unrepeating … trace.
    658658    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
     
    687687  =
    688688   lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective)
    689    (as_cost_get_label (ASM_abstract_status (load_code_memory ccode1) ccode2)
     689   (as_cost_get_label (OC_abstract_status (load_code_memory ccode1) ccode2)
    690690    «tl,Htl») PRF2.
    691691//
  • src/ASM/Interpret.ma

    r2770 r2899  
    11791179        program_counter ? cm (execute_1 cm s) =
    11801180          program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))).
    1181 (*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
     1181(*    (OC_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
    11821182  #cm #s normalize nodelta
    11831183  whd in match execute_1; normalize nodelta @pi2
  • src/ASM/Interpret2.ma

    r2875 r2899  
    4242  mk_preclassified_system_of_abstract_status
    4343   labelled_object_code
    44    (ASM_abstract_status cm (costlabels c))
     44   (OC_abstract_status cm (costlabels c))
    4545   (λst. return (execute_1 … st))
    4646   (initialise_status … cm).
     47
     48(* Pre-classified system for ASM *)
     49
     50include "ASM/Assembly.ma".
     51
     52(* Move next function in interpret? *)
     53definition execute_1_pseudo_instruction':
     54 ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
     55 λcm,sigma,policy,status.
     56  execute_1_pseudo_instruction cm
     57   (ticks_of cm  sigma policy) status ….
     58cases daemon (*CSC: we need to prove that we remain inside the program
     59 (code closed), which is impossible in case of function pointers.
     60 But the type does not allow to fail (yet?) *)
     61qed.
     62
     63definition classify_pseudo_instruction: pseudo_instruction → status_class ≝
     64 λinstr.
     65  match instr with
     66  [ Instruction pre ⇒ ASM_classify00 … pre
     67  | Comment _ ⇒ cl_other
     68  | Cost _ ⇒ cl_other
     69  | Jmp _ ⇒ cl_other
     70  | Jnz _ _ _ ⇒ cl_jump
     71  | MovSuccessor _ _ _ ⇒ cl_other
     72  | Call _ ⇒ cl_call
     73  | Mov _ _ ⇒ cl_other ].
     74
     75definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
     76λcm,s.
     77 classify_pseudo_instruction
     78  (\fst (fetch_pseudo_instruction (code cm) (program_counter … s) ?)).
     79cases daemon (*CSC: again*)
     80qed.
     81
     82definition ASM_next_instruction_properly_relates_program_counters ≝
     83  λcm.
     84  λbefore: PseudoStatus cm.
     85  λafter : PseudoStatus cm.
     86    let 〈instruction, program_counter_after〉 ≝
     87     fetch_pseudo_instruction (code cm) (program_counter … before) ?
     88    in
     89     program_counter ?? after = program_counter_after.
     90cases daemon (*CSC: again*)
     91qed.
     92
     93definition ASM_as_label_of_pc:
     94 ∀prog:pseudo_assembly_program. Word → option costlabel
     95
     96 λprog,pc.
     97 match \fst (fetch_pseudo_instruction (code prog) pc ?) with
     98 [ Cost label ⇒ Some … label
     99 | _ ⇒ None ? ].
     100cases daemon (*CSC: again*)
     101qed.
     102
     103definition ASM_abstract_status:
     104 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
     105  λprog,sigma,policy.
     106    mk_abstract_status
     107      (PseudoStatus prog)
     108      (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2)
     109      word_deqset
     110      (program_counter …)
     111      (ASM_classify …)
     112      (ASM_as_label_of_pc prog …)
     113      (ASM_next_instruction_properly_relates_program_counters prog)
     114      ? (* (λs.False) *)
     115      ?
     116      ?.
     117  #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
     118qed.
     119
     120definition ASM_preclassified_system:
     121 pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
     122 λc,sigma,policy.
     123  mk_preclassified_system_of_abstract_status
     124   pseudo_assembly_program
     125   (ASM_abstract_status c sigma policy)
     126   (λst. return (execute_1_pseudo_instruction' … sigma policy st))
     127   (initialise_status … c).
  • src/compiler.ma

    r2875 r2899  
    5151  | ltl_pass ⇒ with_stack_model ltl_program
    5252  | lin_pass ⇒ with_stack_model lin_program
    53   | assembly_pass ⇒ pseudo_assembly_program
     53  | assembly_pass ⇒
     54     pseudo_assembly_program × (Word → Word) × (Word → bool)
    5455  | object_code_pass ⇒ labelled_object_code ].
    5556
     
    114115  let i ≝ observe lin_pass 〈p,st〉 in
    115116   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
    116   let i ≝ observe assembly_pass p in
    117117   return 〈p,stack_cost,max_stack〉.
    118118
     
    126126  let sigma ≝ λppc. \fst sigma_pol ppc in
    127127  let pol ≝ λppc. \snd sigma_pol ppc in
     128  let i ≝ observe assembly_pass 〈p,sigma,pol〉 in
    128129  let p ≝ assembly p sigma pol in
    129130  let i ≝ observe object_code_pass p in
     
    135136definition lift_cost_map_back_to_front :
    136137  ∀clight, code_memory, lbls.
    137     let abstat ≝ ASM_abstract_status code_memory lbls in
     138    let abstat ≝ OC_abstract_status code_memory lbls in
    138139  as_cost_map abstat → clight_cost_map clight ≝
    139140  λclight,code_memory,lbls,k,asm_cost_map.
  • src/semantics.ma

    r2875 r2899  
    3939     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
    4040  | assembly_pass ⇒
    41      ?
     41     λprog. let 〈code,sigma,policy〉 ≝ prog in
     42      mk_preclassified_system_pass … (ASM_preclassified_system prog sigma policy) …
    4243  | object_code_pass ⇒
    4344     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
    4445  ].
    45 try % cases daemon
     46%
    4647qed.
    4748
Note: See TracChangeset for help on using the changeset viewer.