Ignore:
Timestamp:
Jun 26, 2012, 4:05:15 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2108 r2110  
    15111511lemma assembly_ok:
    15121512  ∀program.
    1513   ∀length_proof: |\snd program| < 2^16.
     1513  ∀length_proof: |\snd program| 2^16.
    15141514  ∀sigma: Word → Word.
    15151515  ∀policy: Word → bool.
     
    15331533                  sigma newppc = add … pc (bitvector_of_nat … len).
    15341534  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
    1535   @pair_elim #preamble #instr_list #EQprogram
    15361535  cases (assembly program sigma policy) * #assembled' #costs''
    1537   >EQprogram normalize nodelta
    1538   @pair_elim #labels #costs #EQcreate_label_cost_refl normalize nodelta
    1539   #assembly_ok #Pair_eq destruct(Pair_eq) whd
    1540   #ppc #ppc_ok
    1541   @pair_elim #pi #newppc #EQfetch_pseudo_instruction
    1542   >EQprogram in sigma_policy_witness; #sigma_policy_witness
    1543   lapply (assembly_ok sigma_policy_witness ? ppc ?)
    1544   [2: >EQprogram in length_proof; #length_proof; assumption ] try assumption
    1545   >EQfetch_pseudo_instruction normalize nodelta
     1536  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
     1537  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
     1538  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
     1539  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
     1540  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
     1541  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
     1542  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     1543  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
     1544  >eq_fetch_pseudo_instruction
    15461545  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
    1547   @pair_elim #len #assembledi #EQassembly_1_pseudo_instruction
    1548   letin lookup_labels ≝ (λx.sigma (bitvector_of_nat 16 (lookup_def ASMTag ℕ labels x O)))
    1549   letin lookup_datalabels ≝ (λx. lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16))
    1550   >(? : assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi = 〈len,assembledi〉)
    1551   [2: <EQassembly_1_pseudo_instruction % ]
    1552   whd in ⊢ (% → ?); #assembly_ok %
    1553   [2: (*CSC: Use Jaap's invariant here *) cases daemon
    1554   |1:
    1555     lapply (load_code_memory_ok assembledi ?)
    1556     [1:
    1557       lapply sigma_policy_witness whd in match sigma_policy_specification;
    1558       normalize nodelta * #_ #relevant
    1559       (* XXX: wait for Jaap to propagate the property that program
    1560               is less than 2^16.
    1561        *)
     1546  > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
     1547       (λx.address_of_word_labels_code_mem instr_list x)))
     1548  [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
     1549      #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
     1550  >eq_assembly_1_pseudoinstruction
     1551  whd in ⊢ (% → ?); #assembly_ok
     1552  %
     1553  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
     1554      >snd_fetch_pseudo_instruction
     1555      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
     1556      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
     1557      >eq_fetch_pseudo_instruction whd in match instruction_size;
     1558      normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
    15621559      cases daemon
    1563     ]
     1560  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
    15641561    #load_code_memory_ok
    1565     cut (len=|assembledi|)
     1562    cut (len=|assembled|)
    15661563    [1: (*CSC: provable before cleaning *)
    15671564        cases daemon
     
    15691566    #EQlen
    15701567    (* Nice statement here *)
    1571     cut (∀j. ∀H: j < |assembledi|.
    1572           nth_safe Byte j assembledi H =
     1568    cut (∀j. ∀H: j < |assembled|.
     1569          nth_safe Byte j assembled H =
    15731570          \snd (next (load_code_memory assembled')
    15741571          (bitvector_of_nat 16
     
    15791576    |2:
    15801577      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
    1581       elim assembledi
     1578      elim assembled
    15821579      [1:
    1583         #pc #_ whd (* <add_zero %
    1584        | #hd #tl #IH #pc #H %
     1580        #pc #_ whd <add_zero %
     1581      | #hd #tl #IH #pc #H %
    15851582         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
    15861583           >H -H whd in ⊢ (??%?); <add_zero //
    15871584         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
    1588            [2: (*CSC: TRUE, ARITHMETIC*) cases daemon]
     1585           [2: <add_bitvector_of_nat_Sm @add_associative ]
    15891586           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
    1590            <(nth_safe_prepend … [hd] … LTj) #IH >IH
    1591            (*CSC: TRUE, ARITHMETICS*)
    1592            cases daemon
    1593          ]
    1594     ] *) cases daemon
    1595   ]
    1596   cases daemon
     1587           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
     1588           >add_associative % ]]
     1589  ]]
    15971590qed.
    15981591
     
    16001593lemma fetch_assembly_pseudo2:
    16011594  ∀program.
    1602   ∀length_proof: |\snd program| < 2^16.
     1595  ∀length_proof: |\snd program| 2^16.
    16031596  ∀sigma.
    16041597  ∀policy.
     
    19731966        match pol lookup_labels ppc with
    19741967        [ short_jump ⇒ 〈2, 2〉
    1975         | medium_jump ⇒ ?
     1968        | absolute_jump ⇒ ?
    19761969        | long_jump ⇒ 〈4, 4〉
    19771970        ] *)
     
    19791972        match pol lookup_labels ppc with
    19801973        [ short_jump ⇒ 〈2, 2〉
    1981         | medium_jump ⇒ ?
     1974        | absolute_jump ⇒ ?
    19821975        | long_jump ⇒ 〈4, 4〉
    19831976        ] *)
     
    19851978        match pol lookup_labels ppc with
    19861979        [ short_jump ⇒ 〈2, 2〉
    1987         | medium_jump ⇒ ?
     1980        | absolute_jump ⇒ ?
    19881981        | long_jump ⇒ 〈4, 4〉
    19891982        ] *)
     
    19911984        match pol lookup_labels ppc with
    19921985        [ short_jump ⇒ 〈2, 2〉
    1993         | medium_jump ⇒ ?
     1986        | absolute_jump ⇒ ?
    19941987        | long_jump ⇒ 〈4, 4〉
    19951988        ] *)
     
    19971990        match pol lookup_labels ppc with
    19981991        [ short_jump ⇒ 〈2, 2〉
    1999         | medium_jump ⇒ ?
     1992        | absolute_jump ⇒ ?
    20001993        | long_jump ⇒ 〈4, 4〉
    20011994        ] *)
     
    20031996        match pol lookup_labels ppc with
    20041997        [ short_jump ⇒ 〈2, 2〉
    2005         | medium_jump ⇒ ?
     1998        | absolute_jump ⇒ ?
    20061999        | long_jump ⇒ 〈4, 4〉
    20072000        ] *)
     
    20092002        match pol lookup_labels  ppc with
    20102003        [ short_jump ⇒ 〈2, 2〉
    2011         | medium_jump ⇒ ?
     2004        | absolute_jump ⇒ ?
    20122005        | long_jump ⇒ 〈4, 4〉
    20132006        ] *)
     
    20152008        match pol lookup_labels ppc with
    20162009        [ short_jump ⇒ 〈2, 2〉
    2017         | medium_jump ⇒ ?
     2010        | absolute_jump ⇒ ?
    20182011        | long_jump ⇒ 〈4, 4〉
    20192012        ] *)
     
    20212014        match pol lookup_labels ppc with
    20222015        [ short_jump ⇒ 〈2, 2〉
    2023         | medium_jump ⇒ ?
     2016        | absolute_jump ⇒ ?
    20242017        | long_jump ⇒ 〈4, 4〉
    20252018        ] *)
     
    23202313lemma snd_assembly_1_pseudoinstruction_ok:
    23212314  ∀program: pseudo_assembly_program.
    2322   ∀program_length_proof: |\snd program| < 2^16.
     2315  ∀program_length_proof: |\snd program| 2^16.
    23232316  ∀sigma: Word → Word.
    23242317  ∀policy: Word → bool.
Note: See TracChangeset for help on using the changeset viewer.