Changeset 2008


Ignore:
Timestamp:
May 30, 2012, 7:22:05 PM (5 years ago)
Author:
boender
Message:
  • substantial closing of holes in proof
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1973 r2008  
    1919definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝
    2020  λprefix.λsigma.
    21   ∀i:ℕ.i |prefix| → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?.
     21  ∀i:ℕ.i > |prefix| → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?.
    2222
    2323(* If instruction i is a jump, then there will be something in the policy at
     
    7070  ∀i:ℕ.i < |prefix| →
    7171  ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →
    72   \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump.
     72  \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd sigma) 〈0,short_jump〉) = short_jump.
    7373
    7474(* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
     
    118118 λprogram.λop.λp.
    119119 ∀i.i < |program| →
    120    let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in
    121    let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in
     120   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd op) 〈0,short_jump〉 in
     121   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉 in
    122122     (*opc ≤ pc ∧*) jmpleq oj j.
    123123
     
    245245qed.
    246246
    247 (* new safety condition: policy corresponds to program and resulting program is compact *)
    248 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
     247definition policy_compact_unsafe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    249248 λprogram.λlabels.λsigma.
    250  ∀n:ℕ.S n < |program| →
     249 ∀n:ℕ.n < |program| →
    251250  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
    252251  [ None ⇒ False
     
    255254    [ None ⇒ False
    256255    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    257        pc1 = instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
     256       pc1 = pc + instruction_size_jmplen j (\snd (nth n ? program 〈None ?, Comment []〉))
     257    ]
     258  ].
     259   
     260(* new safety condition: policy corresponds to program and resulting program is compact *)
     261definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
     262 λprogram.λlabels.λsigma.
     263 ∀n:ℕ.n < |program| →
     264  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
     265  [ None ⇒ False
     266  | Some x ⇒ let 〈pc,j〉 ≝ x in
     267    match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
     268    [ None ⇒ False
     269    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
     270       pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    258271         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    259272         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    260          (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉))
     273         (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))
    261274    ]
    262275  ].
     
    406419qed.
    407420
     421lemma nth_last: ∀A,a,l.
     422  nth (|l|) A l a = a.
     423 #A #a #l elim l
     424 [ / by /
     425 | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind
     426 ]
     427qed.
     428
    408429(* The first step of the jump expansion: everything to short. *)
    409430definition jump_expansion_start:
    410   ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     431  ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
    411432  ∀labels:label_map.
    412433  Σpolicy:option ppc_pc_map.
     
    414435    [ None ⇒ True
    415436    | Some p ⇒
    416        And (And (And (And (out_of_program_none (pi1 ?? program) p)
     437       And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p)
    417438       (jump_not_in_policy (pi1 ?? program) p))
    418        (policy_compact program labels p))
    419        (∀i.i < |program| →
    420          \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉) = short_jump))
     439       (policy_compact_unsafe program labels p))
     440       (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉))
     441       (∀i.i ≤ |program| → ∃pc.
     442         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
     443       (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) =
     444         Some ? 〈\fst p,short_jump〉))
    421445       (\fst p < 2^16)
    422446    ] ≝
     
    424448  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    425449  (λprefix.Σpolicy:ppc_pc_map.
    426     And (And (And (out_of_program_none prefix policy)
     450    And (And (And (And (And (out_of_program_none prefix policy)
    427451    (jump_not_in_policy prefix policy))
    428     (policy_compact prefix labels policy))
    429     (∀i.i < |prefix| →
    430       \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉) = short_jump))
     452    (policy_compact_unsafe prefix labels policy))
     453    (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))
     454    (∀i.i ≤ |prefix| → ∃pc.
     455      bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
     456    (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd policy) =
     457      Some ? 〈\fst policy,short_jump〉))
    431458  program
    432459  (λprefix.λx.λtl.λprf.λp.
    433    let 〈pc,sigma〉 ≝ p in
     460   let 〈pc,sigma〉 ≝ pi1 ?? p in
    434461   let 〈label,instr〉 ≝ x in
    435462   let isize ≝ instruction_size_jmplen short_jump instr in
    436    〈pc + isize, bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma〉
    437   ) 〈0, Stub ? ?〉 in
    438   if geb (\fst final_policy) 2^16 then
     463   〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉
     464  ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in
     465  if geb (\fst (pi1 ?? final_policy)) 2^16 then
    439466    None ?
    440467  else
     
    443470| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    444471  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    445 | @conj [ @conj [ @conj
     472| @conj [ @conj [ @conj [ @conj [ @conj
    446473  [ (* out_of_program_none *)
    447474    #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
     
    449476    cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
    450477    [ >lookup_opt_insert_miss
    451       [ @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     478      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i ? Hi2)
     479        @le_S_to_le @le_S_to_le @Hi
    452480      | @bitvector_of_nat_abs
    453481        [ @Hi2
     
    457485      ]
    458486    | >lookup_opt_insert_miss
    459       [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    460         >Hi @Hi2
     487      [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?)
     488        [ @le_S @le_n
     489        | >Hi @Hi2
     490        ]
    461491      | @bitvector_of_nat_abs
    462492        [ @Hi2
     
    466496      ]
    467497    ]
    468   | (* jump_not_in_policy *) #i >append_length <commutative_plus
    469     #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    470     [ cases p -p #p cases p -p #pc #sigma #Hp cases x #l #ins >lookup_insert_miss
    471       [ >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
     498  | (* jump_not_in_policy *) cases p -p #p cases p -p #pc #sigma #Hp
     499    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
     500    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     501    [ >lookup_insert_miss
     502      [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i ?)
     503        [ @Hi
     504        | >nth_append_first
     505          [ #H #H2 @H @H2
     506          | @Hi
     507          ]
     508        ]
    472509      | @bitvector_of_nat_abs
    473         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     510        [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <commutative_plus @le_S
    474511          @le_plus_a @Hi
     512        | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S
     513          @le_plus_n_r
     514        | @lt_to_not_eq @le_S_S @Hi
     515        ]
     516      ]
     517    | >Hi >lookup_insert_hit #_ @refl
     518    ]
     519  ]
     520  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
     521    cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta
     522    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     523    [ >lookup_opt_insert_miss
     524      [ >lookup_opt_insert_miss
     525        [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
     526          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
     527          cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
     528          [ #_ normalize nodelta / by /
     529          | #x cases x -x #pci #ji #EQi
     530            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma))
     531            cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %);
     532            [ #_ normalize nodelta / by /
     533            | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first
     534              [ / by /
     535              | @Hi
     536              ]
     537            ]
     538          ]
     539        ]
     540      ]
     541      [2: lapply (le_S_to_le … Hi) -Hi #Hi]
     542      @bitvector_of_nat_abs
     543      [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus
     544        @le_plus_a @Hi
     545      |2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
     546        @le_S_S @le_plus_n_r
     547      |3,6: @lt_to_not_eq @le_S_S @Hi
     548      ]
     549    | >lookup_opt_insert_miss
     550      [ >Hi >lookup_opt_insert_hit normalize nodelta
     551        >(proj2 ?? Hp) normalize nodelta >nth_append_second
     552        [ <minus_n_n whd in match (nth ????); @refl
     553        | @le_n
     554        ]
     555      | @bitvector_of_nat_abs
     556        [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus
     557          @le_plus_a @le_n
     558        | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
     559          @le_S_S @le_plus_n_r
     560        | @lt_to_not_eq @le_S_S >Hi @le_n
     561        ]
     562      ]
     563    ]
     564  ]
     565  | (* lookup 0 = 0 *)
     566    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     567    >lookup_opt_insert_miss
     568    [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp)))
     569    | @bitvector_of_nat_abs
     570      [ / by /
     571      | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
     572        @le_S_S @le_plus_n_r
     573      | @lt_to_not_eq / by /
     574      ]
     575    ]
     576  ]
     577  | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
     578    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     579    cases (le_to_or_lt_eq … Hi) -Hi #Hi
     580    [ >lookup_opt_insert_miss
     581      [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi))
     582      | @bitvector_of_nat_abs
     583        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus
     584          @le_plus_a @le_S_S_to_le @Hi
    475585        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    476           @le_plus_n_r
     586          @le_S_S @le_plus_n_r
    477587        | @lt_to_not_eq @Hi
    478588        ]
    479589      ]
    480     | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
    481       cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #ins
    482       >lookup_insert_hit #_ / by /
    483     ]
    484   ]
    485   | (* policy_compact *) cases daemon
    486   ]       
    487   | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
    488     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    489     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    490     [ >lookup_insert_miss
    491       [ @((proj2 ?? Hp) i Hi)
     590    | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr))
     591      @refl
     592    ]
     593  ]
     594  | (* lookup at the end *) cases p -p #p cases p -p #pc #sigma #Hp cases x
     595    #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit
     596    / by refl/
     597  ]
     598| @conj [ @conj [ @conj [ @conj [ @conj
     599  [ #i cases i
     600    [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
     601    | -i #i #Hi #Hi2 >lookup_opt_insert_miss
     602      [ / by refl/
    492603      | @bitvector_of_nat_abs
    493         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    494           @le_plus_a @Hi
    495         | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    496           @le_plus_n_r
    497         | @lt_to_not_eq @Hi
     604        [ @Hi2
     605        | / by /
     606        | @sym_neq @lt_to_not_eq / by /
    498607        ]
    499608      ]
    500     | >Hi >lookup_insert_hit @refl
    501     ]
    502   ]
    503 | @conj [ @conj [ @conj
    504   [ #i #_ #Hi2 / by refl/
    505   ]]]
    506   #i #H @⊥ @(absurd … H) @not_le_Sn_O
     609    ]
     610  | #i cases i
     611    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     612    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
     613    ]
     614  ]
     615  | #i cases i
     616    [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n
     617    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     618    ]
     619  ]
     620  | >lookup_opt_insert_hit @refl
     621  ]
     622  | #i cases i
     623    [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl
     624    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     625    ]
     626  ]
     627  | >lookup_opt_insert_hit @refl
     628  ]
    507629]
    508630qed.
     
    511633  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
    512634  (* \fst p1 = \fst p2 ∧ *)
    513   (∀n:ℕ.n < |program| →
     635  (∀n:ℕ.n |program| →
    514636    let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
    515637    let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
     
    519641  λprogram:list labelled_instruction.λp:ppc_pc_map.
    520642  ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →
    521   \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump).
     643  \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉) = long_jump).
    522644 
    523645(*include alias "common/Identifiers.ma".*)
     
    700822
    701823(* One step in the search for a jump expansion fixpoint. *)
    702 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     824definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
    703825  ∀labels:(Σlm:label_map.∀l.
    704826    occurs_exactly_once ?? l program →
     
    706828    address_of_word_labels_code_mem program l).
    707829  ∀old_policy:(Σpolicy:ppc_pc_map.
    708     And (And (out_of_program_none program policy)
     830    And (And (And (out_of_program_none program policy)
    709831    (jump_not_in_policy program policy))
     832    (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))
    710833    (\fst policy < 2^16)).
    711834  (Σx:bool × (option ppc_pc_map).
     
    713836    match y with
    714837    [ None ⇒ nec_plus_ultra program old_policy
    715     | Some p ⇒ And (And (And (And (And (out_of_program_none program p)
     838    | Some p ⇒ And (And (And (And (And (And (out_of_program_none program p)
    716839       (jump_not_in_policy program p))
    717840       (policy_increase program old_policy p))
    718841       (policy_compact program labels p))
     842       (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉))
    719843       (no_ch = true → policy_equal program old_policy p))
    720844       (\fst p < 2^16)
     
    723847  λprogram.λlabels.λold_sigma.
    724848  let 〈final_added, final_policy〉 ≝
    725     foldl_strong (option Identifier × pseudo_instruction)
     849    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    726850    (λprefix.Σx:ℕ × ppc_pc_map.
    727851      let 〈added,policy〉 ≝ x in
    728       And (And (And (And (out_of_program_none prefix policy)
     852      And (And (And (And (And (out_of_program_none prefix policy)
    729853      (jump_not_in_policy prefix policy))
    730854      (policy_increase prefix old_sigma policy))
    731       (policy_compact prefix labels policy))
     855      (policy_compact_unsafe prefix labels policy))
     856      (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))
    732857      (added = 0 → policy_equal prefix old_sigma policy))
    733858    program
     
    751876      ] in
    752877      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
    753       let 〈old_pc,old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉 in
     878      let 〈old_pc,old_length〉 ≝
     879        bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉 in
    754880      let old_size ≝ instruction_size_jmplen old_length instr in
    755881      let 〈new_length, isize〉 ≝ match add_instr with
     
    761887      | Some x ⇒ plus inc_added (minus isize old_size)
    762888      ] in
    763       〈new_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma〉〉
    764     ) 〈0, 〈0, Stub ??〉〉 in
     889      〈new_added, 〈plus inc_pc isize,
     890       bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc+isize, new_length〉 inc_sigma〉〉
     891    ) 〈0, 〈0, bvt_insert … (bitvector_of_nat 16 0) 〈0, short_jump〉 (Stub ??)〉〉) in
    765892    if geb (\fst final_policy) 2^16 then
    766893      〈eqb final_added 0, None ?〉
     
    771898  >H2 in H; normalize nodelta -H2 -x #H @conj
    772899  [ @conj
    773     [ @(proj1 ?? H)
     900    [ @conj
     901      [ @conj
     902        [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     903        | cases daemon (* XXX policy_compact_unsafe → policy_compact *)
     904        ]
     905      | @(proj2 ?? (proj1 ?? H))
     906      ]
    774907    | #H2 @(proj2 ?? H) @eqb_true_to_eq @H2
    775908    ]
    776909  | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
    777910  ]
    778 | lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
    779   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉))
    780   cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) in ⊢ (???% → %);
     911|4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
     912  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
     913  cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
    781914  #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
    782915  @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
    783   @conj [ @conj [ @conj [ @conj
     916  @conj [ @conj [ @conj [ @conj [ @conj
    784917  [ (* out_of_program_none *) #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
    785918    cases instr in Heq2; normalize nodelta
    786919    #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
    787     [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i ? Hi2)
     920    [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ? Hi2)
    788921      @le_S_to_le @Hi
    789922    |2,4,6,8,10,12: @bitvector_of_nat_abs
     
    794927    ]
    795928  | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;
    796     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    797     [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     929     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     930     [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    798931      [ >(nth_append_first ? i prefix ?? Hi)
    799         @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
     932        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i Hi)
    800933      | @bitvector_of_nat_abs
    801         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     934        [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length >commutative_plus
    802935          @le_plus_a @Hi
    803         | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     936        | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    804937          @le_plus_n_r
    805         | @lt_to_not_eq @Hi
     938        | @lt_to_not_eq @le_S_S @Hi
    806939        ]
    807940      ]
    808     | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit
    809       >nth_append_second
    810       [ <minus_n_n whd in match (nth ????); cases instr in Heq1;
    811         [4,5: #x #_ #H cases H #H2 @⊥ @H2 / by I/
    812         |2,3,6: #x [3: #y] #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by /
    813         |1: #pi cases pi
    814           [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:
    815             [1,2,3,6,7,24,25: #x #y
    816             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #Heq1
    817               <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by /
    818           |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    819             #_ #H @⊥ cases H #H2 @H2 / by I/
    820           ]
    821         ]
    822       | @le_n
    823       ]
    824     ]
    825   ]
     941     | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     942       cases instr in Heq1;
     943       [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     944       |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
     945         [1,3: <minus_n_n whd in match (nth ????); / by I/
     946         |2,4: @le_n
     947         ]
     948       |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
     949         [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:
     950           [1,2,3,6,7,24,25: #x #y
     951           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
     952             <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     953           |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
     954             #_ #H @⊥ cases H #H2 @H2 / by I/
     955           ]
     956         ]
     957       ]
     958     ]
    826959  | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
    827960    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi
    828     [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i Hi)
     961    [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
    829962      <(proj2 ?? (pair_destruct ?????? Heq2))     
    830963      @pair_elim #opc #oj #EQ1 >lookup_insert_miss
    831964      [ @pair_elim #pc #j #EQ2 / by /
    832965      | @bitvector_of_nat_abs
    833         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a
    834           @Hi
    835         | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    836         | @lt_to_not_eq @Hi
     966        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus
     967          @le_plus_a @Hi
     968        | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
     969        | @lt_to_not_eq @le_S_S @Hi
    837970        ]
    838971      ]
     
    860993            whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
    861994            #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    862             lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     995            lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    863996            [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    864997              >prf >nth_append_second
     
    8711004              >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    8721005            |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    873               cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     1006              cases (lookup ?? (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    8741007              #a #b #H >H normalize nodelta %2 @refl
    8751008            ]
     
    8781011          ]
    8791012        |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    880           lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     1013          lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    8811014          [1,4,7: >prf >nth_append_second
    8821015            [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     
    8841017            ]
    8851018          |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    886           |3,6,9: cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     1019          |3,6,9: cases (lookup ?? (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    8871020            #a #b #H >H normalize nodelta %2 @refl
    8881021          ]
     
    8921025    ]
    8931026  ]
    894   | (* policy_compact *) (*XXX*) cases daemon
    895   ]
     1027  | (* policy_compact_unsafe *) (*XXX*) cases daemon
     1028  ]
     1029  | (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_opt_insert_miss
     1030    [ @(proj2 ?? (proj1 ?? Hpolicy))
     1031    | @bitvector_of_nat_abs
     1032      [ / by /
     1033      | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
     1034        @le_S_S @le_plus_n_r
     1035      | @lt_to_not_eq / by /
     1036      ]
     1037    ]
     1038  ]
    8961039  | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy)
    8971040    lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
     
    9031046        #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
    9041047        #i >append_length >commutative_plus #Hi normalize in Hi;
    905         cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     1048        cases (le_to_or_lt_eq … Hi) -Hi #Hi
    9061049        [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:
    9071050          <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    9081051          [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:
    909             @(Hold Hadded i Hi)
     1052            @(Hold Hadded i (le_S_S_to_le … Hi))
    9101053          |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:
    9111054            @bitvector_of_nat_abs
    9121055            [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    9131056              @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    914               @le_plus_a @Hi
     1057              @le_S_S @le_plus_a @le_S_S_to_le @Hi
    9151058            |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    916               @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     1059              @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_S_S
    9171060              @le_plus_n_r
    9181061            |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
     
    9221065        |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:
    9231066           <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    924            lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     1067           lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    9251068           [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    9261069             >prf >nth_append_second
     
    9331076             >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    9341077           |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    935              cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     1078             cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    9361079             #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
    9371080           ]
     
    9401083         <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
    9411084         #H #i >append_length >commutative_plus #Hi normalize in Hi;
    942          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     1085         cases (le_to_or_lt_eq … Hi) -Hi #Hi
    9431086         [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
    9441087           >lookup_insert_miss
    945            [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)
     1088           [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_S_to_le … Hi))
    9461089             [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
    9471090           ]
    9481091           @bitvector_of_nat_abs
    9491092           [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    950              >append_length >commutative_plus @le_plus_a @Hi
     1093             >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi
    9511094           |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    952              >append_length <plus_n_Sm @le_S_S
     1095             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    9531096           |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
    954            ] @le_plus_n_r
     1097           ]
    9551098         |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
    9561099           >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
     
    9681111     |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
    9691112       #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
    970        cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     1113       cases (le_to_or_lt_eq …Hi) -Hi #Hi
    9711114       [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    972          [1,3,5: @(Hold Hadded i Hi)
     1115         [1,3,5: @(Hold Hadded i (le_S_S_to_le … Hi))
    9731116         |2,4,6: @bitvector_of_nat_abs
    9741117           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    975              @le_plus_a @Hi
    976            |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    977              @le_plus_n_r
     1118             @le_S_S @le_plus_a @le_S_S_to_le @Hi
     1119           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
     1120             @le_S_S @le_plus_n_r
    9781121           |3,6,9: @lt_to_not_eq @Hi
    9791122           ]
    9801123         ]
    9811124       |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    982          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     1125         lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    9831126         [1,4,7: >prf >nth_append_second
    9841127           [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
     
    9861129           ]
    9871130         |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    988          |3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     1131         |3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    9891132           #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
    9901133         ]
     
    9931136       <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
    9941137       #H #i >append_length >commutative_plus #Hi normalize in Hi;
    995        cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     1138       cases (le_to_or_lt_eq … Hi) -Hi #Hi
    9961139       [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    997          [1,3: @(Hold ? i Hi)
     1140         [1,3: @(Hold ? i (le_S_S_to_le … Hi))
    9981141           [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
    9991142         ]
    10001143         @bitvector_of_nat_abs
    10011144         [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    1002            >append_length >commutative_plus @le_plus_a @Hi
     1145           >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi
    10031146         |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    1004            >append_length <plus_n_Sm @le_S_S
     1147           >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    10051148         |3,6: @lt_to_not_eq @Hi
    1006          ] @le_plus_n_r
     1149         ]
    10071150         |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    10081151           <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta
     
    10181161       ]
    10191162     ]
    1020 | normalize nodelta @conj [ @conj [ @conj [ @conj
    1021   [ #i #Hi / by refl/
    1022   | / by refl/
    1023   ]]]]
    1024   [3: #_]
    1025   #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
     1163| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj
     1164  [ #i cases i
     1165    [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
     1166    | -i #i #Hi #Hi2 >lookup_opt_insert_miss
     1167      [ / by refl/
     1168      | @bitvector_of_nat_abs
     1169        [ @Hi2
     1170        | / by /
     1171        | @sym_neq @lt_to_not_eq / by /
     1172        ]
     1173      ]
     1174    ] 
     1175  | #i cases i
     1176    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1177    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
     1178    ]
     1179  ]
     1180  | #i cases i
     1181    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1182    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1183    ]
     1184  ]
     1185  | #i cases i
     1186    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1187    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1188    ]
     1189  ]
     1190  | >lookup_opt_insert_hit @refl
     1191  ]
     1192  | #_ #i cases i
     1193    [ #Hi >lookup_insert_hit
     1194      >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (pi2 ?? old_sigma))) 〈0,short_jump〉)
     1195      @refl
     1196    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1197    ]
     1198  ]
    10261199]
    10271200qed.
    10281201   
    1029 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ)
     1202let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (|l|)) 2^16) (n: ℕ)
    10301203  on n:(Σx:bool × (option ppc_pc_map).
    10311204    let 〈c,pol〉 ≝ x in
     
    10331206    [ None ⇒ True
    10341207    | Some x ⇒
    1035       And (And (And
     1208      And (And (And (And
    10361209        (out_of_program_none program x)
    10371210        (jump_not_in_policy program x))
    1038         (policy_compact program (create_label_map program) x))
     1211        (n > 0 → policy_compact program (create_label_map program) x))
     1212        (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd x) = Some ? 〈0,short_jump〉))
    10391213        (\fst x < 2^16)
    10401214    ]) ≝
     
    10511225  ].
    10521226[ normalize nodelta cases (jump_expansion_start program (create_label_map program))
    1053   #p cases p
     1227  #x cases x -x
    10541228  [ / by I/
    1055   | #pm normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
    1056   ]
     1229  | #sigma normalize nodelta #H @conj [ @conj [ @conj
     1230    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     1231    | #H @⊥ @(absurd ? H) @le_to_not_lt @le_n
     1232    ]
     1233    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     1234    ]
     1235    | @(proj2 ?? H) ]
     1236  ]
     1237| cases daemon
    10571238| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
    10581239| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta
    1059   #H @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
     1240  #H @conj [ @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) |  @(proj2 ?? (proj1 ?? H)) ] | @(proj2 ?? H) ]
    10601241| normalize nodelta cases (jump_expansion_step program labels «op,?»)
    10611242  #p cases p -p #p #r cases r normalize nodelta
     
    10631244  | #j #H @conj
    10641245    [ @conj
    1065       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     1246      [ @conj
     1247        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     1248        | cases daemon
     1249        ]
    10661250      | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    10671251      ]
     
    11581342qed.
    11591343
    1160 lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     1344lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
    11611345  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
    11621346   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
     
    11711355  #n (elim n) normalize /2 by S_pred/ qed.
    11721356 
    1173 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
     1357lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).∀n:ℕ.
    11741358  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
    11751359   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
     
    11921376 match program with
    11931377 [ nil      ⇒ acc
    1194  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with
     1378 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉)) with
    11951379   [ long_jump   ⇒ measure_int t policy (acc + 2)
    11961380   | medium_jump ⇒ measure_int t policy (acc + 1)
     
    12061390  [ / by refl/
    12071391  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    1208     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
     1392    cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉))
    12091393    [ normalize nodelta @Hd
    12101394    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     
    12201404[ normalize @le_n
    12211405| #h #t #Hind whd in match (measure_int ???);
    1222   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
     1406  cases (\snd (lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉))
    12231407  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    12241408  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
     
    12291413
    12301414(* uses the second part of policy_increase *)
    1231 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
     1415lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.S (|l|) <2^16.
    12321416  ∀policy:Σp:ppc_pc_map.
    12331417    out_of_program_none program p ∧
    1234     jump_not_in_policy program p ∧ \fst p < 2^16.
     1418    jump_not_in_policy program p ∧
     1419    lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉 ∧
     1420    \fst p < 2^16.
    12351421  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    1236   match \snd (jump_expansion_step program (create_label_map program) policy) with
     1422  match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with
    12371423  [ None   ⇒ True
    12381424  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
     
    12441430  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
    12451431  [ / by I/
    1246   | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))) (|t|) Hp)
     1432  | #x normalize nodelta #Hx #Hjeq
     1433    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) Hp)
    12471434    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    1248     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)
    1249     #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉)
    1250     #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2
     1435    cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
     1436    #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd x) 〈0,short_jump〉)
     1437    #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2 
    12511438    [1,4,5,7,8,9: #H cases H
    12521439    |2,3,6: #_ normalize nodelta
     
    12811468  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    12821469  is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
    1283   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
     1470  (\snd (bvt_lookup ?? (bitvector_of_nat ? (S i)) (\snd policy) 〈0,short_jump〉)) = long_jump.
    12841471#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
    12851472[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     
    12881475  [ #Hi @Hind
    12891476    [ whd in match (measure_int ???) in Hm;
    1290       cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
     1477      cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉)) in Hm;
    12911478      normalize nodelta
    12921479      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     
    12991486    ]
    13001487  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    1301     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
     1488    cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉)) in Hm;
    13021489    normalize nodelta
    13031490    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
     
    13111498
    13121499(* uses second part of policy_increase *)
    1313 lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     1500lemma measure_special: ∀program:(Σl:list labelled_instruction.(S (|l|)) < 2^16).
    13141501  ∀policy:Σp:ppc_pc_map.
    1315     out_of_program_none program p ∧ jump_not_in_policy program p ∧ \fst p < 2^16.
     1502    out_of_program_none program p ∧ jump_not_in_policy program p ∧
     1503    bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉 ∧
     1504    \fst p < 2^16.
    13161505  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    13171506  [ None ⇒ True
     
    13251514      measure_int x policy 0 = measure_int x p 0 →
    13261515      policy_equal x policy p) ?? (pi1 ?? program))
    1327  [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
     1516 [ #_ #_ #i #Hi <(le_n_O_to_eq … Hi)
     1517   >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (proj1 ?? Hpol))))
     1518   >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (pi2 ?? policy))))
     1519   / by refl/
    13281520 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    13291521   [ #Hi @Hind
    13301522     [ @(transitive_le … Hp) / by /
    13311523     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    1332        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp) #Hinc
    1333        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2
    1334        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
     1524       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp) #Hinc
     1525       cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2
     1526       cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉); #y1 #y2
    13351527       #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
    13361528       cases x2 cases y2 normalize nodelta
     
    13521544     | @(le_S_S_to_le … Hi)
    13531545     ]
    1354    | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
     1546   | #Hi >Hi whd in match (measure_int ???) in Hm;
    13551547     whd in match (measure_int ? p ?) in Hm;
    1356      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp)
    1357      cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
     1548     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
     1549     cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉) in Hm;
    13581550     #x1 #x2
    1359      cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
    1360      #y1 #y2 
     1551     cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉);
     1552     #y1 #y2
    13611553     normalize nodelta cases x2 cases y2 normalize nodelta
    13621554     [1,5,9: #_ #_ @refl
     
    13901582qed.
    13911583
    1392 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
     1584lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.S (|l|) < 2^16.
    13931585  match jump_expansion_start program (create_label_map program) with
    13941586  [ None ⇒ True
     
    14021594   [ / by refl/
    14031595   | #h #t #Hind #Hp whd in match (measure_int ???);
    1404      >(proj2 ?? (proj1 ?? Hpl) (|t|))
    1405      [ normalize nodelta @Hind ]
    1406      @(transitive_le … Hp) [ @le_n_Sn | @ le_n ]
     1596     elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (S (|t|)) Hp)
     1597     #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind
     1598     @(transitive_le … Hp) @le_n_Sn
    14071599   ]
    14081600 ]   
     
    14101602
    14111603(* the actual computation of the fixpoint *)
    1412 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     1604definition je_fixpoint: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
    14131605  Σp:option ppc_pc_map.
    14141606    And (match p with
    14151607      [ None ⇒ True
    14161608      | Some pol ⇒ And (out_of_program_none program pol)
    1417       (policy_compact program (create_label_map program) pol)
     1609      ((pi1 ?? program) ≠ [] → policy_compact program (create_label_map program) pol)
    14181610      ])
    14191611    (∃n.∀k.n < k →
     
    14241616    #c #pol #Hp cases pol
    14251617    [ normalize nodelta //
    1426     | #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
    1427     | cases daemon ] ]
     1618    | #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     1619    | #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? H))) cases (pi1 ?? program) in Hneq;
     1620      [ #H cases H #H @⊥ @H @refl
     1621      | #h #t #_ / by /
     1622      ] ]
     1623    ]
    14281624| cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
    14291625   (\snd (pi1 ?? (jump_expansion_internal program k)))
     
    14381634  | @equal_remains_equal
    14391635    [ @(proj2 ?? Hx)
    1440     | @le_S_S_to_le @le_S @(proj1 ?? Hx)
     1636    | @(proj1 ?? Hx)
    14411637    ]   
    14421638  ]
     
    14521648      >EQ normalize nodelta
    14531649      lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»))
    1454       [ @conj [ @(proj1 ?? (proj1 ?? HFp)) | @(proj2 ?? HFp) ]
     1650      [ @conj [ @conj
     1651      [ @(proj1 ?? (proj1 ?? (proj1 ?? HFp)))
     1652      | @(proj2 ?? (proj1 ?? HFp)) ]
     1653      | @(proj2 ?? HFp) ]
    14551654      | lapply (measure_full program Fp ?)
    14561655        [ @le_to_le_to_eq
     
    14891688                    [ cases (jump_expansion_internal program x) in Hxpol;
    14901689                      #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
    1491                       normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
    1492                     | lapply (Hfa x Hx) lapply HeqSxpol -HeqSxpol
     1690                      normalize nodelta #H @conj [ @conj
     1691                      [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     1692                      | @(proj2 ?? (proj1 ?? H)) ]
     1693                      | @(proj2 ?? H) ]
     1694                    | lapply (Hfa x (le_S_to_le … Hx)) lapply HeqSxpol -HeqSxpol
    14931695                      whd in match (jump_expansion_internal program (S x));
    14941696                      lapply (refl ? (jump_expansion_internal program x))
     
    14971699                      #H #Heq cases xch in Heq; #Heq normalize nodelta
    14981700                      [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    1499                         [ @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
     1701                        [ @conj [ @conj
     1702                          [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     1703                          | @(proj2 ?? (proj1 ?? H)) ]
     1704                          | @(proj2 ?? H) ]
    15001705                        | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    15011706                          normalize nodelta cases c normalize nodelta
     
    15041709                            [ / by /
    15051710                            | #H3 lapply (measure_special program «xpol,?»)
    1506                               [ @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
     1711                              [ @conj [ @conj
     1712                                [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     1713                                | @(proj2 ?? (proj1 ?? H)) ]
     1714                                | @(proj2 ?? H) ]
    15071715                              | >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull
    15081716                              ]
     
    15111719                        ]
    15121720                      | lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    1513                         [ @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
     1721                        [ @conj [ @conj
     1722                          [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     1723                          | @(proj2 ?? (proj1 ?? H)) ]
     1724                          | @(proj2 ?? H) ]
    15141725                        | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    15151726                          normalize nodelta cases c normalize nodelta
     
    15311742          [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
    15321743          | #Gp #HGp #EQ2 cases Fch
    1533             [ normalize nodelta #i #Hi
    1534               cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
    1535               [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi)
    1536                 lapply (Hfull i Hi Hj) cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    1537                 #fp #fj #Hfj >Hfj normalize nodelta
    1538                 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉) #gp #gj
    1539                 cases gj normalize nodelta
    1540                 [1,2: #H cases H #H2 cases H2 destruct (H2)
    1541                 |3: #_ @refl
     1744            [ normalize nodelta #i cases i
     1745              [ #_ >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? HFp)) 〈0,short_jump〉)
     1746                >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (proj1 ?? HGp))) 〈0,short_jump〉)
     1747                / by refl/
     1748              | -i #i #Hi
     1749                cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
     1750                [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi)
     1751                  lapply (Hfull i Hi Hj)
     1752                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Fp) 〈0,short_jump〉)
     1753                  #fp #fj #Hfj >Hfj normalize nodelta
     1754                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Gp) 〈0,short_jump〉)
     1755                  #gp #gj cases gj normalize nodelta
     1756                  [1,2: #H cases H #H2 cases H2 destruct (H2)
     1757                  |3: #_ @refl
     1758                  ]
     1759                | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi Hj)
     1760                  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
    15421761                ]
    1543               | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi Hj)
    1544                 >(proj2 ?? (proj1 ?? (proj1 ?? HFp)) i Hi Hj) @refl
    15451762              ]
    15461763            | normalize nodelta /2 by pe_int_refl/
     
    15601777    #H destruct (H)
    15611778  |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m
    1562       cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
    1563       #x1 #x2
    1564       cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
    1565       #y1 #y2 normalize nodelta
    1566       @dec_eq_jump_length 
     1779    cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
     1780    #x1 #x2
     1781    cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
     1782    #y1 #y2 normalize nodelta
     1783    @dec_eq_jump_length 
    15671784  ]
    15681785]
     
    15741791(* The glue between Policy and Assembly. *)
    15751792definition jump_expansion':
    1576 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
     1793∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
    15771794 option (Σsigma:Word → Word × bool.
    15781795   ∀ppc: Word.
Note: See TracChangeset for help on using the changeset viewer.