Changeset 2240 for src/ASM


Ignore:
Timestamp:
Jul 24, 2012, 11:40:43 AM (7 years ago)
Author:
sacerdot
Message:

All "interesting" technical lemmas singled out, proofs to be uncommented.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/PolicyStep.ma

    r2239 r2240  
    452452qed.
    453453
    454 (* One step in the search for a jump expansion fixpoint. *)
    455 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
    456   S (|l|) < 2^16 ∧ is_well_labelled_p l).
    457   ∀labels:(Σlm:label_map.∀l.
    458     occurs_exactly_once ?? l program →
    459     bitvector_of_nat ? (lookup_def … lm l 0) =
    460     address_of_word_labels_code_mem program l).
    461   ∀old_policy:(Σpolicy:ppc_pc_map.
    462     (* out_of_program_none program policy *)
    463     And (And (And (And (not_jump_default program policy)
    464     (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    465     (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
    466     (sigma_compact_unsafe program labels policy))
    467     (\fst policy ≤ 2^16)).
    468   (Σx:bool × (option ppc_pc_map).
    469     let 〈no_ch,y〉 ≝ x in
    470     match y with
    471     [ None ⇒ nec_plus_ultra program old_policy
    472     | Some p ⇒ And (And (And (And (And (And (And
    473        (not_jump_default program p)
    474        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    475        (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
    476        (jump_increase program old_policy p))
    477        (sigma_compact_unsafe program labels p))
    478        (sigma_jump_equal program old_policy p → no_ch = true))
    479        (no_ch = true → sigma_pc_equal program old_policy p))
    480        (\fst p ≤ 2^16)
    481     ])
    482     ≝
    483   λprogram.λlabels.λold_sigma.
    484   let 〈final_added, final_policy〉 ≝
    485     pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    486     (λprefix.Σx:ℕ × ppc_pc_map.
    487       let 〈added,policy〉 ≝ x in
    488       And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
    489       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    490       (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    491       (jump_increase prefix old_sigma policy))
    492       (sigma_compact_unsafe prefix labels policy))
    493       (sigma_jump_equal prefix old_sigma policy → added = 0))
    494       (added = 0 → sigma_pc_equal prefix old_sigma policy))
    495       (out_of_program_none prefix policy))
    496       (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
    497        \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
    498       (sigma_safe prefix labels added old_sigma policy))
    499     program
    500     (λprefix.λx.λtl.λprf.λacc.
    501       let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
    502       let 〈label,instr〉 ≝ x in
    503       (* Now, we must add the current ppc and its pc translation.
    504        * Three possibilities:
    505        *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
    506        *   - Instruction is a backward jump; we can use the sigma we're constructing,
    507        *     since it will already know the translation of its destination;
    508        *   - Instruction is a forward jump; we must use the old sigma (the new sigma
    509        *     does not know the translation yet), but compensate for the jumps we
    510        *     have lengthened.
    511        *)
    512       let add_instr ≝ match instr with
    513       [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    514       | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    515       | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
    516       | _             ⇒ None ?
    517       ] in
    518       let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
    519       let old_length ≝
    520         \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
    521       let old_size ≝ instruction_size_jmplen old_length instr in
    522       let 〈new_length, isize〉 ≝ match add_instr with
    523       [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
    524       | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
    525       ] in
    526       let new_added ≝ match add_instr with
    527       [ None   ⇒ inc_added
    528       | Some x ⇒ plus inc_added (minus isize old_size)
    529       ] in
    530       let old_Slength ≝
    531         \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
    532       let updated_sigma ≝
    533         (* we add the new PC to the next position and the new jump length to this one *)
    534         bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
    535         (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
    536       〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
    537     ) 〈0, 〈0,
    538       bvt_insert …
    539         (bitvector_of_nat ? 0)
    540         〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
    541         (Stub ??)〉〉
    542     ) in
    543     if gtb (\fst final_policy) 2^16 then
    544       〈eqb final_added 0, None ?〉
    545     else
    546       〈eqb final_added 0, Some ? final_policy〉.
    547 [ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
    548   #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
    549   (* USE: inc_pc = fst of policy (from fold) *)
    550   >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
    551   (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
    552   lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
    553   #Hsig #Hge
    554   (* USE: added = 0 → policy_pc_equal (from fold) *)
    555   lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|)))
    556   [ (* USE: policy_jump_equal → added = 0 (from fold) *)
    557     @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
    558     inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    559     [ #Hj
    560       (* USE: policy_increase (from fold) *)
    561       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
    562       lapply (Habs i Hi ?) [ >Hj %]
    563       cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
    564       #opc #oj
    565       cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
    566       #pc #j normalize nodelta #Heq >Heq cases j
    567       [1,2: #abs cases abs #abs2 try (cases abs2) @refl
    568       |3: #_ @refl
    569       ]
    570     | #Hnj
    571       (* USE: not_jump_default (from fold and old_sigma) *)
    572       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
    573       [2: >Hnj %]
    574       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
    575       >Hnj %
    576     ]
    577   | #abs >abs in Hsig; #Hsig
    578     @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
    579   ]
    580 | normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
    581   >H2 in H; normalize nodelta -H2 -x #H @conj
    582   [ @conj [ @conj
    583   [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
    584      * jump_increase, sigma_compact_unsafe (from fold) *)
    585     @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    586   | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
    587     @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
    588   ]
    589   | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
    590      #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
    591   ]
    592   | @not_lt_to_le @ltb_false_to_not_lt @p1
    593   ]
    594 |4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
    595   #inc_pc #inc_sigma #Hips
    596   inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    597   #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
    598   #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
    599   #Heq1 #Heq2
    600  cut (S (|prefix|) < 2^16)
    601  [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
    602    <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
    603  cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
    604  cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
    605   % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    606   (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    607    * commented out for full proofs, but this needs a lot of memory and time *)
    608   [ (* not_jump_default *)
    609     @(jump_expansion_step1 … Heq1 Heq2b) try assumption
    610     @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    611   | (* 0 ↦ 0 *)
    612     @(jump_expansion_step2 … Heq2b) try assumption
    613     [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    614     | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
    615   | (* inc_pc = fst of policy *)
    616     <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    617   | (* jump_increase *)
    618     @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
    619       … Heq1 prefix_ok1 prefix_ok Heq2b)
    620     try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    621     cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
    622   | (* sigma_compact_unsafe *)
    623     @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
    624     try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    625     try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))
    626     @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
    627   | (* policy_jump_equal → added = 0 *)
    628     @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
    629     try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
    630     @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    631   | (* added = 0 → policy_pc_equal *) cases daemon
     454lemma jump_expansion_step6:
     455(*
     456 program :
     457  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
     458 labels :
     459  (Σlm:label_map
     460   .(∀l:identifier ASMTag
     461     .occurs_exactly_once ASMTag pseudo_instruction l program
     462      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
     463       =address_of_word_labels_code_mem program l))*)
     464 ∀old_sigma : ppc_pc_map.(*
     465  (Σpolicy:ppc_pc_map
     466   .not_jump_default program policy
     467    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     468                 〈O,short_jump〉)
     469     =O
     470    ∧\fst  policy
     471     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
     472                  (\snd  policy) 〈O,short_jump〉)
     473    ∧sigma_compact_unsafe program labels policy
     474    ∧\fst  policy≤ 2 \sup 16 )*)
     475 ∀prefix : list (option Identifier×pseudo_instruction).(*
     476 x : (option Identifier×pseudo_instruction)
     477 tl : (list (option Identifier×pseudo_instruction))
     478 prf : (program=prefix@[x]@tl)
     479 acc :
     480  (Σx0:ℕ×ppc_pc_map
     481   .(let 〈added,policy〉 ≝x0 in 
     482     not_jump_default prefix policy
     483     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     484                  〈O,short_jump〉)
     485      =O
     486     ∧\fst  policy
     487      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     488                   (\snd  policy) 〈O,short_jump〉)
     489     ∧jump_increase prefix old_sigma policy
     490     ∧sigma_compact_unsafe prefix labels policy
     491     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     492     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     493     ∧out_of_program_none prefix policy
     494     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     495                  (\snd  policy) 〈O,short_jump〉)
     496      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     497                   (\snd  old_sigma) 〈O,short_jump〉)
     498       +added
     499     ∧sigma_safe prefix labels added old_sigma policy))
     500 inc_added : ℕ
     501 inc_pc_sigma : ppc_pc_map
     502 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     503 ∀label : option Identifier.
     504 ∀instr : pseudo_instruction.(*
     505 p1 : (x≃〈label,instr〉)
     506 add_instr ≝
     507  match instr
     508   in pseudo_instruction
     509   return λ_:pseudo_instruction.(option jump_length)
     510   with 
     511  [Instruction (i:(preinstruction Identifier))⇒
     512   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     513   (|prefix|) i
     514  |Comment (_:String)⇒None jump_length
     515  |Cost (_:costlabel)⇒None jump_length
     516  |Jmp (j:Identifier)⇒
     517   Some jump_length
     518   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     519  |Call (c:Identifier)⇒
     520   Some jump_length
     521   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     522  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     523 inc_pc : ℕ
     524 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
     525 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
     526 old_pc : ℕ
     527 old_length : jump_length
     528 Holdeq :
     529  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     530   〈O,short_jump〉
     531   =〈old_pc,old_length〉)
     532 Hpolicy :
     533  (not_jump_default prefix 〈inc_pc,inc_sigma〉
     534   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
     535                〈O,short_jump〉)
     536    =O
     537   ∧inc_pc
     538    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     539                 〈O,short_jump〉)
     540   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
     541   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
     542   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
     543   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
     544   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
     545   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     546                〈O,short_jump〉)
     547    =old_pc+inc_added
     548   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
     549 ∀added : ℕ.
     550 ∀policy : ppc_pc_map.(*
     551 new_length : jump_length
     552 isize : ℕ
     553 Heq1 :
     554  (match 
     555   match instr
     556    in pseudo_instruction
     557    return λ_:pseudo_instruction.(option jump_length)
     558    with 
     559   [Instruction (i:(preinstruction Identifier))⇒
     560    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     561    (|prefix|) i
     562   |Comment (_:String)⇒None jump_length
     563   |Cost (_:costlabel)⇒None jump_length
     564   |Jmp (j:Identifier)⇒
     565    Some jump_length
     566    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     567   |Call (c:Identifier)⇒
     568    Some jump_length
     569    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     570   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     571    in option
     572    return λ_0:(option jump_length).(jump_length×ℕ)
     573    with 
     574   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     575   |Some (pl:jump_length)⇒
     576    〈max_length old_length pl,
     577    instruction_size_jmplen (max_length old_length pl) instr〉]
     578   =〈new_length,isize〉)
     579 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
     580 prefix_ok : (|prefix|< 2 \sup 16 )
     581 Heq2a :
     582  (match 
     583   match instr
     584    in pseudo_instruction
     585    return λ_0:pseudo_instruction.(option jump_length)
     586    with 
     587   [Instruction (i:(preinstruction Identifier))⇒
     588    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     589    (|prefix|) i
     590   |Comment (_0:String)⇒None jump_length
     591   |Cost (_0:costlabel)⇒None jump_length
     592   |Jmp (j:Identifier)⇒
     593    Some jump_length
     594    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     595   |Call (c:Identifier)⇒
     596    Some jump_length
     597    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     598   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
     599    in option
     600    return λ_0:(option jump_length).ℕ
     601    with 
     602   [None⇒inc_added
     603   |Some (x0:jump_length)⇒
     604    inc_added+(isize-instruction_size_jmplen old_length instr)]
     605   =added)
     606 Heq2b :
     607  (〈inc_pc+isize,
     608   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     609   〈inc_pc+isize,
     610   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     611               (\snd  old_sigma) 〈O,short_jump〉)〉
     612   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     613    〈inc_pc,new_length〉 inc_sigma)〉
     614   =policy)
     615*)
     616 added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy.
     617cases daemon(*
    632618    (* USE[pass]: added = 0 → policy_pc_equal *)
    633     (* lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
     619    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    634620    <(proj2 ?? (pair_destruct ?????? Heq2))
    635621    <(proj1 ?? (pair_destruct ?????? Heq2))
    … …  
    928914        ]
    929915      ]
    930     ] *)
    931   | (* out_of_program_none *) cases daemon
    932     (* #i #Hi2 >append_length <commutative_plus @conj
     916    ]*)
     917qed.
     918
     919lemma jump_expansion_step7:
     920(*
     921 program :
     922  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
     923 labels :
     924  (Σlm:label_map
     925   .(∀l:identifier ASMTag
     926     .occurs_exactly_once ASMTag pseudo_instruction l program
     927      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
     928       =address_of_word_labels_code_mem program l))
     929 old_sigma :
     930  (Σpolicy:ppc_pc_map
     931   .not_jump_default program policy
     932    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     933                 〈O,short_jump〉)
     934     =O
     935    ∧\fst  policy
     936     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
     937                  (\snd  policy) 〈O,short_jump〉)
     938    ∧sigma_compact_unsafe program labels policy
     939    ∧\fst  policy≤ 2 \sup 16 )*)
     940 ∀prefix : list (option Identifier×pseudo_instruction).(*
     941 x : (option Identifier×pseudo_instruction)
     942 tl : (list (option Identifier×pseudo_instruction))
     943 prf : (program=prefix@[x]@tl)
     944 acc :
     945  (Σx0:ℕ×ppc_pc_map
     946   .(let 〈added,policy〉 ≝x0 in 
     947     not_jump_default prefix policy
     948     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     949                  〈O,short_jump〉)
     950      =O
     951     ∧\fst  policy
     952      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     953                   (\snd  policy) 〈O,short_jump〉)
     954     ∧jump_increase prefix old_sigma policy
     955     ∧sigma_compact_unsafe prefix labels policy
     956     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     957     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     958     ∧out_of_program_none prefix policy
     959     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     960                  (\snd  policy) 〈O,short_jump〉)
     961      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     962                   (\snd  old_sigma) 〈O,short_jump〉)
     963       +added
     964     ∧sigma_safe prefix labels added old_sigma policy))
     965 inc_added : ℕ
     966 inc_pc_sigma : ppc_pc_map
     967 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     968 ∀label : option Identifier.
     969 ∀instr : pseudo_instruction.(*
     970 p1 : (x≃〈label,instr〉)
     971 add_instr ≝
     972  match instr
     973   in pseudo_instruction
     974   return λ_:pseudo_instruction.(option jump_length)
     975   with 
     976  [Instruction (i:(preinstruction Identifier))⇒
     977   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     978   (|prefix|) i
     979  |Comment (_:String)⇒None jump_length
     980  |Cost (_:costlabel)⇒None jump_length
     981  |Jmp (j:Identifier)⇒
     982   Some jump_length
     983   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     984  |Call (c:Identifier)⇒
     985   Some jump_length
     986   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     987  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     988 inc_pc : ℕ
     989 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
     990 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
     991 old_pc : ℕ
     992 old_length : jump_length
     993 Holdeq :
     994  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     995   〈O,short_jump〉
     996   =〈old_pc,old_length〉)
     997 Hpolicy :
     998  (not_jump_default prefix 〈inc_pc,inc_sigma〉
     999   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
     1000                〈O,short_jump〉)
     1001    =O
     1002   ∧inc_pc
     1003    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     1004                 〈O,short_jump〉)
     1005   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
     1006   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
     1007   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
     1008   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
     1009   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
     1010   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     1011                〈O,short_jump〉)
     1012    =old_pc+inc_added
     1013   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)
     1014 added : ℕ*)
     1015 ∀policy : ppc_pc_map.(*
     1016 new_length : jump_length
     1017 isize : ℕ
     1018 Heq1 :
     1019  (match 
     1020   match instr
     1021    in pseudo_instruction
     1022    return λ_:pseudo_instruction.(option jump_length)
     1023    with 
     1024   [Instruction (i:(preinstruction Identifier))⇒
     1025    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1026    (|prefix|) i
     1027   |Comment (_:String)⇒None jump_length
     1028   |Cost (_:costlabel)⇒None jump_length
     1029   |Jmp (j:Identifier)⇒
     1030    Some jump_length
     1031    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1032   |Call (c:Identifier)⇒
     1033    Some jump_length
     1034    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1035   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     1036    in option
     1037    return λ_0:(option jump_length).(jump_length×ℕ)
     1038    with 
     1039   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     1040   |Some (pl:jump_length)⇒
     1041    〈max_length old_length pl,
     1042    instruction_size_jmplen (max_length old_length pl) instr〉]
     1043   =〈new_length,isize〉)
     1044 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
     1045 prefix_ok : (|prefix|< 2 \sup 16 )
     1046 Heq2a :
     1047  (match 
     1048   match instr
     1049    in pseudo_instruction
     1050    return λ_0:pseudo_instruction.(option jump_length)
     1051    with 
     1052   [Instruction (i:(preinstruction Identifier))⇒
     1053    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1054    (|prefix|) i
     1055   |Comment (_0:String)⇒None jump_length
     1056   |Cost (_0:costlabel)⇒None jump_length
     1057   |Jmp (j:Identifier)⇒
     1058    Some jump_length
     1059    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1060   |Call (c:Identifier)⇒
     1061    Some jump_length
     1062    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1063   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
     1064    in option
     1065    return λ_0:(option jump_length).ℕ
     1066    with 
     1067   [None⇒inc_added
     1068   |Some (x0:jump_length)⇒
     1069    inc_added+(isize-instruction_size_jmplen old_length instr)]
     1070   =added)
     1071 Heq2b :
     1072  (〈inc_pc+isize,
     1073   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     1074   〈inc_pc+isize,
     1075   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     1076               (\snd  old_sigma) 〈O,short_jump〉)〉
     1077   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1078    〈inc_pc,new_length〉 inc_sigma)〉
     1079   =policy)
     1080*)
     1081 out_of_program_none (prefix@[〈label,instr〉]) policy.
     1082cases daemon (*
     1083    #i #Hi2 >append_length <commutative_plus @conj
    9331084    [ (* → *) #Hi normalize in Hi;
    9341085      cases instr in Heq2; normalize nodelta
    … …  
    9661117        ]
    9671118      ]
    968     ] *)
    969   | (* lookup p = lookup old_sigma + added *) cases daemon
    970     (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
     1119    ]*)
     1120qed.
     1121
     1122lemma jump_expansion_step8:
     1123(*
     1124 program :
     1125  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
     1126 labels :
     1127  (Σlm:label_map
     1128   .(∀l:identifier ASMTag
     1129     .occurs_exactly_once ASMTag pseudo_instruction l program
     1130      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
     1131       =address_of_word_labels_code_mem program l))*)
     1132 ∀old_sigma : ppc_pc_map.(*
     1133  (Σpolicy:ppc_pc_map
     1134   .not_jump_default program policy
     1135    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     1136                 〈O,short_jump〉)
     1137     =O
     1138    ∧\fst  policy
     1139     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
     1140                  (\snd  policy) 〈O,short_jump〉)
     1141    ∧sigma_compact_unsafe program labels policy
     1142    ∧\fst  policy≤ 2 \sup 16 )*)
     1143 ∀prefix : list (option Identifier×pseudo_instruction).(*
     1144 x : (option Identifier×pseudo_instruction)
     1145 tl : (list (option Identifier×pseudo_instruction))
     1146 prf : (program=prefix@[x]@tl)
     1147 acc :
     1148  (Σx0:ℕ×ppc_pc_map
     1149   .(let 〈added,policy〉 ≝x0 in 
     1150     not_jump_default prefix policy
     1151     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     1152                  〈O,short_jump〉)
     1153      =O
     1154     ∧\fst  policy
     1155      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1156                   (\snd  policy) 〈O,short_jump〉)
     1157     ∧jump_increase prefix old_sigma policy
     1158     ∧sigma_compact_unsafe prefix labels policy
     1159     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     1160     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     1161     ∧out_of_program_none prefix policy
     1162     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1163                  (\snd  policy) 〈O,short_jump〉)
     1164      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1165                   (\snd  old_sigma) 〈O,short_jump〉)
     1166       +added
     1167     ∧sigma_safe prefix labels added old_sigma policy))
     1168 inc_added : ℕ
     1169 inc_pc_sigma : ppc_pc_map
     1170 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     1171 ∀label : option Identifier.
     1172 ∀instr : pseudo_instruction.(*
     1173 p1 : (x≃〈label,instr〉)
     1174 add_instr ≝
     1175  match instr
     1176   in pseudo_instruction
     1177   return λ_:pseudo_instruction.(option jump_length)
     1178   with 
     1179  [Instruction (i:(preinstruction Identifier))⇒
     1180   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1181   (|prefix|) i
     1182  |Comment (_:String)⇒None jump_length
     1183  |Cost (_:costlabel)⇒None jump_length
     1184  |Jmp (j:Identifier)⇒
     1185   Some jump_length
     1186   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1187  |Call (c:Identifier)⇒
     1188   Some jump_length
     1189   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1190  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     1191 inc_pc : ℕ
     1192 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
     1193 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
     1194 old_pc : ℕ
     1195 old_length : jump_length
     1196 Holdeq :
     1197  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     1198   〈O,short_jump〉
     1199   =〈old_pc,old_length〉)
     1200 Hpolicy :
     1201  (not_jump_default prefix 〈inc_pc,inc_sigma〉
     1202   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
     1203                〈O,short_jump〉)
     1204    =O
     1205   ∧inc_pc
     1206    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     1207                 〈O,short_jump〉)
     1208   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
     1209   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
     1210   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
     1211   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
     1212   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
     1213   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     1214                〈O,short_jump〉)
     1215    =old_pc+inc_added
     1216   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
     1217 ∀added : ℕ.
     1218 ∀policy : ppc_pc_map.(*
     1219 new_length : jump_length
     1220 isize : ℕ
     1221 Heq1 :
     1222  (match 
     1223   match instr
     1224    in pseudo_instruction
     1225    return λ_:pseudo_instruction.(option jump_length)
     1226    with 
     1227   [Instruction (i:(preinstruction Identifier))⇒
     1228    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1229    (|prefix|) i
     1230   |Comment (_:String)⇒None jump_length
     1231   |Cost (_:costlabel)⇒None jump_length
     1232   |Jmp (j:Identifier)⇒
     1233    Some jump_length
     1234    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1235   |Call (c:Identifier)⇒
     1236    Some jump_length
     1237    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1238   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     1239    in option
     1240    return λ_0:(option jump_length).(jump_length×ℕ)
     1241    with 
     1242   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     1243   |Some (pl:jump_length)⇒
     1244    〈max_length old_length pl,
     1245    instruction_size_jmplen (max_length old_length pl) instr〉]
     1246   =〈new_length,isize〉)
     1247 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
     1248 prefix_ok : (|prefix|< 2 \sup 16 )
     1249 Heq2a :
     1250  (match 
     1251   match instr
     1252    in pseudo_instruction
     1253    return λ_0:pseudo_instruction.(option jump_length)
     1254    with 
     1255   [Instruction (i:(preinstruction Identifier))⇒
     1256    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1257    (|prefix|) i
     1258   |Comment (_0:String)⇒None jump_length
     1259   |Cost (_0:costlabel)⇒None jump_length
     1260   |Jmp (j:Identifier)⇒
     1261    Some jump_length
     1262    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1263   |Call (c:Identifier)⇒
     1264    Some jump_length
     1265    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1266   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
     1267    in option
     1268    return λ_0:(option jump_length).ℕ
     1269    with 
     1270   [None⇒inc_added
     1271   |Some (x0:jump_length)⇒
     1272    inc_added+(isize-instruction_size_jmplen old_length instr)]
     1273   =added)
     1274 Heq2b :
     1275  (〈inc_pc+isize,
     1276   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     1277   〈inc_pc+isize,
     1278   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     1279               (\snd  old_sigma) 〈O,short_jump〉)〉
     1280   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1281    〈inc_pc,new_length〉 inc_sigma)〉
     1282   =policy)
     1283*)
     1284   \fst  (lookup (ℕ×jump_length) 16
     1285              (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  policy)
     1286              〈O,short_jump〉)
     1287  =\fst  (lookup (ℕ×jump_length) 16
     1288               (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  old_sigma)
     1289               〈O,short_jump〉)
     1290   +added.
     1291cases daemon(*
     1292    <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
    9711293    >lookup_insert_hit
    9721294    <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1;
    … …  
    10981420        ]
    10991421      ]
    1100     ] *)
    1101   | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
     1422    ]*)
     1423qed.
     1424
     1425lemma jump_expansion_step9:
     1426(*
     1427 program :
     1428  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
     1429 ∀labels : label_map.(*
     1430  (Σlm:label_map
     1431   .(∀l:identifier ASMTag
     1432     .occurs_exactly_once ASMTag pseudo_instruction l program
     1433      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
     1434       =address_of_word_labels_code_mem program l))*)
     1435 ∀old_sigma : ppc_pc_map.(*
     1436  (Σpolicy:ppc_pc_map
     1437   .not_jump_default program policy
     1438    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     1439                 〈O,short_jump〉)
     1440     =O
     1441    ∧\fst  policy
     1442     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
     1443                  (\snd  policy) 〈O,short_jump〉)
     1444    ∧sigma_compact_unsafe program labels policy
     1445    ∧\fst  policy≤ 2 \sup 16 )*)
     1446 ∀prefix : list (option Identifier×pseudo_instruction).(*
     1447 x : (option Identifier×pseudo_instruction)
     1448 tl : (list (option Identifier×pseudo_instruction))
     1449 prf : (program=prefix@[x]@tl)
     1450 acc :
     1451  (Σx0:ℕ×ppc_pc_map
     1452   .(let 〈added,policy〉 ≝x0 in 
     1453     not_jump_default prefix policy
     1454     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     1455                  〈O,short_jump〉)
     1456      =O
     1457     ∧\fst  policy
     1458      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1459                   (\snd  policy) 〈O,short_jump〉)
     1460     ∧jump_increase prefix old_sigma policy
     1461     ∧sigma_compact_unsafe prefix labels policy
     1462     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     1463     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     1464     ∧out_of_program_none prefix policy
     1465     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1466                  (\snd  policy) 〈O,short_jump〉)
     1467      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1468                   (\snd  old_sigma) 〈O,short_jump〉)
     1469       +added
     1470     ∧sigma_safe prefix labels added old_sigma policy))
     1471 inc_added : ℕ
     1472 inc_pc_sigma : ppc_pc_map
     1473 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     1474 ∀label : option Identifier.
     1475 ∀instr : pseudo_instruction.(*
     1476 p1 : (x≃〈label,instr〉)
     1477 add_instr ≝
     1478  match instr
     1479   in pseudo_instruction
     1480   return λ_:pseudo_instruction.(option jump_length)
     1481   with 
     1482  [Instruction (i:(preinstruction Identifier))⇒
     1483   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1484   (|prefix|) i
     1485  |Comment (_:String)⇒None jump_length
     1486  |Cost (_:costlabel)⇒None jump_length
     1487  |Jmp (j:Identifier)⇒
     1488   Some jump_length
     1489   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1490  |Call (c:Identifier)⇒
     1491   Some jump_length
     1492   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1493  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     1494 inc_pc : ℕ
     1495 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
     1496 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
     1497 old_pc : ℕ
     1498 old_length : jump_length
     1499 Holdeq :
     1500  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     1501   〈O,short_jump〉
     1502   =〈old_pc,old_length〉)
     1503 Hpolicy :
     1504  (not_jump_default prefix 〈inc_pc,inc_sigma〉
     1505   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
     1506                〈O,short_jump〉)
     1507    =O
     1508   ∧inc_pc
     1509    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     1510                 〈O,short_jump〉)
     1511   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
     1512   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
     1513   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
     1514   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
     1515   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
     1516   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     1517                〈O,short_jump〉)
     1518    =old_pc+inc_added
     1519   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
     1520 ∀added : ℕ.
     1521 ∀policy : ppc_pc_map.(*
     1522 new_length : jump_length
     1523 isize : ℕ
     1524 Heq1 :
     1525  (match 
     1526   match instr
     1527    in pseudo_instruction
     1528    return λ_:pseudo_instruction.(option jump_length)
     1529    with 
     1530   [Instruction (i:(preinstruction Identifier))⇒
     1531    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1532    (|prefix|) i
     1533   |Comment (_:String)⇒None jump_length
     1534   |Cost (_:costlabel)⇒None jump_length
     1535   |Jmp (j:Identifier)⇒
     1536    Some jump_length
     1537    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1538   |Call (c:Identifier)⇒
     1539    Some jump_length
     1540    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1541   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     1542    in option
     1543    return λ_0:(option jump_length).(jump_length×ℕ)
     1544    with 
     1545   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     1546   |Some (pl:jump_length)⇒
     1547    〈max_length old_length pl,
     1548    instruction_size_jmplen (max_length old_length pl) instr〉]
     1549   =〈new_length,isize〉)
     1550 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
     1551 prefix_ok : (|prefix|< 2 \sup 16 )
     1552 Heq2a :
     1553  (match 
     1554   match instr
     1555    in pseudo_instruction
     1556    return λ_0:pseudo_instruction.(option jump_length)
     1557    with 
     1558   [Instruction (i:(preinstruction Identifier))⇒
     1559    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     1560    (|prefix|) i
     1561   |Comment (_0:String)⇒None jump_length
     1562   |Cost (_0:costlabel)⇒None jump_length
     1563   |Jmp (j:Identifier)⇒
     1564    Some jump_length
     1565    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1566   |Call (c:Identifier)⇒
     1567    Some jump_length
     1568    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1569   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
     1570    in option
     1571    return λ_0:(option jump_length).ℕ
     1572    with 
     1573   [None⇒inc_added
     1574   |Some (x0:jump_length)⇒
     1575    inc_added+(isize-instruction_size_jmplen old_length instr)]
     1576   =added)
     1577 Heq2b :
     1578  (〈inc_pc+isize,
     1579   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     1580   〈inc_pc+isize,
     1581   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     1582               (\snd  old_sigma) 〈O,short_jump〉)〉
     1583   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     1584    〈inc_pc,new_length〉 inc_sigma)〉
     1585   =policy)
     1586*)
     1587 sigma_safe (prefix@[〈label,instr〉]) labels added old_sigma policy.
     1588cases daemon(*
     1589    #i >append_length >commutative_plus #Hi normalize in Hi;
    11021590    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    11031591    [ >nth_append_first [2: @Hi]
    … …  
    11171605                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
    11181606                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
    1119                     [1,4,7: *)
    1120                  
    1121   ]       
     1607                    [1,4,7:
     1608*)
     1609qed.
     1610
     1611(* One step in the search for a jump expansion fixpoint. *)
     1612definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
     1613  S (|l|) < 2^16 ∧ is_well_labelled_p l).
     1614  ∀labels:(Σlm:label_map.∀l.
     1615    occurs_exactly_once ?? l program →
     1616    bitvector_of_nat ? (lookup_def … lm l 0) =
     1617    address_of_word_labels_code_mem program l).
     1618  ∀old_policy:(Σpolicy:ppc_pc_map.
     1619    (* out_of_program_none program policy *)
     1620    And (And (And (And (not_jump_default program policy)
     1621    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
     1622    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
     1623    (sigma_compact_unsafe program labels policy))
     1624    (\fst policy ≤ 2^16)).
     1625  (Σx:bool × (option ppc_pc_map).
     1626    let 〈no_ch,y〉 ≝ x in
     1627    match y with
     1628    [ None ⇒ nec_plus_ultra program old_policy
     1629    | Some p ⇒ And (And (And (And (And (And (And
     1630       (not_jump_default program p)
     1631       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
     1632       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
     1633       (jump_increase program old_policy p))
     1634       (sigma_compact_unsafe program labels p))
     1635       (sigma_jump_equal program old_policy p → no_ch = true))
     1636       (no_ch = true → sigma_pc_equal program old_policy p))
     1637       (\fst p ≤ 2^16)
     1638    ])
     1639    ≝
     1640  λprogram.λlabels.λold_sigma.
     1641  let 〈final_added, final_policy〉 ≝
     1642    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
     1643    (λprefix.Σx:ℕ × ppc_pc_map.
     1644      let 〈added,policy〉 ≝ x in
     1645      And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
     1646      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
     1647      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
     1648      (jump_increase prefix old_sigma policy))
     1649      (sigma_compact_unsafe prefix labels policy))
     1650      (sigma_jump_equal prefix old_sigma policy → added = 0))
     1651      (added = 0 → sigma_pc_equal prefix old_sigma policy))
     1652      (out_of_program_none prefix policy))
     1653      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
     1654       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
     1655      (sigma_safe prefix labels added old_sigma policy))
     1656    program
     1657    (λprefix.λx.λtl.λprf.λacc.
     1658      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
     1659      let 〈label,instr〉 ≝ x in
     1660      (* Now, we must add the current ppc and its pc translation.
     1661       * Three possibilities:
     1662       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
     1663       *   - Instruction is a backward jump; we can use the sigma we're constructing,
     1664       *     since it will already know the translation of its destination;
     1665       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
     1666       *     does not know the translation yet), but compensate for the jumps we
     1667       *     have lengthened.
     1668       *)
     1669      let add_instr ≝ match instr with
     1670      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1671      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1672      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     1673      | _             ⇒ None ?
     1674      ] in
     1675      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
     1676      let old_length ≝
     1677        \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
     1678      let old_size ≝ instruction_size_jmplen old_length instr in
     1679      let 〈new_length, isize〉 ≝ match add_instr with
     1680      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
     1681      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
     1682      ] in
     1683      let new_added ≝ match add_instr with
     1684      [ None   ⇒ inc_added
     1685      | Some x ⇒ plus inc_added (minus isize old_size)
     1686      ] in
     1687      let old_Slength ≝
     1688        \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
     1689      let updated_sigma ≝
     1690        (* we add the new PC to the next position and the new jump length to this one *)
     1691        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
     1692        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
     1693      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
     1694    ) 〈0, 〈0,
     1695      bvt_insert …
     1696        (bitvector_of_nat ? 0)
     1697        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
     1698        (Stub ??)〉〉
     1699    ) in
     1700    if gtb (\fst final_policy) 2^16 then
     1701      〈eqb final_added 0, None ?〉
     1702    else
     1703      〈eqb final_added 0, Some ? final_policy〉.
     1704[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
     1705  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
     1706  (* USE: inc_pc = fst of policy (from fold) *)
     1707  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
     1708  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
     1709  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
     1710  #Hsig #Hge
     1711  (* USE: added = 0 → policy_pc_equal (from fold) *)
     1712  lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|)))
     1713  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
     1714    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
     1715    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     1716    [ #Hj
     1717      (* USE: policy_increase (from fold) *)
     1718      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
     1719      lapply (Habs i Hi ?) [ >Hj %]
     1720      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
     1721      #opc #oj
     1722      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
     1723      #pc #j normalize nodelta #Heq >Heq cases j
     1724      [1,2: #abs cases abs #abs2 try (cases abs2) @refl
     1725      |3: #_ @refl
     1726      ]
     1727    | #Hnj
     1728      (* USE: not_jump_default (from fold and old_sigma) *)
     1729      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
     1730      [2: >Hnj %]
     1731      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
     1732      >Hnj %
     1733    ]
     1734  | #abs >abs in Hsig; #Hsig
     1735    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
     1736  ]
     1737| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
     1738  >H2 in H; normalize nodelta -H2 -x #H @conj
     1739  [ @conj [ @conj
     1740  [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
     1741     * jump_increase, sigma_compact_unsafe (from fold) *)
     1742    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     1743  | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
     1744    @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
     1745  ]
     1746  | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
     1747     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
     1748  ]
     1749  | @not_lt_to_le @ltb_false_to_not_lt @p1
     1750  ]
     1751|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
     1752  #inc_pc #inc_sigma #Hips
     1753  inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
     1754  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
     1755  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
     1756  #Heq1 #Heq2
     1757 cut (S (|prefix|) < 2^16)
     1758 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
     1759   <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
     1760 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
     1761 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
     1762  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
     1763  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
     1764   * commented out for full proofs, but this needs a lot of memory and time *)
     1765  [ (* not_jump_default *)
     1766    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
     1767    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
     1768  | (* 0 ↦ 0 *)
     1769    @(jump_expansion_step2 … Heq2b) try assumption
     1770    [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
     1771    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
     1772  | (* inc_pc = fst of policy *)
     1773    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
     1774  | (* jump_increase *)
     1775    @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
     1776      … Heq1 prefix_ok1 prefix_ok Heq2b)
     1777    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     1778    cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
     1779  | (* sigma_compact_unsafe *)
     1780    @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
     1781    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1782    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))
     1783    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     1784  | (* policy_jump_equal → added = 0 *)
     1785    @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
     1786    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
     1787    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1788  | (* added = 0 → policy_pc_equal *) cases daemon (*
     1789    @(jump_expansion_step6 … Heq1 … Heq2b) try assumption
     1790    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
     1791    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1792    *)
     1793  | (* out_of_program_none *) cases daemon(*
     1794    @jump_expansion_step7 try assumption
     1795    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))))
     1796    *)
     1797  | (* lookup p = lookup old_sigma + added *) cases daemon(*
     1798    @jump_expansion_step8 try assumption
     1799    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))   
     1800    @(proj2 ?? (proj1 ?? Hpolicy)) *)
     1801  | (* sigma_safe *) cases daemon (*
     1802    @jump_expansion_step9 try assumption
     1803    @(proj2 ?? Hpolicy) *)
     1804  ]     
    11221805| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    11231806  [ #i cases i
Note: See TracChangeset for help on using the changeset viewer.