Changeset 2235


Ignore:
Timestamp:
Jul 23, 2012, 9:22:02 PM (7 years ago)
Author:
sacerdot
Message:

Towards smaller proofs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2225 r2235  
    140140qed.
    141141
     142definition strip_target:
     143  preinstruction Identifier →
     144   ([[relative]] → preinstruction [[relative]]) ⊎ instruction ≝
     145  λi.
     146  match i with
     147  [ JC _ ⇒ inl … (JC ?)
     148  | JNC _ ⇒ inl … (JNC ?)
     149  | JB baddr _ ⇒ inl … (JB ? baddr)
     150  | JZ _ ⇒ inl … (JZ ?)
     151  | JNZ _ ⇒ inl … (JNZ ?)
     152  | JBC baddr _ ⇒ inl … (JBC ? baddr)
     153  | JNB baddr _ ⇒ inl … (JNB ? baddr)
     154  | CJNE addr _ ⇒ inl … (CJNE ? addr)
     155  | DJNZ addr _ ⇒ inl … (DJNZ ? addr)
     156  | ADD arg1 arg2 ⇒ inr … (ADD ? arg1 arg2)
     157  | ADDC arg1 arg2 ⇒ inr … (ADDC ? arg1 arg2)
     158  | SUBB arg1 arg2 ⇒ inr … (SUBB ? arg1 arg2)
     159  | INC arg ⇒ inr … (INC ? arg)
     160  | DEC arg ⇒ inr … (DEC ? arg)
     161  | MUL arg1 arg2 ⇒ inr … (MUL ? arg1 arg2)
     162  | DIV arg1 arg2 ⇒ inr … (DIV ? arg1 arg2)
     163  | DA arg ⇒ inr … (DA ? arg)
     164  | ANL arg ⇒ inr … (ANL ? arg)
     165  | ORL arg ⇒ inr … (ORL ? arg)
     166  | XRL arg ⇒ inr … (XRL ? arg)
     167  | CLR arg ⇒ inr … (CLR ? arg)
     168  | CPL arg ⇒ inr … (CPL ? arg)
     169  | RL arg ⇒ inr … (RL ? arg)
     170  | RR arg ⇒ inr … (RR ? arg)
     171  | RLC arg ⇒ inr … (RLC ? arg)
     172  | RRC arg ⇒ inr … (RRC ? arg)
     173  | SWAP arg ⇒ inr … (SWAP ? arg)
     174  | MOV arg ⇒ inr … (MOV ? arg)
     175  | MOVX arg ⇒ inr … (MOVX ? arg)
     176  | SETB arg ⇒ inr … (SETB ? arg)
     177  | PUSH arg ⇒ inr … (PUSH ? arg)
     178  | POP arg ⇒ inr … (POP ? arg)
     179  | XCH arg1 arg2 ⇒ inr … (XCH ? arg1 arg2)
     180  | XCHD arg1 arg2 ⇒ inr … (XCHD ? arg1 arg2)
     181  | RET ⇒ inr … (RET ?)
     182  | RETI ⇒ inr … (RETI ?)
     183  | NOP ⇒ inr … (RealInstruction (NOP ?))
     184  ].
     185
    142186definition expand_relative_jump_unsafe:
    143187  jump_length → preinstruction Identifier → list instruction ≝
    144188  λjmp_len:jump_length.λi.
    145   match i with
    146   [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
    147   | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)
    148   | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)
    149   | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)
    150   | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)
    151   | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)
    152   | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)
    153   | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)
    154   | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)
    155   | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
    156   | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
    157   | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]
    158   | INC arg ⇒ [ INC ? arg ]
    159   | DEC arg ⇒ [ DEC ? arg ]
    160   | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]
    161   | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]
    162   | DA arg ⇒ [ DA ? arg ]
    163   | ANL arg ⇒ [ ANL ? arg ]
    164   | ORL arg ⇒ [ ORL ? arg ]
    165   | XRL arg ⇒ [ XRL ? arg ]
    166   | CLR arg ⇒ [ CLR ? arg ]
    167   | CPL arg ⇒ [ CPL ? arg ]
    168   | RL arg ⇒ [ RL ? arg ]
    169   | RR arg ⇒ [ RR ? arg ]
    170   | RLC arg ⇒ [ RLC ? arg ]
    171   | RRC arg ⇒ [ RRC ? arg ]
    172   | SWAP arg ⇒ [ SWAP ? arg ]
    173   | MOV arg ⇒ [ MOV ? arg ]
    174   | MOVX arg ⇒ [ MOVX ? arg ]
    175   | SETB arg ⇒ [ SETB ? arg ]
    176   | PUSH arg ⇒ [ PUSH ? arg ]
    177   | POP arg ⇒ [ POP ? arg ]
    178   | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]
    179   | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]
    180   | RET ⇒ [ RET ? ]
    181   | RETI ⇒ [ RETI ? ]
    182   | NOP ⇒ [ RealInstruction (NOP ?) ]
    183   ].
    184 
    185 definition instruction_size_jmplen:
    186  jump_length → pseudo_instruction → ℕ ≝
     189  match strip_target i with
     190  [ inl jmp ⇒ expand_relative_jump_internal_unsafe jmp_len jmp
     191  | inr instr ⇒ [ instr ] ].
     192
     193definition expand_pseudo_instruction_unsafe:
     194 jump_length → pseudo_instruction → list instruction ≝
    187195  λjmp_len.
    188196  λi.
    189   let pseudos ≝ match i with
     197  match i with
    190198  [ Cost cost ⇒ [ ]
    191199  | Comment comment ⇒ [ ]
     
    205213    | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ]
    206214    ]
    207   ] in
    208   let mapped ≝ map ? ? assembly1 pseudos in
     215  ].
     216 %
     217qed.
     218
     219definition instruction_size_jmplen:
     220 jump_length → pseudo_instruction → ℕ ≝
     221  λjmp_len.
     222  λi.
     223  let mapped ≝ map ? ? assembly1 (expand_pseudo_instruction_unsafe jmp_len i) in
    209224  let flattened ≝ flatten ? mapped in
    210225  let pc_len ≝ length ? flattened in
    211226    pc_len.
    212  @I.
    213 qed.
    214227
    215228definition sigma_compact_unsafe ≝
     
    625638  #Hsafe #Hcp_unsafe #i #Hi
    626639  lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
    627   lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)))
    628   cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %);
     640  inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))
    629641  [ / by /
    630642  | #x cases x -x #x1 #x2 #EQ
     
    632644    [ / by /
    633645    | #y cases y -y #y1 #y2 normalize nodelta #H #H2
     646      (*CSC: make a lemma here; to shorten the proof, reimplement the
     647        safe case so that it also does a pattern matching on the jump_length
     648        type *)
    634649      cut (instruction_size_jmplen x2
    635650       (\snd (nth i ? program 〈None ?, Comment []〉)) =
     
    641656          whd in match (assembly_1_pseudoinstruction …);
    642657          whd in match (expand_pseudo_instruction …);
    643           normalize nodelta whd in match (append …) in H;
    644           lapply (refl ? (nth i ? program 〈None ?, Comment []〉)) lapply H
    645           cases (nth i ? program 〈None ?,Comment []〉) in ⊢ (% → ???% → %);
     658          normalize nodelta whd in match (append …) in H; lapply H
     659          inversion (nth i ? program 〈None ?,Comment []〉)
    646660          #lbl #instr cases instr
    647661          [2,3,6: #x [3: #y] normalize nodelta #H #_ %
    648           |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj #Heq
     662          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Heq #Hj
    649663            lapply (Hj x (refl ? x)) -Hj normalize nodelta
    650664            >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
     
    679693              ]
    680694              ]
    681             |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
     695            |2,3,5,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    682696              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    683               [1,3: cases (create_label_map program) #clm #Hclm
     697              [1,3,5,7: cases (create_label_map program) #clm #Hclm
    684698                @le_S_to_le @(proj2 ?? (Hclm x ?))
    685                 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    686                 |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
    687                 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
    688                   [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    689                 |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
     699                [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
     700                |3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
     701                [1,4,7,10: >nat_of_bitvector_bitvector_of_nat_inverse
     702                  [2,4,6,8: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     703                |2,5,8,11: whd in match fetch_pseudo_instruction; normalize nodelta
    690704                  >nth_safe_nth
    691                   [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
    692                     [1,3: >Heq / by refl/
    693                     |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
     705                  [1,3,5,7: >nat_of_bitvector_bitvector_of_nat_inverse
     706                    [1,3,5,7: >Heq / by refl/
     707                    |*: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    694708                    ]
    695709                  ]
    696                 |3,6: / by /
     710                |*: / by /
    697711                ]
    698               |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
     712              |*: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    699713              normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
    700714              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     
    703717              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    704718              cases (get_index' bool 2 0 flags) normalize nodelta
    705               #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
    706               ]
    707             |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    708               cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    709               [1,3: cases (create_label_map program) #clm #Hclm
    710                 @le_S_to_le @(proj2 ?? (Hclm x ?))
    711                 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
    712                 |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
    713                 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
    714                   [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    715                 |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
    716                   >nth_safe_nth
    717                   [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
    718                     [1,3: >Heq / by refl/
    719                     |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    720                     ]
    721                   ]
    722                 |3,6: / by /
    723                 ]
    724               |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    725               cases (vsplit bool 5 11 ?) #addr1 #addr2
    726               cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    727               cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    728               #result #flags normalize nodelta
    729               cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    730               cases (get_index' bool 2 0 flags) normalize nodelta
    731               #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
    732               ]
    733             ]
    734           |1: cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
     719              #H
     720              [1,2,5,6: >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
     721              |*: >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
     722              ]]]
     723          |1: normalize nodelta
     724              cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
    735725              [#A #B * / by refl/] #fst_foo
    736726              cut (∀x.
     
    749739                 | assumption ]] #lookup_in_program
    750740              -H #pi cases pi
    751               try (#y #x #H #Heq) try (#x #H #Heq) try (#H #Heq) try %
    752               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in H;
     741              try (#y #x #Heq #H) try (#x #Heq #H) try (#Heq #H) try % lapply H -H
     742              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    753743              #Hj lapply (Hj x (refl ? x)) -Hj
    754744              whd in match expand_relative_jump; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.