Changeset 2152 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jul 4, 2012, 1:23:00 PM (7 years ago)
Author:
boender
Message:
  • this should compile
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2141 r2152  
    1212    [ None ⇒ True
    1313    | Some x ⇒
    14       And (And (And (And (And
    15         (out_of_program_none program x)
    16         (not_jump_default program x))
     14      And (And (And (And
     15        (not_jump_default program x)
    1716        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
    1817        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
    19         (\fst x < 2^16))
    20         (no_ch = true → sigma_compact program (create_label_map program) x)
     18        (sigma_compact_unsafe program (create_label_map program) x))
     19        (\fst x < 2^16)
    2120    ]) ≝
    2221 let labels ≝ create_label_map program in
     
    3433  #x cases x -x
    3534  [ #H / by I/
    36   | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
    37     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    38     | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    39     ]
    40     | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     35  | #sigma normalize nodelta #H @conj [ @conj
     36    [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     37    | (* #Ht destruct (Ht) *) @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    4138    ]
    4239    | @(proj2 ?? H)
    43     ]
    44     | #H destruct (H)
    4540    ]
    4641  ]
     
    5146    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
    5247    [ #_ / by I/
    53     | #j2 #H2 @conj [ @conj [ @conj [ @conj
    54       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
    55       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
    56       ]
    57       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    58       ]     
     48    | #j2 #H2 @conj [ @conj
     49      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
     50      | (*#Ht @(equal_compact_unsafe_compact ?? op)
     51        [ @(proj2 ?? (proj1 ?? H2)) @Ht
     52        | cases daemon (* add sigma_safe to properties *)
     53        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     54        ]*)
     55        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     56      ]
    5957      | @(proj2 ?? H2)
    6058      ]
    61       | #Ht @(equal_compact_unsafe_compact ?? op)
    62         [ @(proj2 ?? (proj1 ?? (proj1 ?? H2))) @Ht
    63         | cases daemon (* add to invvariants *)
    64         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
    65         ]
    66       ]
    6759    ]
    6860  ]
     
    7163  [ #_ >p2 #ABS destruct (ABS)
    7264  | #map >p2 normalize nodelta
    73     #H #eq destruct (eq) cases daemon (* change order *)
     65    #H #eq destruct (eq) @H
    7466  ]
    7567]
     
    396388    match p with
    397389      [ None ⇒ True
    398       | Some pol ⇒ And (And (out_of_program_none program pol)
    399       (sigma_compact program (create_label_map program) pol))
     390      | Some pol ⇒ And (*And (out_of_program_none program pol)*)
     391      (sigma_compact program (create_label_map program) pol)
    400392      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
    401393      ].
     
    419411      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
    420412      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
    421         @conj [ @conj
    422         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))
    423         | @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
     413        @conj
     414        [ @(equal_compact_unsafe_compact ?? Fp)
     415          [ cases daemon
     416          | cases daemon
     417          | @(proj2 ?? (proj1 ?? HGp))
     418          ]
     419        (*| @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
    424420          >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq
    425421          [ destruct (Geq) / by /
     
    436432            ]
    437433          ]
     434        ]*)
     435        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
    438436        ]
    439         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
    440         ]
    441437      ]
    442438    ]
     
    525521      >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq
    526522      normalize nodelta
    527       [ @conj [ @conj
    528         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))))
    529         | @((proj2 ?? HFp) (refl ? true)) ]
     523      [ @conj
     524        [ cases daemon (* XXX *)
    530525        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
    531526        ]
    532527      | cases (jump_expansion_step ???); #z cases z -z #stch #sto cases sto
    533528        [ #_ / by I/
    534         | -sto #stp normalize nodelta #Hstp @conj [ @conj
    535           [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))))
    536           | @(equal_compact_unsafe_compact ?? Fp)
    537             [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp))
     529        | -sto #stp normalize nodelta #Hstp @conj
     530          [ @(equal_compact_unsafe_compact ?? Fp)
     531            [ @(proj2 ?? (proj1 ?? Hstp)) @(proj2 ?? (proj1 ?? (proj1 ?? Hstp)))
    538532              #i #Hi
    539533              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     
    548542                |3: #_ @refl
    549543                ]
    550               | #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)
    551                 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
     544              | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i Hi Hj)
     545                >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
    552546              ]
    553547            | cases daemon 
    554548            | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))
    555549            ]
     550          | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))
    556551          ]
    557         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))) ]
    558552        ]
    559553      ]
     
    583577(*CSC: modified to really use the specification in Assembly.ma.*)
    584578definition jump_expansion':
    585 ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
     579∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    586580 option (Σsigma_policy:(Word → Word) × (Word → bool).
    587581   let 〈sigma,policy〉≝ sigma_policy in
     
    604598[ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
    605599  #x #y #Hx normalize nodelta >Hx / by refl/
    606 | #ppc #ppc_ok @conj
     600| cases daemon (* leaving this until stabilisation of sigma predicate *)
     601  (*#ppc #ppc_ok normalize nodelta @conj
    607602  [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok)
    608603    >bitvector_of_nat_inverse_nat_of_bitvector
     
    651646        ]
    652647      ]
    653     ]
     648    ] 
    654649  | cases daemon (* XXX remains to be done *)
    655   ]
     650  ] *)
    656651]
    657652qed.           
Note: See TracChangeset for help on using the changeset viewer.