Changeset 2211 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jul 18, 2012, 3:57:09 PM (7 years ago)
Author:
boender
Message:
  • finished proof of sigma specification
  • added some stuff to Util, as usual
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2153 r2211  
    1717        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
    1818        (sigma_compact_unsafe program (create_label_map program) x))
    19         (\fst x < 2^16)
     19        (\fst x 2^16)
    2020    ]) ≝
    2121 let labels ≝ create_label_map program in
     
    260260    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    261261    sigma_compact_unsafe program (create_label_map program) p ∧
    262     \fst p < 2^16.
     262    \fst p 2^16.
    263263  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    264264  match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with
     
    332332    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    333333    sigma_compact_unsafe program (create_label_map program) p ∧
    334     \fst p < 2^16.
     334    \fst p 2^16.
    335335  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    336336  [ None ⇒ True
     
    418418    match p with
    419419      [ None ⇒ True
    420       | Some pol ⇒ And (*And (out_of_program_none program pol)*)
    421       (sigma_compact program (create_label_map program) pol)
    422       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
     420      | Some pol ⇒ And (And (And
     421          (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
     422          (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉)))
     423          (sigma_compact program (create_label_map program) pol))
     424          (\fst pol ≤ 2^16)
    423425      ].
    424426#program @(\snd (jump_expansion_internal program (S (2*|program|))))
     
    441443      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
    442444      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
    443         @conj
    444         [ @(equal_compact_unsafe_compact ?? Fp)
     445        @conj [ @conj [ @conj
     446        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     447        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
     448        ]
     449        | @(equal_compact_unsafe_compact ?? Fp)
    445450          [ lapply (jump_pc_equal program (2*|program|))
    446451            >Feq >Geq normalize nodelta #H @H @Heq
    447           | cases daemon
     452          | cases daemon (* true, but have to add this to properties *)
    448453          | @(proj2 ?? (proj1 ?? HGp))
    449454          ]
    450         (*| @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
    451           >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq
    452           [ destruct (Geq) / by /
    453           | cases (jump_expansion_step program (create_label_map (pi1 ?? program)) «Fp,?») in Geq;
    454             #x cases x -x #Sch #So normalize nodelta cases So
    455             [ normalize nodelta #_ #ABS destruct (ABS)
    456             | -So normalize nodelta #Sp #HSp #Seq <(proj1 ?? (pair_destruct ?????? (pi1_eq ???? Seq)))
    457               cases Sch in HSp Seq; #HSp #Seq
    458               [ @refl
    459               | normalize nodelta in Seq; @(proj2 ?? (proj1 ?? HSp))
    460                 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Seq))))
    461                 @Heq
    462               ]
    463             ]
    464           ]
    465         ]*)
    466         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     455        ]
     456        | @(proj2 ?? HGp)
    467457        ]
    468458      ]
     
    552542      #z cases z -z #Gch #Go cases Go normalize nodelta
    553543      [ #HGp #Geq @I
    554       | -Go #Gp normalize nodelta #HGp #Geq @conj
    555         [ @(equal_compact_unsafe_compact ?? Fp)
     544      | -Go #Gp normalize nodelta #HGp #Geq @conj [ @conj [ @conj
     545        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     546        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
     547        ]
     548        | @(equal_compact_unsafe_compact ?? Fp)
    556549          [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
    557550            #H @H #i #Hi
     
    580573                >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
    581574              ]
    582             | cases daemon
     575            | cases daemon (* true, but have to add to properties in some way *)
    583576            | @(proj2 ?? (proj1 ?? HGp))
    584577            ]
    585           | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     578          ]
     579          | @(proj2 ?? HGp)
    586580          ]
    587581        ]
     
    608602include alias "basics/logic.ma".
    609603
     604lemma pc_increases: ∀i,j:ℕ.∀program.∀pol:Σp:ppc_pc_map.
     605  And (And (And
     606    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)
     607    (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
     608    (sigma_compact program (create_label_map program) p))
     609    (\fst p ≤ 2^16).i ≤ j → j ≤ |program| →
     610  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 i) (\snd pol) 〈0,short_jump〉) ≤
     611  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 j) (\snd pol) 〈0,short_jump〉).
     612 #i #j #program #pol #H elim (le_to_eq_plus … H) #n #Hn >Hn -Hn -j elim n
     613 [ <plus_n_O #_ @le_n
     614 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
     615   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (i+n) H)
     616   lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
     617   cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
     618   [ normalize nodelta #_ #abs cases abs
     619   | #x cases x -x #pc #jl #EQ normalize nodelta
     620     lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
     621     cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
     622     [ normalize nodelta #_ #abs cases abs
     623     | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
     624       >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     625       >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r
     626     ]
     627   ]
     628 ]
     629qed.
     630 
    610631(* The glue between Policy and Assembly. *)
    611632(*CSC: modified to really use the specification in Assembly.ma.*)
     
    630651#fpc #fpol #Hfpol
    631652@conj
    632 [ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
     653[ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
    633654  #x #y #Hx normalize nodelta >Hx / by refl/
    634 | cases daemon (* leaving this until stabilisation of sigma predicate *)
    635   (*#ppc #ppc_ok normalize nodelta @conj
    636   [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok)
     655| #ppc #ppc_ok normalize nodelta @conj
     656  [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok)
    637657    >bitvector_of_nat_inverse_nat_of_bitvector
    638658    lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
    639     [ normalize nodelta #_ #abs cases abs
    640     | #x cases x -x #x1 #y1 normalize nodelta #Hl_ppc
    641       >(plus_n_O (nat_of_bitvector 16 ppc)) >plus_n_Sm <add_bitvector_of_nat_plus
    642       >bitvector_of_nat_inverse_nat_of_bitvector
    643       lapply (refl ? (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol))
    644       cases (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol) in ⊢ (???% → %);
    645       [ normalize nodelta #_ #abs cases abs
    646       | #x cases x -x #x2 #y2 normalize nodelta #Hl_Sppc
    647         #Hcompact >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉)
    648         >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
    649         >add_bitvector_of_nat_plus whd in match (fetch_pseudo_instruction ???);
    650         >(nth_safe_nth … 〈None ?, Comment []〉)
    651         >Hcompact <plus_n_O
    652         cases (nth (nat_of_bitvector ? ppc) ? (\snd program) ?) #a #b normalize nodelta
    653         whd in match instruction_size; normalize nodelta
    654         whd in match assembly_1_pseudoinstruction; normalize nodelta
    655         whd in match expand_pseudo_instruction; normalize nodelta
    656         cases b
    657         [2,3,6: #p [3: #q] normalize nodelta @refl
    658         |4,5: #p normalize nodelta
    659           >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
    660           >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
    661           whd in match (create_label_map ?);
    662           cases (lookup ?? (bitvector_of_nat ?
    663           (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
    664           #z1 #z2 normalize nodelta @refl
     659    [ #Hl normalize nodelta #abs cases abs
     660    | #x cases x -x #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
     661      >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
     662      lapply (refl ? (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol))
     663      cases (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol) in ⊢ (???% → %);
     664      [ #Hl normalize nodelta #abs cases abs
     665      | #x cases x -x #Spc #Sjl #SHl normalize nodelta #Hcompact
     666        >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
     667        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
     668        >add_bitvector_of_nat_plus >Hcompact whd in match instruction_size;
     669        normalize nodelta whd in match assembly_1_pseudoinstruction;
     670        normalize nodelta whd in match expand_pseudo_instruction;
     671        normalize nodelta whd in match fetch_pseudo_instruction;
     672        normalize nodelta
     673        lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
     674        cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
     675        #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
     676        >Hli normalize nodelta cases instr
     677        [2,3,6: #x [3: #y] normalize nodelta %
     678        |4,5: #x normalize nodelta
     679          >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
     680          whd in match create_label_map; normalize nodelta
     681          >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
     682          cases (bvt_lookup … (bitvector_of_nat ?
     683           (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     684          #lpc #ljl normalize nodelta @refl
    665685        |1: #pi cases pi
    666686          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    667             [1,2,3,6,7,24,25: #p #q
    668             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #p]
    669             normalize nodelta @refl
    670           |9,10,11,12,13,14,15,16,17: [1,2,6,7: #p |3,4,5,8,9: #q #p] normalize nodelta
     687            [1,2,3,6,7,24,25: #x #y
     688            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     689            normalize nodelta %
     690          |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
    671691            whd in match expand_relative_jump; normalize nodelta
    672692            whd in match expand_relative_jump_internal; normalize nodelta
    673             >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
    674             >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
    675             whd in match (create_label_map ?);
    676             cases (lookup ?? (bitvector_of_nat ?
    677             (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
    678             #z1 #z2 normalize nodelta @refl
     693            >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
     694            whd in match create_label_map; normalize nodelta
     695            >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
     696            cases (bvt_lookup … (bitvector_of_nat ?
     697             (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     698            #lpc #ljl normalize nodelta %
    679699          ]
    680700        ]
    681701      ]
    682     ]
    683   | cases daemon (* XXX remains to be done *)
    684   ] *)
    685 ]
    686 qed.           
     702    ]
     703  | (* Basic proof scheme:
     704       - ppc < |snd program|, hence our instruction is in the program
     705       - either we are the last non-zero-size instruction, in which case we are
     706         either smaller than 2^16 (because the entire program is), or we are exactly
     707         2^16 and something weird happens
     708       - or we are not, in which case we are definitely smaller than 2^16 (by transitivity
     709         through the next non-zero instruction)
     710    *)
     711    elim (le_to_or_lt_eq … (proj2 ?? Hfpol)) #Hfpc
     712    [ %1 @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol)))
     713      lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
     714      >bitvector_of_nat_inverse_nat_of_bitvector
     715      lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
     716      [ normalize nodelta #_ #abs cases abs
     717      | #x cases x -x #pc #jl #EQ normalize nodelta
     718        lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
     719        cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
     720        [ normalize nodelta #_ #abs cases abs
     721        | #x cases x -x #Spc #Sjl #SEQ normalize nodelta whd in match instruction_size;
     722          normalize nodelta whd in match assembly_1_pseudoinstruction;
     723          normalize nodelta whd in match expand_pseudo_instruction;
     724          normalize nodelta whd in match fetch_pseudo_instruction;
     725          normalize nodelta
     726          lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
     727          cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
     728          #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
     729          >Hli normalize nodelta cases instr
     730          [2,3,6: #x [3: #y] normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     731            normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     732            [1,3,5: <H
     733              lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     734              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
     735            |2,4,6: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     736              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     737              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     738            ]
     739          |4,5: #x normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     740            normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     741            [1,3: <add_bitvector_of_nat_Sm in SEQ;
     742              >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
     743              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
     744              cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     745              #lpc #ljl normalize nodelta #H <H
     746              lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     747              <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
     748              >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
     749            |2,4: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     750              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     751              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     752            ]
     753          |1: #pi cases pi
     754            [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     755              [1,2,3,6,7,24,25: #x #y
     756              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     757              normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     758              normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     759              [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
     760                <H lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     761                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
     762              |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
     763                lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     764                >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     765                #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     766              ]
     767            |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x]
     768              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     769              normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     770              [1,3,5,7,9,11,13,15,17: <add_bitvector_of_nat_Sm in SEQ;
     771                >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
     772                whd in match expand_relative_jump; normalize nodelta
     773                whd in match expand_relative_jump_internal; normalize nodelta
     774                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
     775                cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     776                #lpc #ljl normalize nodelta #H <H
     777                lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     778                <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
     779                >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
     780              |2,4,6,8,10,12,14,16,18:
     781                lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     782                >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     783                #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     784              ]
     785            ]
     786          ]
     787        ]
     788      ]
     789    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
     790       * until the end of the program *)
     791      elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
     792      [ lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
     793        >bitvector_of_nat_inverse_nat_of_bitvector
     794        lapply (refl ? (lookup_opt … ppc fpol))
     795        cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
     796        [ #_ normalize nodelta #abs cases abs
     797        | #x cases x -x #pc #jl #EQ normalize nodelta
     798          lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
     799          cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
     800          [ #_ normalize nodelta #abs cases abs
     801          | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hc
     802            >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hpc normalize nodelta
     803            >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     804            >nat_of_bitvector_bitvector_of_nat_inverse
     805            [2: <Hfpc >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @Hpc ]
     806            elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
     807            [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
     808              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1
     809              >Hc in HSpc;
     810              whd in match create_label_map;
     811              whd in match fetch_pseudo_instruction; normalize nodelta
     812              >(nth_safe_nth … 〈None ?, Comment []〉)
     813              cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
     814              #lbl #ins normalize nodelta
     815              whd in match instruction_size;
     816              whd in match assembly_1_pseudoinstruction;
     817              whd in match expand_pseudo_instruction; normalize nodelta
     818              <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
     819              >add_commutative #SEQ cases ins
     820              [2,3,6: #x [3: #y] normalize nodelta #H @H
     821              |4,5: #x normalize nodelta
     822                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     823                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     824                cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     825                #lpc #ljl normalize nodelta #H @H
     826              |1: #pi cases pi
     827                [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     828                  [1,2,3,6,7,24,25: #x #y
     829                  |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     830                  normalize nodelta #H @H
     831                |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
     832                  whd in match expand_relative_jump;
     833                  whd in match expand_relative_jump_internal; normalize nodelta
     834                  >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     835                  >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     836                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     837                  #lpc #ljl normalize nodelta #H @H
     838                ]
     839              ]
     840            | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
     841              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj
     842              [ #ppc' #ppc_ok' #Hppc'
     843                (* S ppc < ppc' < |\snd program| *)
     844                (* lookup S ppc = 2^16 *)
     845                (* lookup |\snd program| = 2^16 *)
     846                (* lookup ppc' = 2^16 → instruction size = 0 *)
     847                lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok')
     848                >bitvector_of_nat_inverse_nat_of_bitvector
     849                lapply (refl ? (lookup_opt … ppc' fpol))
     850                cases (lookup_opt … ppc' fpol) in ⊢ (???% → %);
     851                [ normalize nodelta #_ #abs cases abs
     852                | normalize nodelta #x cases x -x #xpc #xjl #XEQ normalize nodelta
     853                  lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol))
     854                  cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol) in ⊢ (???% → %);
     855                  [ normalize nodelta #_ #abs cases abs
     856                  | normalize nodelta #x cases x -x #Sxpc #Sxjl #SXEQ normalize nodelta
     857                    #Hpcompact
     858                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
     859                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
     860                    lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
     861                    <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
     862                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
     863                    >bitvector_of_nat_inverse_nat_of_bitvector
     864                    >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
     865                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
     866                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
     867                    lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
     868                    <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
     869                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
     870                    >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
     871                    >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
     872                    @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
     873                    normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
     874                    cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
     875                    #lbl #ins normalize nodelta
     876                    whd in match instruction_size;
     877                    whd in match assembly_1_pseudoinstruction;
     878                    whd in match expand_pseudo_instruction; normalize nodelta
     879                    <add_bitvector_of_nat_Sm in SXEQ; >bitvector_of_nat_inverse_nat_of_bitvector
     880                    >add_commutative #SXEQ cases ins
     881                    [2,3,6: #x [3: #y] normalize nodelta #H @(sym_eq ??? H)
     882                    |4,5: #x normalize nodelta
     883                      >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
     884                      >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
     885                      cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     886                      #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
     887                    |1: #pi cases pi
     888                      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     889                        [1,2,3,6,7,24,25: #x #y
     890                        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
     891                          #H @(sym_eq ??? H)
     892                      |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
     893                        whd in match expand_relative_jump;
     894                        whd in match expand_relative_jump_internal; normalize nodelta
     895                        >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
     896                        >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
     897                        cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     898                        #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
     899                      ]
     900                    ]
     901                  ]
     902                ]
     903              | >Hc in Hspc;
     904                whd in match create_label_map;
     905                whd in match fetch_pseudo_instruction; normalize nodelta
     906                >(nth_safe_nth … 〈None ?, Comment []〉)
     907                cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
     908                 #lbl #ins normalize nodelta
     909                whd in match instruction_size;
     910                whd in match assembly_1_pseudoinstruction;
     911                whd in match expand_pseudo_instruction; normalize nodelta
     912                <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
     913                >add_commutative #SEQ cases ins
     914                [2,3,6: #x [3: #y] normalize nodelta #H @H
     915                |4,5: #x normalize nodelta
     916                  >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     917                  >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     918                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     919                  #lpc #ljl normalize nodelta #H @H
     920                |1: #pi cases pi
     921                  [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     922                    [1,2,3,6,7,24,25: #x #y
     923                    |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
     924                    #H @H
     925                  |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
     926                    whd in match expand_relative_jump;
     927                    whd in match expand_relative_jump_internal; normalize nodelta
     928                    >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     929                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     930                    cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     931                    #lpc #ljl normalize nodelta #H @H
     932                  ]
     933                ]
     934              ]
     935            ]
     936          ]
     937        ]
     938      | >bitvector_of_nat_inverse_nat_of_bitvector
     939        <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
     940        cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc %1 >Hpc
     941        >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
     942        <plus_O_n whd in match instruction_size; normalize nodelta
     943        lapply (refl ? (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?))
     944        [5: cases (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) in ⊢ (???% → %);
     945          #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
     946          #Hli >Hli
     947          lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
     948          [5: >Hass / by /
     949          ]
     950        ]
     951      ]
     952    ]
     953  ]
     954]
     955qed.
Note: See TracChangeset for help on using the changeset viewer.