Changeset 1309 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Oct 6, 2011, 6:09:18 PM (8 years ago)
Author:
boender
Message:
  • refounded JEP
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1103 r1309  
    408408qed.
    409409
    410 definition is_relative_jump ≝
    411   λi: preinstruction Identifier.
    412   match i with
    413   [ JC _ ⇒ True
    414   | JNC _ ⇒ True
    415   | JB _ _ ⇒ True
    416   | JNB _ _ ⇒ True
    417   | JBC _ _ ⇒ True
    418   | JZ _ ⇒ True
    419   | JNZ _ ⇒ True
    420   | CJNE _ _ ⇒ True
    421   | DJNZ _ _ ⇒ True
    422   | _ ⇒ False
    423   ].
    424 
    425 definition pseudo_instruction_is_relative_jump: pseudo_instruction → Prop ≝
    426  λi.
    427   match i with
    428    [ Instruction j ⇒ is_relative_jump j
    429    | _ ⇒ False ].
    430 
    431410inductive jump_length: Type[0] ≝
    432411  | short_jump: jump_length
     
    434413  | long_jump: jump_length.
    435414
    436 definition find_right_call: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝
    437  (* medium call: 11 bits, only in "current segment" *)
    438  (* can this be done more efficiently with bit vector arithmetic? *)
    439  λpc.λaddress.
    440   let 〈a1, a2〉 ≝ split ? 5 11 address in
    441   let 〈p1, p2〉 ≝ split ? 5 11 pc in
    442    if eq_bv ? a1 p1 then (* we're in the same segment *)
    443     〈2, 2, address, Some ? medium_jump〉
    444    else
    445     〈2, 3, address, Some ? long_jump〉.
    446    
    447 (* lemma frc_ok:
    448   ∀pc.∀j_addr.
    449   let 〈i1,i2,addr,jl〉 ≝ find_right_call pc j_addr in
    450   addr = j_addr ∧
    451   match jl with
    452   [ None ⇒ False (* doesn't happen *)
    453   | Some j ⇒ match j with
    454     [ short_jump ⇒ False (* doesn't happen either *)
    455     | medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc)
    456     | long_jump ⇒ True
    457     ]
    458   ].
    459  #pc #j_addr whd in match (find_right_call pc j_addr) cases (split ????) cases (split ????)
    460  #p1 #p2 #a1 #a2 normalize nodelta
    461  lapply (refl ? (eq_bv 5 a1 p1)) cases (eq_bv 5 a1 p1) in ⊢ (???% → %) #H normalize
    462  [ %1 [ @refl | @(eq_bv_eq … H) ]
    463  | %1 [ @refl | // ] ]
    464 qed. *)
    465        
    466 definition distance ≝
    467  λx.λy.if gtb x y then x - y else y - x.
    468  
    469 definition find_right_jump: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝
    470  (* short jump: 8 bits signed *)
    471  (* medium jump: 11 bits, forward only *)
    472  λpc.λaddress.
    473   let pn ≝ nat_of_bitvector ? pc in
    474   let pa ≝ nat_of_bitvector ? address in
    475    if ltb (distance pn pa) 127 then
    476     〈2, 2, address, Some ? short_jump〉
    477    else
    478     find_right_call pc address.
    479 
    480 (* lemma frj_ok:
    481   ∀pc.∀j_addr.
    482   let 〈i1,i2,addr,jl〉 ≝ find_right_jump pc j_addr in
    483   addr = j_addr ∧
    484   match jl with
    485   [ None ⇒ False (* doesn't happen *)
    486   | Some j ⇒ match j with
    487     [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? j_addr) < 127
    488     | medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc)
    489     | long_jump ⇒ True
    490     ]
    491   ].
    492  #pc #j_addr whd in match (find_right_jump pc j_addr)
    493  lapply (refl ? (ltb (distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 j_addr)) 127))
    494  cases (ltb (distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 j_addr)) 127) in ⊢ (???% → %) #H
    495  normalize nodelta
    496  [ %1 [ @refl | whd @(leb_true_to_le … H) ]
    497  | lapply (frc_ok pc j_addr) cases (find_right_call ??) normalize nodelta #x #y cases x
    498  #i1 #i2 cases y #addr #jl normalize nodelta cases jl normalize
    499    [ //
    500    | #jl cases jl normalize
    501      [1: #f @⊥ @(proj2 ? ? f) |2,3: // ]
    502    ]
    503   ]
    504 qed. *)
    505    
    506 definition find_right_relative_jump: Word → (BitVectorTrie (Word × Identifier) 16) →
    507  Identifier → (nat × nat) × (Word × (option jump_length)) ≝
    508  λpc.λlabels.λjmp.
    509  match lookup_opt ? ? jmp labels with
    510  [ None ⇒ 〈2, 2, pc, Some ? short_jump〉
    511  | Some x ⇒ let 〈ignore, a〉 ≝ x in find_right_jump pc a ].
    512  
    513 (* lemma frrj_ok:
    514   ∀pc.∀labels.∀j_id.
    515   let 〈i1,i2,addr,jl〉 ≝ find_right_relative_jump pc labels j_id in
    516   match lookup_opt ? ? j_id labels with
    517   [ None ⇒ True (* long jump *)
    518   | Some x ⇒ let 〈ignore,j_addr〉 ≝ x in addr = j_addr ∧ match jl with
    519     [ None ⇒ False (* doesn't happen *)
    520     | Some j ⇒ match j with
    521       [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? j_addr) < 127
    522       | medium_jump ⇒ \fst (split ? 5 11 j_addr) = \fst (split ? 5 11 pc)
    523       | long_jump ⇒ True
    524       ]
    525     ]
    526   ].
    527  #pc #labels #j_id whd in match (find_right_relative_jump pc labels j_id)
    528  cases (lookup_opt ? ? j_id labels) normalize nodelta
    529  [ //
    530  | #x cases x #y #j_addr -x; normalize nodelta lapply (frj_ok pc j_addr)
    531    cases (find_right_jump ??) #x cases x #i1 #i2 -x #x cases x #i3 #z -x; cases z
    532    normalize nodelta
    533    [ //
    534    | #jl cases jl normalize nodelta
    535      [1,3: // |2: #H @H ]
    536    ]
    537  ]
    538 qed. *)
    539      
    540 definition jep_relative: Word → (BitVectorTrie (Word × Identifier) 16) → preinstruction Identifier → ? ≝
    541  λpc.λlabels.λi.
    542   match i with
    543   [ JC jmp ⇒ find_right_relative_jump pc labels jmp
    544   | JNC jmp ⇒ find_right_relative_jump pc labels jmp
    545   | JB baddr jmp ⇒ find_right_relative_jump pc labels jmp
    546   | JZ jmp ⇒ find_right_relative_jump pc labels jmp
    547   | JNZ jmp ⇒ find_right_relative_jump pc labels jmp
    548   | JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp
    549   | JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp
    550   | CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp
    551   | DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp
    552   | _ ⇒ let l ≝ length ? (assembly_preinstruction ? (λx.zero ?) i) in
    553          〈l, l, pc, None …〉 ].
    554 
    555 definition is_long_jump ≝
    556  λj.match j with
    557  [ long_jump ⇒ true
    558  | _         ⇒ false
    559  ].
    560 
    561 definition policy_safe ≝
    562  (λ_:Word.λx:Word×Word×jump_length.let 〈pc,addr,j〉 ≝ x in
    563    match j with
    564    [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? addr) < 127
    565    | medium_jump ⇒ \fst (split ? 5 11 addr) = \fst (split ? 5 11 pc)
    566    | long_jump ⇒ True
    567    ]
    568   ).
    569 
    570 definition jump_expansion_policy ≝
    571   Σpolicy:BitVectorTrie (Word × Word × jump_length) 16.
    572     forall ? ? policy policy_safe.
    573  
    574 definition inject_jump_expansion_policy:
    575  ∀p:BitVectorTrie (Word × Word × jump_length) 16.
    576   forall ? ? p policy_safe → jump_expansion_policy ≝ inject ….
    577  
    578 coercion inject_jump_expansion_policy:
    579  ∀p:BitVectorTrie (Word × Word × jump_length) 16.
    580   forall ? ? p policy_safe → jump_expansion_policy ≝ inject_jump_expansion_policy
    581  on p:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy.
    582  
    583 (* the jump length in a is greater than or equal to the jump length in b *)
    584 definition jump_length_decrease ≝
    585  λa:jump_length.λb:jump_length.
    586  match a with
    587  [ short_jump ⇒ b = short_jump
    588  | medium_jump ⇒ b = short_jump ∨ b = medium_jump
    589  | long_jump ⇒ True
    590  ].
    591 
    592 definition jump_expansion_policy_internal: pseudo_assembly_program →
    593  (BitVectorTrie (Word × Identifier) 16) → jump_expansion_policy →
    594  Σres:(BitVectorTrie (Word × Identifier) 16) × (BitVectorTrie (Word × Word × jump_length) 16).
    595   let 〈x,p〉 ≝ res in
    596   True ≝
    597  λprogram.λold_labels.λold_policy.
    598    let res ≝
    599    foldl_strong (option Identifier × pseudo_instruction)
    600     (λprefix.Σres.True)
    601     (\snd program)
    602     (λprefix.λi.λtl.λprf.λacc.   
    603      let 〈label, instr〉 ≝ i in
    604      let 〈pc,orig_pc,labels,policy〉 ≝ acc in
    605      let new_labels ≝ match label return λ_.(BitVectorTrie (Word × Identifier) 16) with
    606       [ None ⇒ labels
    607       | Some l ⇒ insert ? ? orig_pc 〈pc,l〉 labels
    608       ] in
    609      let add_instr ≝ match instr with
    610       [ Call c ⇒
    611         match lookup_opt ? ? c new_labels with
    612          [ None   ⇒ 〈2, 2, pc, Some ? short_jump〉
    613          | Some x ⇒ let 〈ignore,c_addr〉 ≝ x in find_right_call pc c_addr ]
    614       | Jmp j ⇒
    615         match lookup_opt ? ? j new_labels with
    616          [ None   ⇒ 〈2, 2, pc, Some ? short_jump〉
    617          | Some x ⇒ let 〈ignore,j_addr〉 ≝ x in find_right_jump pc j_addr ]
    618       | Instruction i ⇒ jep_relative pc new_labels i
    619       | Mov _ _ ⇒ 〈3, 3, pc, None …〉
    620       | Cost _ ⇒ 〈0, 0, pc, None …〉
    621       | Comment _ ⇒ 〈0, 0, pc, None …〉 ] in
    622      let 〈pc_delta, orig_pc_delta, addr, jmp_len〉 ≝ add_instr in
    623      let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    624      let 〈new_orig_pc,ignore〉 ≝ add_16_with_carry orig_pc (bitvector_of_nat ? orig_pc_delta) false in
    625      match jmp_len with
    626       [ None   ⇒ 〈new_pc, orig_pc, new_labels, policy〉
    627       | Some j ⇒ 〈new_pc, new_orig_pc, new_labels, insert ? ? orig_pc 〈pc, addr, j〉 policy〉
    628       ]
    629     ) 〈zero ?, zero ?, old_labels, eject … old_policy〉 in
    630    let 〈npc, norig_pc, nlabels, npolicy〉 ≝ res in
    631    〈nlabels, npolicy〉.
    632    //.
    633 (* [ cases res in p -res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb;
    634      >Hb in Ha; normalize nodelta #H @H
    635    | generalize in match (sig2 … acc) >p1 >p2 >p3 #H
    636      @(forall_insert … H)  normalize nodelta normalize nodelta in p4; cases instr in p4; >p5 >p6 normalize nodelta
    637      [5: #str >p9 #Heq cases (lookup_opt ? ? str ?) in Heq; normalize nodelta
    638          [ #Heq2 lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
    639            #Heq3 destruct (Heq3) //
    640          | #x cases x -x #i0 #c_addr normalize nodelta lapply (frc_ok pc c_addr)
    641            cases (find_right_call pc c_addr) #x #y cases x #i0 #i1 -x; cases y #ad #jmp -y;
    642            normalize nodelta #Heq #Heq2
    643            >(proj1 ? ? Heq) in Heq2; #Heq2
    644            <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
    645            >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq;
    646            cases j normalize nodelta #Heq [ @⊥ ] @(proj2 ? ? Heq)
    647          ]
    648     |2,3,6: [3: #x] #z >p9 #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
    649        #ctd destruct (ctd)
    650     |1,4:
    651       #pi
    652        [1: cases label normalize nodelta [ #Hjep | #id #Hjep ] whd in Hjep: (??%??); cases pi in Hjep;
    653        |2: cases (lookup_opt ? ? pi ?) normalize nodelta >p9
    654            [ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
    655              #ctd destruct (ctd) //
    656            | #x cases x -x #i0 #j_addr normalize nodelta lapply (frj_ok pc j_addr)
    657              cases (find_right_jump pc j_addr) #x #y cases x #i0 #i1 -x; cases y #ad #jump -y;
    658              normalize nodelta #Heq #Heq2
    659              >(proj1 ? ? Heq) in Heq2; #Heq2
    660              <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
    661              >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq;
    662              cases j normalize nodelta #Heq @(proj2 ? ? Heq)
    663            ]
    664        ]
    665        [1,2,3,6,7,33,34,38,39,40,43,44,70,71: #acc #x normalize nodelta #Heq
    666          <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
    667          #ctd destruct (ctd)
    668        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
    669          #acc normalize nodelta #Heq
    670          <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
    671          #ctd destruct (ctd)
    672        |35,36,37,72,73,74: normalize nodelta #Heq
    673          <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
    674          #ctd destruct (ctd)
    675        |9,10,14,15: #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id)
    676            whd in match (find_right_relative_jump pc labels j_id)
    677           normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta
    678           [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
    679              #Heq2 destruct (Heq2) //
    680           |2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
    681             normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
    682           ]
    683        |46,47,51,52: #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id)
    684           whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id)
    685           normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta
    686           [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
    687              #Heq2 destruct (Heq2) //
    688           |2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
    689             normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
    690           ]
    691        |11,12,13,16,17: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id)
    692           whd in match (find_right_relative_jump pc labels j_id)
    693           normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta
    694           [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
    695              #Heq2 destruct (Heq2) //
    696           |2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
    697             normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
    698           ]
    699        |48,49,50,53,54: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id)
    700           whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id)
    701           normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta
    702           [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
    703              #Heq2 destruct (Heq2) //
    704           |2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
    705             normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
    706           ]
    707        ]
    708      ]
    709    | generalize in match (sig2 … acc) >p1 >p2 >p3 #H
    710      @H
    711    | generalize in match (sig2 … old_policy) #H @H
    712    ] *)
    713 qed.
    714 
    715 (* lemma short_jumps_ok:
    716   ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy.
    717   forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p))
    718     (λk.λx.let 〈pc,addr,j〉 ≝ x in
    719       j = short_jump →
    720       distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127).
    721  #program #l #p @lookup_forall
    722   #x #b cases x -x #x cases x #pc #addr #j #Hl normalize nodelta
    723   cases j in Hl; #Hl #Hj
    724   [2,3: destruct (Hj)
    725   |-Hj; cases (jump_expansion_policy_internal program l p) in Hl;
    726     #res cases res -res #r #res normalize nodelta #Hf #Hl
    727     normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl)
    728     normalize #H @H
    729   ]   
    730 qed. *)
    731 
    732 (* lemma medium_jumps_ok:
    733   ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy.
    734   forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p))
    735     (λk.λx.let 〈pc,addr,j〉 ≝ x in
    736       j = medium_jump →
    737       distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127).
    738  #program #l #p @lookup_forall
    739   #x #b cases x -x #x cases x #pc #addr #j #Hl normalize nodelta
    740   cases j in Hl; #Hl #Hj
    741   [2,3: destruct (Hj)
    742   |-Hj; cases (jump_expansion_policy_internal program l p) in Hl;
    743     #res cases res -res #r #res normalize nodelta #Hf #Hl
    744     normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl)
    745     normalize #H @H
    746   ]   
    747 qed. *)
    748      
     415(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
     416definition jump_expansion_policy ≝ BitVectorTrie (Word × jump_length) 16.
     417
    749418definition expand_relative_jump_internal:
    750419 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
     
    819488  ].
    820489
    821 definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
     490definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
    822491  λlookup_labels.
    823492  λlookup_datalabels.
     
    875544qed.
    876545
    877 let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program)
    878  (old_labels: BitVectorTrie (Word × Identifier) 16)
    879  (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16.
    880    forall ? ? bla policy_safe)
    881  on n: BitVectorTrie jump_length 16 ≝
    882  match n with
    883  [ O ⇒ fold …
    884    (λ_.λx.λacc.let 〈pc,i2,jmp_len〉 ≝ x in insert … pc jmp_len acc)
    885    old_policy (Stub ? ?)
    886  | S n' ⇒
    887     jump_expansion_internal n' program
    888     (\fst (jump_expansion_policy_internal program old_labels old_policy))
    889     (\snd (jump_expansion_policy_internal program old_labels old_policy))
    890  ].
    891  generalize in match (sig2 … (jump_expansion_policy_internal program old_labels old_policy))
    892  cases (jump_expansion_policy_internal program old_labels old_policy)
    893  #a cases a #xx #pp normalize nodelta
    894  #H #H2 normalize nodelta @H2
    895 qed.
    896 
    897 
    898 
     546(* label_trie: identifier ↦ 〈instruction number, address〉 *)
     547definition label_trie ≝ BitVectorTrie (nat × Word) 16.
     548
     549definition add_instruction_size: Word → jump_length → pseudo_instruction → Word ≝
     550  λpc.λjmp_len.λinstr.
     551  let ilist ≝ expand_pseudo_instruction_safe (λx.pc) (λx.pc) pc jmp_len instr in
     552  let bv: list (BitVector 8) ≝ match ilist with
     553    [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
     554    | Some l ⇒ flatten … (map … assembly1 l)
     555    ] in
     556  let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in
     557  new_pc.
     558 
     559definition create_label_trie: list labelled_instruction → jump_expansion_policy →
     560  label_trie ≝
     561  λprogram.λpolicy.
     562  let 〈final_n, final_pc, final_labels〉 ≝
     563    foldl_strong (option Identifier × pseudo_instruction)
     564    (λprefix.Σres.True)
     565    program
     566    (λprefix.λx.λtl.λprf.λacc.
     567     let 〈n,pc,labels〉 ≝ acc in
     568     let 〈label,instr〉 ≝ x in
     569     let new_labels ≝
     570       match label with
     571       [ None   ⇒ labels
     572       | Some l ⇒ insert … l 〈n, pc〉 labels
     573       ] in
     574     let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, long_jump〉 in
     575     let new_pc ≝ add_instruction_size pc jmp_len instr in
     576     〈S n, new_pc, new_labels〉
     577    ) 〈0, zero ?, Stub ? ?〉 in
     578    final_labels.
     579 @I
     580qed.
     581
     582definition select_reljump_length: label_trie → Word → Identifier → jump_length ≝
     583  λlabels.λpc.λlbl.
     584  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
     585  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT pending lookup of right condition *)
     586  then short_jump
     587  else long_jump.
     588
     589definition select_call_length: label_trie → Word → Identifier → jump_length ≝
     590  λlabels.λpc.λlbl.
     591  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
     592  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
     593  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     594  if eq_bv ? fst_5_addr fst_5_pc
     595  then medium_jump
     596  else long_jump.
     597 
     598definition select_jump_length: label_trie → Word → Identifier → jump_length ≝
     599  λlabels.λpc.λlbl.
     600  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
     601  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT *)
     602  then short_jump
     603  else
     604    let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
     605    let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
     606    let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     607    if eq_bv ? fst_5_addr fst_5_pc
     608    then medium_jump
     609    else long_jump.
    899610 
     611definition jump_expansion_step_instruction: label_trie → Word →
     612  preinstruction Identifier → option jump_length ≝
     613  λlabels.λpc.λi.
     614  match i with
     615  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
     616  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
     617  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
     618  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
     619  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
     620  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
     621  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
     622  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
     623  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
     624  | _        ⇒ None ?
     625  ].
     626
     627definition max_length: jump_length → jump_length → jump_length ≝
     628  λj1.λj2.
     629  match j1 with
     630  [ long_jump   ⇒ long_jump
     631  | medium_jump ⇒
     632    match j2 with
     633    [ long_jump ⇒ long_jump
     634    | _         ⇒ medium_jump
     635    ]
     636  | short_jump  ⇒ j2
     637  ].
     638     
     639definition jump_expansion_step: list labelled_instruction →
     640  jump_expansion_policy → jump_expansion_policy ≝
     641  λprogram.λpolicy.
     642  let labels ≝ create_label_trie program policy in
     643  let 〈final_n, final_pc, final_policy〉 ≝
     644    foldl_strong (option Identifier × pseudo_instruction)
     645    (λprefix.Σres.True)
     646    program
     647    (λprefix.λx.λtl.λprf.λacc.
     648      let 〈n, pc, policy〉 ≝ acc in
     649      let 〈label,instr〉 ≝ x in
     650      let old_jump_length ≝ lookup_opt … (bitvector_of_nat 16 n) policy in
     651      let add_instr ≝
     652        match instr with
     653        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
     654        | Call c        ⇒ Some ? (select_call_length labels pc c)
     655        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
     656        | _             ⇒ None ?
     657        ] in
     658      let 〈new_pc, new_policy〉 ≝
     659        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, short_jump〉 in
     660        match add_instr with
     661        [ None    ⇒ (* i.e. it's not a jump *)
     662          〈add_instruction_size pc long_jump instr, policy〉
     663        | Some ai ⇒
     664          let new_length ≝ max_length old_length ai in
     665          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 n) 〈pc, new_length〉 policy〉
     666        ] in
     667      〈S n, new_pc, new_policy〉
     668    ) 〈0, zero ?, Stub ? ?〉 in
     669    final_policy.
     670 @I
     671qed.
     672 
     673definition jump_expansion_internal: list labelled_instruction → jump_expansion_policy ≝
     674  λprogram.
     675    Stub ? ?.
     676   
    900677(**************************************** START OF POLICY ABSTRACTION ********************)
    901678
     
    904681definition jump_expansion': pseudo_assembly_program → policy_type ≝
    905682 λprogram.λpc.
    906   let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
    907   lookup ? ? pc policy long_jump.
    908  normalize //
    909 qed.
    910  
     683  let policy ≝ jump_expansion_internal (\snd program) in
     684  let 〈n,j〉 ≝ lookup ? ? pc policy 〈zero ?, long_jump〉 in
     685    j.
     686 
    911687definition assembly_1_pseudoinstruction_safe ≝
    912688  λprogram: pseudo_assembly_program.
     
    918694  λi.
    919695  let expansion ≝ jump_expansion ppc in
    920     match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
     696    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
    921697    [ None ⇒ None ?
    922698    | Some pseudos ⇒
     
    958734   program counters. It is at the heart of the proof. *)
    959735(*CSC: code taken from build_maps *)
    960 definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     736definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    961737 λinstr_list.
    962738 λjump_expansion: policy_type.
    963739 λl:list labelled_instruction.
     740 λacc.
    964741  foldl ??
    965742   (λt,i.
     
    975752              let 〈pc,ignore〉 ≝ pc_ignore in
    976753              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
    977        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
     754       ]) acc l.
    978755
    979756definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
    980  ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
     757 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
    981758
    982759definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
    983760 λprogram,jump_expansion,instr_list.
    984   match sigma00 program jump_expansion instr_list with
     761  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
    985762   [ None ⇒ None …
    986763   | Some result ⇒
     
    1042819
    1043820(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    1044 definition assembly_1_pseudoinstruction:
     821definition assembly_1_pseudoinstruction':
    1045822 ∀program:pseudo_assembly_program.∀pol: policy program.
    1046823  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
     
    1049826  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    1050827  Σres:(nat × (list Byte)).
     828   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
    1051829   let 〈len,code〉 ≝ res in
    1052830    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     
    1068846   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
    1069847   cases daemon
    1070  | cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
     848 | % [ >p %]
     849   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
    1071850   (* THIS SHOULD BE TRUE INSTEAD *)
    1072851   cases daemon]
    1073852qed.
    1074853
     854definition assembly_1_pseudoinstruction:
     855 ∀program:pseudo_assembly_program.∀pol: policy program.
     856  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
     857  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
     858  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
     859  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     860   nat × (list Byte)
     861≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
     862   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
     863    prf2 prf3.
     864
     865lemma assembly_1_pseudoinstruction_ok1:
     866 ∀program:pseudo_assembly_program.∀pol: policy program.
     867  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
     868  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
     869  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
     870  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
     871     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
     872   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
     873 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
     874 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
     875 #H1 #_ @H1
     876qed.
     877
    1075878(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    1076879definition construct_costs':
    1077  ∀program. policy program → nat → nat → ? → ? →
    1078   Σres:(nat × (BitVectorTrie Word 16)). True
     880 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
     881  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
    1079882
    1080883  λprogram.λpol: policy program.λppc,pc,costs,i.
     
    1083886    | Some res ⇒ res ].
    1084887 [ cases daemon
    1085  | %]
     888 | >p %]
    1086889qed.
    1087890
    1088891definition construct_costs ≝
    1089892 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
     893
     894lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
     895 #A #a #b #EQ destruct //
     896qed.
     897
     898lemma sigma00_strict:
     899 ∀instr_list,jump_expansion,l,acc. acc = None ? →
     900  sigma00 instr_list jump_expansion l acc = None ….
     901 #instr_list #jump_expansion #l elim l
     902  [ #acc #H >H %
     903  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
     904qed.
     905
     906lemma sigma00_append:
     907 ∀instr_list,jump_expansion,l1,l2,acc.
     908  sigma00 instr_list jump_expansion (l1@l2) acc =
     909   sigma00 instr_list jump_expansion
     910    l2 (sigma00 instr_list jump_expansion l1 acc).
     911 whd in match sigma00; normalize nodelta;
     912 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
     913qed.
     914
     915lemma policy_ok_prefix_ok:
     916 ∀program.∀pol:policy program.∀suffix,prefix.
     917  prefix@suffix = \snd program →
     918   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
     919 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
     920 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
     921 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
     922 normalize nodelta >sigma00_append
     923 cases (sigma00 ?? prefix ?)
     924  [2: #x #_ % #abs destruct(abs)
     925  | * #abs @⊥ @abs >sigma00_strict % ]
     926qed.
     927
     928lemma policy_ok_prefix_hd_ok:
     929 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
     930  (prefix@[hd])@suffix = \snd program →
     931   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
     932    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     933    let 〈program_counter, sigma_map〉 ≝ pc_map in
     934    let 〈label, i〉 ≝ hd in
     935     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
     936 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
     937 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
     938  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
     939 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
     940 @pair_elim' #pc #map #EQ4 normalize nodelta
     941 @pair_elim' #l' #i' #EQ5 normalize nodelta
     942 cases (construct_costs_safe ??????) normalize
     943  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
     944qed.
     945
     946(*
     947lemma tech_pc_sigma00_append_Some:
     948 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
     949  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
     950   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
     951 #program #pol #prefix #costs #label #i #ppc #pc #H
     952  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
     953  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
     954  generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
     955  whd in match sigma0; normalize nodelta;
     956  >foldl_step
     957  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
     958  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
     959  cases (sigma00 program pol prefix) in H ⊢ %
     960   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
     961   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
     962     
     963     normalize nodelta; -H;
     964     
     965 
     966   generalize in match H; -H;
     967  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
     968   [2: whd in ⊢ (??%%)
     969XXX
     970*)
    1090971
    1091972axiom construct_costs_sigma:
Note: See TracChangeset for help on using the changeset viewer.