Changeset 1054


Ignore:
Timestamp:
Jul 5, 2011, 9:51:31 AM (8 years ago)
Author:
boender
Message:
  • proven policy safe
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1040 r1054  
    434434  | long_jump: jump_length.
    435435
    436 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
    437 
    438 definition find_right_call: Word → Word → nat × (option jump_length) ≝
     436definition find_right_call: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝
    439437 (* medium call: 11 bits, only in "current segment" *)
    440438 (* can this be done more efficiently with bit vector arithmetic? *)
    441439 λpc.λaddress.
    442   let 〈p1, p2〉 ≝ split ? 5 11 address in
    443   let 〈a1, a2〉 ≝ split ? 5 11 pc in
    444    if eq_bv ? p1 a1 then (* we're in the same segment *)
    445     〈2, Some ? medium_jump〉
     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    〈3, 2, address, Some ? medium_jump〉
    446444   else
    447     〈3, Some ? long_jump〉.
    448 
     445    〈3, 3, address, Some ? long_jump〉.
     446   
     447lemma 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 | // ] ]
     464qed.
     465       
    449466definition distance ≝
    450467 λx.λy.if gtb x y then x - y else y - x.
    451468 
    452 definition find_right_jump: Word → Word → nat × (option jump_length) ≝
     469definition find_right_jump: Word → Word → (nat × nat) × (Word × (option jump_length)) ≝
    453470 (* short jump: 8 bits signed *)
    454471 (* medium jump: 11 bits, forward only *)
     
    457474  let pa ≝ nat_of_bitvector ? address in
    458475   if ltb (distance pn pa) 127 then
    459     〈2, Some ? short_jump〉
     476    〈2, 3, address, Some ? short_jump〉
    460477   else
    461478    find_right_call pc address.
    462479
    463 definition find_right_relative_jump: Word → (BitVectorTrie Word 16) →
    464  Identifier → nat × (option jump_length) ≝
     480lemma 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  ]
     504qed.
     505   
     506definition find_right_relative_jump: Word → (BitVectorTrie (Word × Identifier) 16) →
     507 Identifier → (nat × nat) × (Word × (option jump_length)) ≝
    465508 λpc.λlabels.λjmp.
    466509 match lookup_opt ? ? jmp labels with
    467  [ None ⇒ 〈2, Some ? short_jump〉
    468  | Some a ⇒ find_right_jump pc a ].
     510 [ None ⇒ 〈3, 3, pc, Some ? long_jump〉
     511 | Some x ⇒ let 〈ignore, a〉 ≝ x in find_right_jump pc a ].
    469512 
    470 definition jep_relative: Word → (BitVectorTrie Word 16) → preinstruction Identifier → ? ≝
     513lemma 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 ]
     538qed.
     539     
     540definition jep_relative: Word → (BitVectorTrie (Word × Identifier) 16) → preinstruction Identifier → ? ≝
    471541 λpc.λlabels.λi.
    472542  match i with
     
    480550  | CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp
    481551  | DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp
    482   | _ ⇒ 〈length ? (assembly_preinstruction ? (λx.zero ?) i), None …〉 ].
    483  
     552  | _ ⇒ let l ≝ length ? (assembly_preinstruction ? (λx.zero ?) i) in
     553         〈l, l, pc, None …〉 ].
     554
     555definition jgeq_opt ≝
     556 λa:jump_length.λb:option (Word × jump_length).
     557 match a with
     558 [ short_jump ⇒ match b with
     559   [ None ⇒ (* XXX *) False
     560   | Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump
     561   ]
     562 | medium_jump ⇒ match b with
     563  [ None ⇒  (* XXX *) False
     564  | Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump ∨ j = medium_jump ]
     565 | long_jump ⇒ True
     566 ].
     567
     568definition is_long_jump ≝
     569 λj.match j with
     570 [ long_jump ⇒ true
     571 | _         ⇒ false
     572 ].
     573
     574definition policy_safe ≝
     575 λp:BitVectorTrie (Word × Word × jump_length) 16.
     576  forall ? ? p (λ_.λx.let 〈pc,addr,j〉 ≝ x in
     577   match j with
     578   [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? addr) < 127
     579   | medium_jump ⇒ \fst (split ? 5 11 addr) = \fst (split ? 5 11 pc)
     580   | long_jump ⇒ True
     581   ]
     582  ).
     583
     584definition jump_expansion_policy ≝
     585  Σpolicy:BitVectorTrie (Word × Word × jump_length) 16.policy_safe policy.
     586 
     587definition inject_jump_expansion_policy:
     588 ∀x:BitVectorTrie (Word × Word × jump_length) 16.
     589  policy_safe x → jump_expansion_policy ≝ inject ….
     590 
     591coercion inject_jump_expansion_policy:
     592 ∀x:BitVectorTrie (Word × Word × jump_length) 16.
     593  policy_safe x → jump_expansion_policy ≝ inject_jump_expansion_policy
     594 on x:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy.
     595
    484596definition jump_expansion_policy_internal: pseudo_assembly_program →
    485  (BitVectorTrie Word 16) → jump_expansion_policy →
    486  ((BitVectorTrie Word 16) × jump_expansion_policy × bool)≝
    487  λprogram.λlabels.λpolicy.
    488    let 〈pc, new_labels, new_policy, changed〉 ≝
    489    foldl ? ? (λacc.λi:labelled_instruction.
    490     let 〈label, instr〉 ≝ i in
    491     let 〈pc,labels,policy,c0〉 ≝ acc in
    492     let 〈c1,new_labels〉 ≝ match label with
    493      [ None ⇒ 〈c0,labels〉
    494      | Some l ⇒
    495        match update ? ? pc l labels with
    496        [ None ⇒ 〈c0,labels〉
    497        | Some x ⇒ 〈true, x〉 ] ] in
    498     let 〈pc_delta, jmp_len〉 ≝ match instr with
    499      [ Call c ⇒
    500        match lookup_opt ? ? c new_labels with
    501         [ None        ⇒ 〈2, Some ? medium_jump〉
    502         | Some c_addr ⇒ find_right_call pc c_addr ]
    503      | Jmp j ⇒
    504        match lookup_opt ? ? j new_labels with
    505         [ None        ⇒ 〈2, Some ? short_jump〉
    506         | Some j_addr ⇒ find_right_jump pc j_addr ]
    507      | Instruction i ⇒ jep_relative pc new_labels i
    508      | Mov _ _ ⇒ 〈3, None …〉
    509      | Cost _ ⇒ 〈0, None …〉
    510      | Comment _ ⇒ 〈0, None …〉 ] in
    511     let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    512     match jmp_len with
    513     [ None   ⇒ 〈new_pc, new_labels, policy, c1〉
    514     | Some j ⇒
    515       match update ? ? pc j policy with
    516       [ None ⇒ 〈new_pc, new_labels, policy, c1〉
    517       | Some x ⇒ 〈new_pc, new_labels, x, true〉 ] ]
    518    ) 〈zero ?, labels, policy, false〉 (\snd program) in
    519    〈labels, policy, changed〉.
    520 
     597 (BitVectorTrie (Word × Identifier) 16) → jump_expansion_policy →
     598 Σres:(BitVectorTrie (Word × Identifier) 16) × (BitVectorTrie (Word × Word × jump_length) 16).
     599  let 〈x,p〉 ≝ res in policy_safe p ≝
     600 λprogram.λold_labels.λold_policy.
     601   let res ≝
     602   foldl_strong (option Identifier × pseudo_instruction)
     603    (λprefix.Σresult:(Word × Word) × ((BitVectorTrie (Word × Identifier) 16) ×
     604      (BitVectorTrie (Word × Word × jump_length) 16)).
     605      let 〈x,y,z,p〉 ≝ result in policy_safe p
     606    )
     607    (\snd program)
     608    (λprefix.λi.λtl.λprf.λacc.   
     609     let 〈label, instr〉 ≝ i in
     610     let 〈pc,orig_pc,labels,policy〉 ≝ acc in
     611     let new_labels ≝ match label return λ_.(BitVectorTrie (Word × Identifier) 16) with
     612      [ None ⇒ labels
     613      | Some l ⇒ insert ? ? orig_pc 〈pc,l〉 labels
     614      ] in
     615     let add_instr ≝ match instr with
     616      [ Call c ⇒
     617        match lookup_opt ? ? c new_labels with
     618         [ None   ⇒ 〈3, 3, pc, Some ? long_jump〉
     619         | Some x ⇒ let 〈ignore,c_addr〉 ≝ x in find_right_call pc c_addr ]
     620      | Jmp j ⇒
     621        match lookup_opt ? ? j new_labels with
     622         [ None   ⇒ 〈3, 3, pc, Some ? long_jump〉
     623         | Some x ⇒ let 〈ignore,j_addr〉 ≝ x in find_right_jump pc j_addr ]
     624      | Instruction i ⇒ jep_relative pc new_labels i
     625      | Mov _ _ ⇒ 〈3, 3, pc, None …〉
     626      | Cost _ ⇒ 〈0, 0, pc, None …〉
     627      | Comment _ ⇒ 〈0, 0, pc, None …〉 ] in
     628     let 〈pc_delta, orig_pc_delta, addr, jmp_len〉 ≝ add_instr in
     629     let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
     630     let 〈new_orig_pc,ignore〉 ≝ add_16_with_carry orig_pc (bitvector_of_nat ? orig_pc_delta) false in
     631     match jmp_len with
     632      [ None   ⇒ 〈new_pc, orig_pc, new_labels, policy〉
     633      | Some j ⇒ 〈new_pc, new_orig_pc, new_labels, insert ? ? orig_pc 〈pc, addr, j〉 policy〉
     634      ]
     635    ) 〈zero ?, zero ?, old_labels, eject … old_policy〉 in
     636   let 〈npc, norig_pc, nlabels, npolicy〉 ≝ res in
     637   〈nlabels, npolicy〉.
     638   [ cases res in p -res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb;
     639     >Hb in Ha; normalize nodelta #H @H
     640   | generalize in match (sig2 … acc) >p1 >p2 >p3 #H
     641     @(forall_insert … H)  normalize nodelta normalize nodelta in p4; cases instr in p4; >p5 >p6 normalize nodelta
     642     [5: #str >p9 #Heq cases (lookup_opt ? ? str ?) in Heq; normalize nodelta
     643         [ #Heq2 lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
     644           #Heq3 destruct (Heq3) //
     645         | #x cases x -x #i0 #c_addr normalize nodelta lapply (frc_ok pc c_addr)
     646           cases (find_right_call pc c_addr) #x #y cases x #i0 #i1 -x; cases y #ad #jmp -y;
     647           normalize nodelta #Heq #Heq2
     648           >(proj1 ? ? Heq) in Heq2; #Heq2
     649           <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
     650           >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq;
     651           cases j normalize nodelta #Heq [ @⊥ ] @(proj2 ? ? Heq)
     652         ]
     653    |2,3,6: [3: #x] #z >p9 #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
     654       #ctd destruct (ctd)
     655    |1,4:
     656      #pi
     657       [1: cases label normalize nodelta [ #Hjep | #id #Hjep ] whd in Hjep: (??%??); cases pi in Hjep;
     658       |2: cases (lookup_opt ? ? pi ?) normalize nodelta >p9
     659           [ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
     660             #ctd destruct (ctd) //
     661           | #x cases x -x #i0 #j_addr normalize nodelta lapply (frj_ok pc j_addr)
     662             cases (find_right_jump pc j_addr) #x #y cases x #i0 #i1 -x; cases y #ad #jump -y;
     663             normalize nodelta #Heq #Heq2
     664             >(proj1 ? ? Heq) in Heq2; #Heq2
     665             <(proj1 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2))))
     666             >(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq2)))) in Heq;
     667             cases j normalize nodelta #Heq @(proj2 ? ? Heq)
     668           ]
     669       ]
     670       [1,2,3,6,7,33,34,38,39,40,43,44,70,71: #acc #x normalize nodelta #Heq
     671         <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
     672         #ctd destruct (ctd)
     673       |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:
     674         #acc normalize nodelta #Heq
     675         <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
     676         #ctd destruct (ctd)
     677       |35,36,37,72,73,74: normalize nodelta #Heq
     678         <(proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq)))) in p9;
     679         #ctd destruct (ctd)
     680       |9,10,14,15: #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id)
     681           whd in match (find_right_relative_jump pc labels j_id)
     682          normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta
     683          [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
     684             #Heq2 destruct (Heq2) //
     685          |2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
     686            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
     687          ]
     688       |46,47,51,52: #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id)
     689          whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id)
     690          normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta
     691          [1,3,5,7: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
     692             #Heq2 destruct (Heq2) //
     693          |2,4,6,8: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
     694            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
     695          ]
     696       |11,12,13,16,17: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc labels j_id)
     697          whd in match (find_right_relative_jump pc labels j_id)
     698          normalize nodelta cases (lookup_opt ? ? j_id labels) normalize nodelta
     699          [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
     700             #Heq2 destruct (Heq2) //
     701          |2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
     702            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
     703          ]
     704       |48,49,50,53,54: #x #j_id normalize nodelta >p9 lapply (frrj_ok pc (insert … orig_pc 〈pc,id〉 labels) j_id)
     705          whd in match (find_right_relative_jump pc (insert … orig_pc 〈pc,id〉 labels) j_id)
     706          normalize nodelta cases (lookup_opt ? ? j_id (insert … orig_pc 〈pc,id〉 labels)) normalize nodelta
     707          [1,3,5,7,9: #_ #Heq lapply (proj2 ? ? (pair_destruct … (proj2 ? ? (pair_destruct … Heq))))
     708             #Heq2 destruct (Heq2) //
     709          |2,4,6,8,10: #x cases x #i0 #j_addr #Hok #Heq >Heq in Hok;
     710            normalize nodelta #Hok >(proj1 … Hok) @(proj2 … Hok)
     711          ]
     712       ]
     713     ]
     714   | generalize in match (sig2 … acc) >p1 >p2 >p3 #H
     715     @H
     716   | generalize in match (sig2 … old_policy) #H @H
     717   ]
     718qed.
     719   
    521720definition expand_relative_jump_internal:
    522721 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
     
    591790  ].
    592791
    593 definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
     792definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
    594793  λlookup_labels.
    595794  λlookup_datalabels.
     
    648847
    649848let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program)
    650  (old_labels: BitVectorTrie Word 16) (old_policy: BitVectorTrie jump_length 16)
    651  on n: jump_expansion_policy ≝
     849 (old_labels: BitVectorTrie (Word × Identifier) 16)
     850 (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16.policy_safe bla)
     851 on n: BitVectorTrie jump_length 16 ≝
    652852 match n with
    653  [ O ⇒ old_policy
     853 [ O ⇒ fold …
     854   (λ_.λx.λacc.let 〈pc,i2,jmp_len〉 ≝ x in insert … pc jmp_len acc)
     855   old_policy (Stub ? ?)
    654856 | S n' ⇒
    655    let 〈new_labels, new_policy, ch〉 ≝
    656     jump_expansion_policy_internal program old_labels old_policy in
    657     jump_expansion_internal n' program new_labels new_policy ].
    658 
     857    (* let 〈x,y〉 ≝ jump_expansion_policy_internal program old_labels old_policy in *)
     858    jump_expansion_internal n' program (* x y *)
     859    (\fst (jump_expansion_policy_internal program old_labels old_policy))
     860    (\snd (jump_expansion_policy_internal program old_labels old_policy))
     861 ].
     862 generalize in match (sig2 … (jump_expansion_policy_internal program old_labels old_policy))
     863 cases (jump_expansion_policy_internal program old_labels old_policy)
     864 #a cases a #xx #pp normalize nodelta
     865 #H #H2 normalize nodelta @H2
     866qed.
     867 
    659868(**************************************** START OF POLICY ABSTRACTION ********************)
    660869
     
    665874  let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
    666875  lookup ? ? pc policy long_jump.
    667  
     876 normalize //
     877qed.
     878 
    668879definition assembly_1_pseudoinstruction_safe ≝
    669880  λprogram: pseudo_assembly_program.
     
    675886  λi.
    676887  let expansion ≝ jump_expansion ppc in
    677     match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
     888    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    678889    [ None ⇒ None ?
    679890    | Some pseudos ⇒
     
    715926   program counters. It is at the heart of the proof. *)
    716927(*CSC: code taken from build_maps *)
    717 definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     928definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    718929 λinstr_list.
    719930 λjump_expansion: policy_type.
    720931 λl:list labelled_instruction.
    721  λacc.
    722932  foldl ??
    723933   (λt,i.
     
    733943              let 〈pc,ignore〉 ≝ pc_ignore in
    734944              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
    735        ]) acc l.
     945       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
    736946
    737947definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
    738  ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
     948 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
    739949
    740950definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
    741951 λprogram,jump_expansion,instr_list.
    742   match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
     952  match sigma00 program jump_expansion instr_list with
    743953   [ None ⇒ None …
    744954   | Some result ⇒
     
    8001010
    8011011(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    802 definition assembly_1_pseudoinstruction':
     1012definition assembly_1_pseudoinstruction:
    8031013 ∀program:pseudo_assembly_program.∀pol: policy program.
    8041014  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
     
    8071017  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    8081018  Σres:(nat × (list Byte)).
    809    Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
    8101019   let 〈len,code〉 ≝ res in
    8111020    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     
    8271036   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
    8281037   cases daemon
    829  | % [ >p %]
    830    cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
     1038 | cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
    8311039   (* THIS SHOULD BE TRUE INSTEAD *)
    8321040   cases daemon]
    8331041qed.
    8341042
    835 definition assembly_1_pseudoinstruction:
    836  ∀program:pseudo_assembly_program.∀pol: policy program.
    837   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    838   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    839   lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
    840   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    841    nat × (list Byte)
    842 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
    843    assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
    844     prf2 prf3.
    845 
    846 lemma assembly_1_pseudoinstruction_ok1:
    847  ∀program:pseudo_assembly_program.∀pol: policy program.
    848   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    849   ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
    850   ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
    851   ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
    852      Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
    853    = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
    854  #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
    855  cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
    856  #H1 #_ @H1
    857 qed.
    858 
    8591043(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    8601044definition construct_costs':
    861  ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
    862   Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
     1045 ∀program. policy program → nat → nat → ? → ? →
     1046  Σres:(nat × (BitVectorTrie Word 16)). True
    8631047
    8641048  λprogram.λpol: policy program.λppc,pc,costs,i.
     
    8671051    | Some res ⇒ res ].
    8681052 [ cases daemon
    869  | >p %]
     1053 | %]
    8701054qed.
    8711055
    8721056definition construct_costs ≝
    8731057 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
    874 
    875 (*
    876 axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
    877 axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
    878 
    879 let rec foldl_strong_internal
    880   (A: Type[0]) (P: list A → Type[0]) (l: list A) (suffix2: list A)
    881   (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl @suffix2 → P prefix → P (prefix @ [hd]))
    882   (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
    883     l = prefix @ suffix @ suffix2 → P(prefix @ suffix) ≝
    884   match suffix return λl'. l = prefix @ l' @ suffix2 → P (prefix @ l') with
    885   [ nil ⇒ λprf. ?
    886   | cons hd tl ⇒ λprf. ?
    887   ].
    888   [ > (append_nil ?)
    889     @ acc
    890   | applyS (foldl_strong_internal A P l suffix2 H (prefix @ [hd]) tl ? ?)
    891     [ @(H prefix hd tl prf acc)
    892     | >prf /2/]]
    893 qed.
    894 
    895 definition foldl_strong ≝
    896   λA: Type[0].
    897   λP: list A → Type[0].
    898   λl: list A.
    899   λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
    900   λacc: P [ ].
    901     foldl_strong_internal A P l [ ] ? [ ] l acc ?.
    902  [ #prefix #hd #tl >append_nil @H
    903  | >append_nil % ]
    904 qed.
    905 
    906 axiom foldl_strong_step:
    907  ∀A:Type[0].
    908   ∀P: list A → Type[0].
    909    ∀l: list A.
    910     ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
    911      ∀acc: P [ ].
    912       ∀Q: ∀prefix. P prefix → Prop.
    913        ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
    914         ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
    915        Q [ ] acc →
    916         Q l (foldl_strong A P l H acc).
    917 (*
    918  #A #P #l #H #acc #Q #HQ #Hacc normalize;
    919  generalize in match
    920   (foldl_strong ?
    921    (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
    922    l ? Hacc)
    923  [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
    924  [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
    925  #K
    926 
    927  generalize in match
    928   (foldl_strong ?
    929    (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
    930  [2: @H
    931 *)
    932 
    933 axiom foldl_elim:
    934  ∀A:Type[0].
    935   ∀B: Type[0].
    936    ∀H: A → B → A.
    937     ∀acc: A.
    938      ∀l: list B.
    939       ∀Q: A → Prop.
    940        (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
    941          Q acc →
    942           Q (foldl A B H acc l).
    943 *)
    944 
    945 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
    946  #A #a #b #EQ destruct //
    947 qed.
    948 
    949 lemma sigma00_strict:
    950  ∀instr_list,jump_expansion,l,acc. acc = None ? →
    951   sigma00 instr_list jump_expansion l acc = None ….
    952  #instr_list #jump_expansion #l elim l
    953   [ #acc #H >H %
    954   | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
    955 qed.
    956 
    957 lemma sigma00_append:
    958  ∀instr_list,jump_expansion,l1,l2,acc.
    959   sigma00 instr_list jump_expansion (l1@l2) acc =
    960    sigma00 instr_list jump_expansion
    961     l2 (sigma00 instr_list jump_expansion l1 acc).
    962  whd in match sigma00; normalize nodelta;
    963  #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
    964 qed.
    965 
    966 lemma policy_ok_prefix_ok:
    967  ∀program.∀pol:policy program.∀suffix,prefix.
    968   prefix@suffix = \snd program →
    969    sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
    970  * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
    971  generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
    972  whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
    973  normalize nodelta >sigma00_append
    974  cases (sigma00 ?? prefix ?)
    975   [2: #x #_ % #abs destruct(abs)
    976   | * #abs @⊥ @abs >sigma00_strict % ]
    977 qed.
    978 
    979 lemma policy_ok_prefix_hd_ok:
    980  ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
    981   (prefix@[hd])@suffix = \snd program →
    982    Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
    983     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    984     let 〈program_counter, sigma_map〉 ≝ pc_map in
    985     let 〈label, i〉 ≝ hd in
    986      construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
    987  * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
    988  generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
    989   (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
    990  @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
    991  @pair_elim' #pc #map #EQ4 normalize nodelta
    992  @pair_elim' #l' #i' #EQ5 normalize nodelta
    993  cases (construct_costs_safe ??????) normalize
    994   [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
    995 qed.
    996 
    997 (*
    998 lemma tech_pc_sigma00_append_Some:
    999  ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
    1000   tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
    1001    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
    1002  #program #pol #prefix #costs #label #i #ppc #pc #H
    1003   whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
    1004   whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
    1005   generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
    1006   whd in match sigma0; normalize nodelta;
    1007   >foldl_step
    1008   change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
    1009   whd in match tech_pc_sigma00 in H; normalize nodelta in H;
    1010   cases (sigma00 program pol prefix) in H ⊢ %
    1011    [ whd in ⊢ (??%% → ?) #abs destruct(abs)
    1012    | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
    1013      
    1014      normalize nodelta; -H;
    1015      
    1016  
    1017    generalize in match H; -H;
    1018   generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
    1019    [2: whd in ⊢ (??%%)
    1020 XXX
    1021 *)
    10221058
    10231059axiom construct_costs_sigma:
Note: See TracChangeset for help on using the changeset viewer.