Changeset 2146


Ignore:
Timestamp:
Jul 3, 2012, 3:09:50 AM (5 years ago)
Author:
sacerdot
Message:
  1. specification fixed again
  2. the proof in AssemblyProof? is now almost closed again (up to two lemmas)
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2144 r2146  
    708708     ∧
    709709     (nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨
    710       nat_of_bitvector … ppc = |instr_list| ∧ next_pc = zero …).
     710      S (nat_of_bitvector … ppc) = |instr_list| ∧ next_pc = zero …).
    711711
    712712definition assembly:
     
    720720       let 〈assembled,costs〉 ≝ res in
    721721       |assembled| ≤ 2^16 ∧
    722        nat_of_bitvector … (sigma (bitvector_of_nat … (|instr_list|))) = |assembled| ∧
     722       (nat_of_bitvector … (sigma (bitvector_of_nat … (|instr_list|))) = |assembled| ∨
     723        sigma (bitvector_of_nat … (|instr_list|)) = zero … ∧ |assembled| = 2^16) ∧
    723724       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    724725       let datalabels ≝ construct_datalabels preamble in
     
    733734           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
    734735            assembled K
    735 
     736 ?. cases daemon(*
    736737  λp.
    737738  λsigma.
     
    750751        let 〈ppc,code〉 ≝ ppc_code in
    751752         ppc = bitvector_of_nat … (|pre|) ∧
    752          nat_of_bitvector … (sigma ppc) = |code| ∧
     753         (nat_of_bitvector … (sigma ppc) = |code| ∨
     754          sigma ppc = zero … ∧ |code| = 2^16) ∧
    753755         ∀ppc'.∀ppc_ok'.
    754756          (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16) →
     
    847849           | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
    848850             [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
    849 *)qed.
     851*)*)qed.
    850852
    851853definition assembly_unlabelled_program:
  • src/ASM/AssemblyProof.ma

    r2144 r2146  
    375375  sigma_policy_specification program sigma policy →
    376376   ∀ppc1,ppc2.
    377     nat_of_bitvector … ppc1 < |\snd program| → nat_of_bitvector … ppc2 < |\snd program| →
     377    nat_of_bitvector … ppc2 ≤ |\snd program| →
    378378    nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 →
    379      nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2).
     379     (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨
     380      sigma ppc2 = zero … ∧ nat_of_bitvector … ppc2 = |\snd program|).
    380381 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2
    381  #ppc1_ok #ppc2_ok #LE
     382 #ppc2_ok #LE
    382383 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1)
    383  <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2)
     384 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) in ⊢ (?%(?%?));
    384385 lapply (le_n … (nat_of_bitvector … ppc2))
    385386 elim LE in ⊢ (?%? → %);
    386  [ #_ %
    387  | #m #LE_ppc1_m #IH #BOUNDED @(transitive_le … (IH …)) -IH
    388    [@(transitive_le … BOUNDED) %2 %]
    389    cut (m < |\snd program|) [ @(transitive_le … ppc2_ok) %2 /by/ ] #m_ok
    390    cases (SIGMAOK2 (bitvector_of_nat … m) ?)
    391    [2: >nat_of_bitvector_bitvector_of_nat_inverse /by/
    392        @(lt_to_le_to_lt … program_bounded) assumption ]
     387 [ #_ % %
     388 | #m #LE_ppc1_m #IH #BOUNDED
     389   cases (IH ?)
     390   [3: @(transitive_le … BOUNDED) %2 %
     391   |2: * #_ #abs @⊥ <abs in ppc2_ok; #abs'
     392       @(absurd ?? (not_le_Sn_n m))
     393       @(transitive_le … BOUNDED abs') ]
     394   -IH #IH
     395   cut (m < |\snd program|) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1
     396   cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2
     397   cases (SIGMAOK2 (bitvector_of_nat … m) ?) -SIGMAOK2
     398   [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
    393399   #_ *
    394    [2: * #abs @⊥ @(absurd ?? (lt_to_not_eq … m_ok))
    395        >nat_of_bitvector_bitvector_of_nat_inverse in abs; [#H @H]
    396        @(lt_to_le_to_lt … m_ok program_bounded) ]
    397    #LT <add_bitvector_of_nat_Sm >add_commutative @(transitive_le … LT) %2 %
    398 qed.
    399 
    400 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
     400   [ #LTsigma_m %1 @(transitive_le … IH) -IH
     401     <add_bitvector_of_nat_Sm >add_commutative
     402     @(transitive_le … LTsigma_m) %2 %
     403   | * #EQ1 #EQ2 %2 %
     404     [ <add_bitvector_of_nat_Sm >add_commutative assumption
     405     | <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption
     406     ]]]
     407qed.
     408
     409(*CSC: move elsewhere *)
     410axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
     411
     412(* This is a non trivial consequence of fetch_assembly_pseudo +
     413   load_code_memory_ok because the finite amount of memory. In
     414   particular the case when the compiled program exhausts the
     415   code memory is very tricky. *)     
    401416lemma assembly_ok:
    402417  ∀program.
     
    457472    [1: #j #H <load_code_memory_ok
    458473        [ @assembly_ok
    459         | cases (le_to_or_lt_eq … assembly_ok1)
    460           [ #assembly_ok1'
     474        | cases assembly_ok3 -assembly_ok3
     475          [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ]
     476          #EQlen_assembled' <EQlen_assembled'
     477          cases sigma_policy_witness #sigma_zero >EQprogram #sigma_ok
     478          cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
     479          whd in match instruction_size; normalize nodelta
     480          >create_label_cost_refl
     481          >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
     482          [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
     483          [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled';
     484              <add_bitvector_of_nat_Sm >add_commutative
     485              >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2
     486              whd in ⊢ (??%? → ?); #EQlen_assembled'
     487              cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ]
     488          cases (le_to_or_lt_eq … instr_list_ok)
     489          [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
     490              whd in ⊢ (??%? → ?); #EQlen_assembled'
     491              cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ]             
     492          ]
     493          #instr_list_ok' #NO_OVERFLOW
     494          @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
     495          [ @lt_to_lt_nat_of_bitvector_add
     496            [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
     497              / by /
     498            | <EQlen cases daemon (*CSC: TRUE BECAUSE OF NO_OVERFLOW*)
     499            | assumption
     500            ]
     501          | <EQlen <OK
     502            cases (monotone_sigma ???? sigma_policy_witness
     503             (add … ppc (bitvector_of_nat … 1))
     504             (bitvector_of_nat … (|instr_list|)) ??) try assumption
     505            [ #H @H
     506            |3: >EQprogram >nat_of_bitvector_bitvector_of_nat_inverse
     507                try % assumption
     508            |4: >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     509                >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption
     510                @(transitive_le … instr_list_ok') @le_S_S assumption
     511            | * #EQ1 @⊥ >EQ1 in EQlen_assembled';
     512                whd in ⊢ (??%? → ?); #EQlen_assembled'
     513                cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *)
     514            ]
     515          ]
     516(* OLD CODE          [ #assembly_ok1'
    461517            cut (nat_of_bitvector 16 (sigma ppc)+|assembled|≤|assembled'|)
    462             [ <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok
     518            [ cases sigma_policy_witness #_ >EQprogram #sigma_ok
    463519              cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
    464               #sigma_ok1 #sigma_ok2
    465               cases daemon (*CSC: True, apply lemma above + monotonicity of sigma *)
     520              whd in match instruction_size; normalize nodelta
     521              >create_label_cost_refl
     522              >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
     523              [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
     524              [ #JAP1
     525                cut (nat_of_bitvector … (sigma ppc) + len < 2^16)
     526                [cases daemon (*CSC: provable, needs lemma*)] #LT1
     527                <(nat_of_bitvector_bitvector_of_nat_inverse 16 len)
     528                [2: @(le_to_lt_to_lt … LT1) / by / ]
     529                cases assembly_ok3
     530                [2: * #_ #abs @⊥ @(absurd … abs (lt_to_not_eq … assembly_ok1')) ]
     531                #EQ_sigma_instr_list <EQ_sigma_instr_list
     532                <nat_of_bitvector_add
     533                [2: >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     534                    @(transitive_le … LT1) @le_S_S / by / ]
     535                <OK XXX
     536               
     537                 XXX cases daemon (*CSC: ???*)
     538                | -assembly_ok3 #assembly_ok3
     539                  <assembly_ok3             
     540                (*CSC: we have to go by cases here!*)
     541                <nat_of_bitvector_add
     542                [2: cases daemon ] (*CSC: end of wrong part*)
     543 
     544              |
     545              ]
     546             
     547             
     548               #JAP1
     549              <(nat_of_bitvector_bitvector_of_nat_inverse 16 len)
     550              [2: cases daemon ]
     551              cases assembly_ok3
     552              [2: * #_ #EQ2 cases daemon (*CSC: ???*)
     553              | -assembly_ok3 #assembly_ok3
     554                <assembly_ok3             
     555              (*CSC: we have to go by cases here!*)
     556              <nat_of_bitvector_add
     557              [2: cases daemon ] (*CSC: end of wrong part*)
     558           
     559           
     560             cases assembly_ok3
     561              [2: * #_ #EQ2 cases daemon (*CSC: ???*)
     562              | -assembly_ok3 #assembly_ok3
     563                <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok
     564                cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
     565                whd in match instruction_size; normalize nodelta
     566                >create_label_cost_refl
     567                >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
     568                [>eq_assembly_1_pseudoinstruction |2: skip] #OK #_ <EQlen
     569                <(nat_of_bitvector_bitvector_of_nat_inverse 16 len)
     570                [2: cases daemon ]
     571                <nat_of_bitvector_add
     572                [2: cases daemon ]
     573                <OK @(monotone_sigma2 … sigma_policy_witness) >EQprogram
     574                cases daemon (*CSC: ???*)
     575              ]
    466576            | #LE2
    467577              cut (|assembled| < 2^16)
     
    481591            ]
    482592          | #assembly_ok1' >assembly_ok1' / by /
    483           ]
    484         ]
     593          ]*)
    485594    |2:
    486595      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
     
    795904*)
    796905
    797 (* DEAD CODE?
    798 lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
    799  ∀M:internal_pseudo_address_map.
    800  ∀ps,ps': PseudoStatus.
    801  ∀pol.
    802   ∀prf:code_memory … ps = code_memory … ps'.
    803    let pol' ≝ ? in
    804    match status_of_pseudo_status M ps pol with
    805     [ None ⇒ status_of_pseudo_status M ps' pol' = None …
    806     | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
    807     ].
    808  [2: <prf @pol]
    809  #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    810  generalize in match (refl … (assembly (code_memory … ps) pol))
    811  cases (assembly ??) in ⊢ (???% → %)
    812   [ #K whd whd in ⊢ (??%?) <H >K %
    813   | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
    814 qed.
    815 *)
    816 
    817906(* XXX: check values returned for conditional jumps below! *)
    818907definition ticks_of0:
Note: See TracChangeset for help on using the changeset viewer.