Changeset 1937 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 11, 2012, 3:06:15 PM (8 years ago)
Author:
boender
Message:
  • filled in some of the gaps in the proof of Policy
  • reverted internal type of ppc_map from bool to jump_length (in order to help with termination)
  • moved some lemmas to Util
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1934 r1937  
    1515
    1616(* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *)
    17 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × bool) 16).
     17definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16).
    1818
    1919(* The different properties that we want/need to prove at some point *)
     
    8585 
    8686(* Between two policies, jumps cannot decrease *)
     87definition jmpeqb: jump_length → jump_length → bool ≝
     88  λj1.λj2.
     89  match j1 with
     90  [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ]
     91  | medium_jump ⇒ match j2 with [ medium_jump ⇒ true | _ ⇒ false ]
     92  | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ]
     93  ].
     94
     95lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2.
     96 #j1 #j2 cases j1 cases j2
     97 [1,5,9: / by /]
     98 #H cases H
     99qed.
     100
    87101definition jmple: jump_length → jump_length → Prop ≝
    88102  λj1.λj2.
     
    108122 λprogram.λop.λp.
    109123 ∀i.i < |program| →
    110    let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,false〉 in
    111    let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,false〉 in
    112      opc ≤ pc.
    113      (*∧ match ox with
    114      [ Some oj ⇒
    115        match x with
    116        [ Some j ⇒ jmpleq oj j
    117        | _ ⇒ True
    118        ]
    119      | _ ⇒ True
    120      ].*)
    121 
    122 (*
     124   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in
     125   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in
     126     opc ≤ pc ∧ jmpleq oj j.
    123127
    124128(* Policy safety *)
     
    149153
    150154(* this is the instruction size as determined by the distance from origin to destination *)
    151 definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝
     155(*definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝
    152156 λlabels.λsigma.λpc.λi.
    153157 \fst (assembly_1_pseudoinstruction
    154158   (λid.bitvector_of_nat 16 (lookup_def … labels id 0))
    155    (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,None ?〉))) pc
    156    (λx.zero 16) i).
     159   (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,false〉))) pc
     160   (λx.zero 16) i).*)
    157161 
    158162(* this is the instruction size as determined by the jump length given *)
     
    255259    [ None ⇒ False
    256260    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    257        pc1 = instruction_size_sigma labels sigma (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉))
     261       pc1 = instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
     262         (λppc.let 〈x,y〉 ≝ bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉 in
     263           〈bitvector_of_nat ? x, jmpeqb y long_jump〉)
     264         (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉))
    258265    ]
    259266  ].
     
    297304  prefix
    298305  (λhd.λx.λtl.λp.λacc.
    299     acc + (instruction_size_sigma labels sigma (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
     306    acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
     307    (λppc.let 〈x,y〉 ≝ bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉 in
     308           〈bitvector_of_nat ? x, jmpeqb y long_jump〉)
     309    (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
    300310  0.
    301311
     
    309319  ) ≝
    310320 λprogram.
    311  
     321   \fst (create_label_cost_map program).
     322 #i #Hi #l #Hl1 #Hl2 lapply (pi2 ?? (create_label_cost_map program)) @pair_elim
     323 #labels #costs #EQ normalize nodelta #H @(H i Hi l Hl1 Hl2)
    312324qed.
    313325
     
    318330  if leb ppc paddr (* forward jump *)
    319331  then
    320     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,None ?〉)
     332    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)
    321333                    + added in
    322334    if leb (addr - \fst inc_sigma) 126
     
    324336    else long_jump
    325337  else
    326     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,None ?〉) in
     338    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    327339    if leb (\fst inc_sigma - addr) 129
    328340    then short_jump
     
    335347  let addr ≝
    336348    if leb ppc paddr (* forward jump *)
    337     then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,None ?〉)
     349    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)
    338350            + added
    339     else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,None ?〉) in
     351    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    340352  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (bitvector_of_nat ? addr) in
    341353  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in
     
    350362  if leb ppc paddr (* forward jump *)
    351363  then
    352     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,None ?〉)
     364    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)
    353365              + added in
    354366    if leb (addr - \fst inc_sigma) 126
     
    356368    else select_call_length labels old_sigma inc_sigma added ppc lbl
    357369  else
    358     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,None ?〉) in
     370    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    359371    if leb (\fst inc_sigma - addr) 129
    360372    then short_jump
     
    394406qed.
    395407
    396 lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
     408(*lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    397409 ∀policy:(Σp:ppc_pc_map.
    398410 out_of_program_none prefix p ∧ jump_in_policy prefix p).
     
    411423  #H elim H -H; #x #H >H in Hnone; #abs destruct (abs)
    412424
    413 qed.
    414 
    415 (* these two obviously belong somewhere else *) 
    416 lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
    417   s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
    418  #A #P #s1 #s2 / by /
    419 qed.
    420 
    421 lemma Some_eq:
    422  ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
    423  #T #x #y #H @option_destruct_Some @H
    424 qed.
     425qed.*)
    425426
    426427(* The first step of the jump expansion: everything to short.
     
    431432  ∀labels:label_map.
    432433  Σpolicy:ppc_pc_map.
    433     And (And (out_of_program_none (pi1 ?? program) policy)
    434     (jump_in_policy (pi1 ?? program) policy))
     434    And (out_of_program_none (pi1 ?? program) policy)
    435435    (policy_isize_sum (pi1 ?? program) labels policy) ≝
    436436  λprogram.λlabels.
    437437  foldl_strong (option Identifier × pseudo_instruction)
    438438  (λprefix.Σpolicy:ppc_pc_map. 
    439     And (And (out_of_program_none prefix policy)
    440     (jump_in_policy prefix policy))
     439    And (out_of_program_none prefix policy)
    441440    (policy_isize_sum prefix labels policy))
    442441  program
     
    448447   match instr with
    449448   [ Instruction i ⇒ match i with
    450      [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    451      | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    452      | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    453      | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    454      | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    455      | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    456      | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    457      | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    458      | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    459      | _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,None ?〉 sigma
     449     [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     450     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     451     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     452     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     453     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     454     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     455     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     456     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     457     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     458     | _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    460459     ]
    461    | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    462    | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
    463    | _      ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,None ?〉 sigma
     460   | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     461   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
     462   | _      ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    464463   ]〉
    465464  ) 〈0, Stub ? ?〉.
    466 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
    467   [ #Hi2
     465[ @conj
     466  [ #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
    468467    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    469468    cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi
     
    482481            ]
    483482          ]
    484           @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     483          @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    485484        |38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74:
    486485          [1,2,3,6,7,24,25: #x #y
     
    497496            ]
    498497          ]
    499           <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     498          <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    500499          >Hi @Hi2
    501500        |9,10,11,12,13,14,15,16,17:
     
    507506            ]
    508507          |1,3,5,7,9,11,13,15,17:
    509             @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     508            @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    510509          ]
    511510        |46,47,48,49,50,51,52,53,54:
     
    517516            ]
    518517          |1,3,5,7,9,11,13,15,17:
    519             @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
     518            @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
    520519          ]
    521520        ]
     
    529528          ]
    530529        ]
    531         [1,3,4: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     530        [1,3,4: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    532531        |2,5,6:
    533           <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     532          <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    534533          >Hi @Hi2
    535534        ]
     
    542541          |9,12: @sym_neq @lt_to_not_eq <Hi @le_n
    543542          ]         
    544         |1,3: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    545         |5,7: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
     543        |1,3: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     544        |5,7: @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
    546545        ]
    547546      ]
    548     | cases (le_to_or_lt_eq … Hi) -Hi #Hi
     547(*    | cases (le_to_or_lt_eq … Hi) -Hi #Hi
    549548      [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj
    550549        [ #Hj cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
     
    615614            ]
    616615          ]
    617           @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj)
     616          @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj) 
    618617        | #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i (le_S_S_to_le … Hi)))
    619618          cases p in H; -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
     
    682681            / by /
    683682          ]
    684         ]
     683        ] 
    685684    | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
    686685      <minus_n_n whd in match (nth ????); cases x #l #ins cases ins
     
    717716      ]
    718717    ]
    719   ]
     718  ] *)
    720719| cases daemon
    721720]
    722721| @conj
    723   [ @conj
    724     [#i #_ #Hi2 / by refl/
    725     | #i #_ @conj
    726       [ >nth_nil #H @⊥ @H
    727       | #H elim H -H #p >lookup_stub #H destruct (H)
    728       ]
    729     ]
     722  [ #i #_ #Hi2 / by refl/
    730723  | whd in match policy_isize_sum; normalize nodelta
    731724    cases daemon
     
    738731  (* \fst p1 = \fst p2 ∧ *)
    739732  (∀n:ℕ.n < |program| →
    740     let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,None ?〉 in
    741     let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,None ?〉 in
     733    let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
     734    let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
    742735    pc1 = pc2).
    743736   
     
    756749include alias "basics/logic.ma".
    757750
    758 
    759751(* One step in the search for a jump expansion fixpoint. *)
    760 (* Takes a horrible amount of time to typecheck. I suspect disambiguation problems. *)
    761752definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    762753  ∀labels:(Σlm:label_map. ∀i:ℕ.lt i (|program|) →
     
    765756    lookup … lm l = Some ? i).
    766757  ∀old_policy:(Σpolicy:ppc_pc_map.
    767     And (And (And (out_of_program_none program policy)
    768     (jump_in_policy program policy))
     758    And (And (out_of_program_none program policy)
    769759    (policy_isize_sum program labels policy))
    770760    (\fst policy < 2^16)).
     
    773763    match y with
    774764    [ None ⇒ (* nec_plus_ultra program old_policy *) True
    775     | Some p ⇒ And (And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*)
    776        (jump_in_policy program p))
     765    | Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*)
    777766       (policy_isize_sum program labels p))
    778767       (policy_increase program old_policy p))
    779        (policy_safe program labels p))
    780768       (policy_compact program labels p))
    781769       (no_ch = true → policy_equal program old_policy p))
     
    788776    (λprefix.Σx:ℕ × ppc_pc_map.
    789777      let 〈added,policy〉 ≝ x in
    790       And (And (And (And (And (And (out_of_program_none prefix policy)
    791       (jump_in_policy prefix policy))
     778      And (And (And (And (out_of_program_none prefix policy)
    792779      (policy_isize_sum prefix labels policy))
    793780      (policy_increase prefix old_sigma policy))
    794       (policy_safe prefix labels policy))
    795781      (policy_compact prefix labels policy))
    796782      (added = 0 → policy_equal prefix old_sigma policy))
     
    815801      ] in
    816802      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
    817       let 〈old_pc, ol〉 ≝ bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,None ?〉 in
    818       let old_length ≝ match ol with
    819       [ None   ⇒ short_jump
    820       | Some x ⇒ x
    821       ] in
     803      let 〈old_pc,old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉 in
    822804      let old_size ≝ instruction_size_jmplen old_length instr in
    823805      let 〈new_length, isize〉 ≝ match add_instr with
    824       [ None    ⇒ 〈None ?, instruction_size_jmplen short_jump instr〉
    825       | Some pl ⇒ 〈Some ? (max_length old_length pl), instruction_size_jmplen (max_length old_length pl) instr〉
     806      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
     807      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
    826808      ] in
    827809      let new_added ≝ match add_instr with
     
    845827  ]
    846828| lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
    847   cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,None ?〉)
     829  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
    848830  #old_pc #old_length normalize nodelta
    849831(* XXX complicated proof *) cases daemon 
    850 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     832| normalize nodelta @conj [ @conj [ @conj [ @conj
    851833  [ #i #Hi / by refl/
    852   | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x -H #H
    853                    normalize in Hi; @⊥ @(absurd ? Hi) @not_le_Sn_O ]
    854   ]
    855834  | / by refl/
    856   ]]]]]
    857   [4: #_]
     835  ]]]]
     836  [3: #_]
    858837  #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
    859838]
     
    12771256    [ None ⇒ True
    12781257    | Some x ⇒
    1279       And (And (And
     1258      And (And
    12801259        (out_of_program_none program x)
    1281         (jump_in_policy program x))
    12821260        (policy_isize_sum program (create_label_map program) x))
    12831261        (\fst x < 2^16)
     
    13051283  | #j #H @conj
    13061284    [ @conj
    1307       [ @conj
    1308         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
    1309         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
    1310         ]
    1311       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     1285      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     1286      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    13121287      ]
    13131288    | @(proj2 ?? H)
     
    13191294lemma pe_int_refl: ∀program.reflexive ? (policy_equal program).
    13201295#program whd #x whd #n #Hn
    1321 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,None ?〉)
     1296cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
    13221297#y #z normalize nodelta @refl
    13231298qed.
     
    13251300lemma pe_int_sym: ∀program.symmetric ? (policy_equal program).
    13261301#program whd #x #y #Hxy whd #n #Hn
    1327 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉)
     1302lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
    13281303#x1 #x2
    1329 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉)
     1304cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉)
    13301305#y1 #y2 normalize nodelta //
    13311306qed.
     
    13341309#program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
    13351310whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
    1336 lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉)
     1311lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
    13371312#x1 #x2
    1338 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉) #y1 #y2
    1339 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,None ?〉) #z1 #z2
     1313cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2
     1314cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2
    13401315normalize nodelta //
    13411316qed.
     
    14371412 match program with
    14381413 [ nil      ⇒ acc
    1439  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) with
    1440    [ None ⇒ measure_int t policy acc
    1441    | Some j ⇒ match j with
    1442      [ long_jump   ⇒ measure_int t policy (acc + 2)
    1443      | medium_jump ⇒ measure_int t policy (acc + 1)
    1444      | _           ⇒ measure_int t policy acc
    1445      ]
     1414 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with
     1415   [ long_jump   ⇒ measure_int t policy (acc + 2)
     1416   | medium_jump ⇒ measure_int t policy (acc + 1)
     1417   | _           ⇒ measure_int t policy acc
    14461418   ]
    14471419 ].
     
    14541426  [ / by refl/
    14551427  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    1456     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉))
     1428    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
    14571429    [ normalize nodelta @Hd
    1458     | #x cases x
    1459       [ normalize nodelta @Hd
    1460       |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
    1461         @Hd
    1462       ]
     1430    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     1431      @Hd
    14631432    ]
    14641433  ]
     
    14711440[ normalize @le_n
    14721441| #h #t #Hind whd in match (measure_int ???);
    1473   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉))
     1442  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
    14741443  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    1475   | #x cases x
    1476     [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    1477     |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
    1478       @le_plus [1,3: @Hind |2,4: / by le_n/ ]
    1479     ]
     1444  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
     1445    @le_plus [1,3: @Hind |2,4: / by le_n/ ]
    14801446  ]
    14811447]
     
    14841450lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
    14851451  ∀policy:Σp:ppc_pc_map.
    1486     out_of_program_none program p ∧ jump_in_policy program p ∧
     1452    out_of_program_none program p ∧
    14871453    policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
    14881454  ∀l.|l| ≤ |program| → ∀acc:ℕ.
     
    14971463  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
    14981464  [ / by I/
    1499   | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) Hp)
     1465  | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))) (|t|) Hp)
    15001466    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    1501     cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉))
    1502     [ #Hj
    1503       elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (|t|) ?) Hj)
    1504       [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (|t|) ?) Hj)
    1505         [ #j1 normalize nodelta
    1506          cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)
    1507          #x1 #x2
    1508          cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,None ?〉)
    1509          #y1 #y2 normalize nodelta #Hx #Hy >Hx >Hy normalize nodelta
    1510          #Hblerp cases (proj2 ?? Hblerp) cases j1 cases j2
    1511          [1,4,5,7,8,9: #H cases H
    1512          |2,3,6: #_ normalize nodelta
    1513            [1,2: @(transitive_le ? (measure_int t x acc))
    1514            |3: @(transitive_le ? (measure_int t x (acc+1)))
    1515            ]
    1516            [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
    1517            >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    1518          |11,12,13,15,16,17: #H destruct (H)
    1519          |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    1520          ]
    1521        | @(transitive_le … Hp) @le_n
    1522        ]
    1523      | @(transitive_le … Hp) @le_n
    1524      ]
    1525    | #Hnj   
    1526      lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (|t|) ?) Hnj)
    1527      [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) x (|t|) ?) Hnj)
    1528        [3: cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)
    1529           #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,None ?〉)
    1530           #y1 #y2 #Hy #Hx >Hx >Hy normalize nodelta
    1531           #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    1532        |1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))))
    1533        |2: @(transitive_le … Hp) @le_n
    1534        ]
    1535      |1: @(proj1 ?? (proj1 ?? (pi2 ?? policy)))
    1536      |2: @(transitive_le … Hp) @le_n
    1537      ]
    1538    ]
    1539  ]
     1467    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)
     1468    #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉)
     1469    #y1 #y2 normalize nodelta #Hblerp cases (proj2 ?? Hblerp) cases x2 cases y2
     1470    [1,4,5,7,8,9: #H cases H
     1471    |2,3,6: #_ normalize nodelta
     1472      [1,2: @(transitive_le ? (measure_int t x acc))
     1473      |3: @(transitive_le ? (measure_int t x (acc+1)))
     1474      ]
     1475      [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
     1476      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
     1477    |11,12,13,15,16,17: #H destruct (H)
     1478    |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
     1479    ]
     1480  ]
     1481]
    15401482qed.
    15411483
     
    15571499lemma measure_full: ∀program.∀policy.
    15581500  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    1559   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = None ? ∨
    1560   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = Some ? long_jump.
    1561 #program #policy elim program
     1501  is_jump (nth i ? program 〈None ?,Comment []〉) →
     1502  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
     1503#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
    15621504[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1563 | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    1564   [ whd in match (measure_int ???) in Hm;
    1565     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) in Hm;
    1566     normalize nodelta
    1567     [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
    1568     | #j cases j normalize nodelta
     1505| #h #t #Hind #Hm #i #Hi #Hj
     1506  cases (le_to_or_lt_eq … Hi) -Hi
     1507  [ #Hi @Hind
     1508    [ whd in match (measure_int ???) in Hm;
     1509      cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
     1510      normalize nodelta
    15691511      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
    15701512      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    1571         <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
    1572         >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
    1573         >plus_n_Sm @le_n
    1574       | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
    1575       ]
    1576     ]
    1577   | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
    1578   [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
     1513        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
     1514      | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
     1515      ]
     1516    | @(le_S_S_to_le … Hi)
     1517    | @Hj
     1518    ]
    15791519  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    1580     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) in Hm;
     1520    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    15811521    normalize nodelta
    1582     [ #_ %1 @refl
    1583     | #j cases j normalize nodelta
    1584       [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
    1585         >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
    1586       | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
    1587         #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
    1588       | #_ %2 @refl
    1589       ]
    1590     ]
    1591   ]]
     1522    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
     1523    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
     1524      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
     1525    | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/
     1526    ]
     1527  ]
    15921528]
    15931529qed.
     
    15951531lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    15961532  ∀policy:Σp:ppc_pc_map.
    1597     out_of_program_none program p ∧ jump_in_policy program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
     1533    out_of_program_none program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
    15981534  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    15991535  [ None ⇒ True
     
    16121548     [ @(transitive_le … Hp) / by /
    16131549     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    1614        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp) #Hinc
    1615        cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉))
    1616        [ #Hj elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) ?) Hj)
    1617          [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (|t|) ?) Hj)
    1618            [ #j1 normalize nodelta
    1619              cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,None ?〉) in Hm Hinc; #x1 #x2
    1620              cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,None ?〉); #y1 #y2
    1621              #Hm #Hinc #Hx #Hy lapply Hm -Hm; lapply Hinc -Hinc; >Hx >Hy normalize nodelta
    1622              cases j1 cases j2 normalize nodelta
    1623              [1: / by /
    1624              |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    1625                lapply (measure_incr_or_equal program policy t ? 0)
    1626                [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    1627              |4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
    1628              |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
    1629                #_ #H @(injective_plus_r … H)
    1630              |6: >measure_plus >measure_plus
    1631                change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
    1632                #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    1633                lapply (measure_incr_or_equal program policy t ? 0)
    1634                [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    1635              |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
    1636                #_ #H @(injective_plus_r … H)
    1637              ]
    1638            | @(transitive_le … Hp) @le_n
    1639            ]
    1640          | @(transitive_le … Hp) @le_n
    1641          ]
    1642        | #Hnj lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (|t|) ?) Hnj)
    1643          [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) p (|t|) ?) Hnj)
    1644            [3: cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉) in Hm Hinc;
    1645                #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd p) 〈0,None ?〉)
    1646                #y1 #y2 #Hm #Hinc #Hy #Hx lapply Hm -Hm; lapply Hinc -Hinc; >Hx >Hy normalize nodelta
    1647                #_ / by /
    1648            |1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))))
    1649            |2: @(transitive_le … Hp) @le_n
    1650            ]
    1651         |1: @(proj1 ?? (proj1 ?? (pi2 ?? policy)))
    1652         |2: @(transitive_le … Hp) @le_n
    1653         ]
    1654       ]
    1655       | @(le_S_S_to_le … Hi)
     1550       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp) #Hinc
     1551       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2
     1552       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
     1553       #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
     1554       cases x2 cases y2 normalize nodelta
     1555       [1: / by /
     1556       |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
     1557         lapply (measure_incr_or_equal program policy t ? 0)
     1558         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
     1559       |4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
     1560       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
     1561         #_ #H @(injective_plus_r … H)
     1562       |6: >measure_plus >measure_plus
     1563         change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
     1564         #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
     1565         lapply (measure_incr_or_equal program policy t ? 0)
     1566         [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
     1567       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
     1568         #_ #H @(injective_plus_r … H)
     1569       ]
     1570     | @(le_S_S_to_le … Hi)
    16561571     ]
    16571572   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    16581573     whd in match (measure_int ? p ?) in Hm;
    1659      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
     1574     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp)
    16601575     (* XXX *) cases daemon
    16611576     (* change proof for not_jump
     
    17271642    And (match p with
    17281643      [ None ⇒ True
    1729       | Some pol ⇒ And (And (And (And (
     1644      | Some pol ⇒ And (And (
    17301645      (out_of_program_none program pol))
    1731       (jump_in_policy program pol))
    17321646      (policy_isize_sum program (create_label_map program) pol))
    1733       (policy_safe program (create_label_map program) pol))
    17341647      (policy_compact program (create_label_map program) pol)
    17351648      ])
     
    18681781] *)
    18691782qed.
    1870 *)
    18711783
    18721784(* The glue between Policy and Assembly. *)
     
    18831795        sigma ppc (\fst (fetch_pseudo_instruction (\snd program) ppc)))))
    18841796    = \fst (sigma (\snd (half_add ? ppc (bitvector_of_nat ? 1)))))
    1885 ≝ ?.
    1886 (*
    1887 λprogram.λppc:ℕ.
     1797≝ λprogram.
    18881798  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
    18891799  match policy with
    1890   [ None ⇒ 〈0, Some ? long_jump〉
    1891   | Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉
    1892   ].*)
     1800  [ None ⇒ None ?
     1801  | Some x ⇒ Some ?
     1802      «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     1803        〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
     1804  ].
    18931805 cases daemon
    18941806qed.
Note: See TracChangeset for help on using the changeset viewer.