Ignore:
Timestamp:
Jun 7, 2012, 1:44:18 AM (8 years ago)
Author:
sacerdot
Message:

Proof skeleton in place. Several daemons to be closed adding invariants.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1984 r2021  
    15741574   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
    15751575*)
     1576
     1577lemma load_code_memory_ok:
     1578 ∀program.
     1579 let program_size ≝ |program| in
     1580  program_size ≤ 2^16 →
     1581   ∀pc. ∀pc_ok: pc < program_size.
     1582    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
     1583 #program elim program
     1584 [ #_ #pc #abs normalize in abs; @⊥ /2/
     1585 | #hd #tl #IH #size_ok *
     1586   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
     1587     whd in match next; normalize nodelta
     1588   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
     1589     whd in match next; normalize nodelta
     1590   ]
     1591 cases daemon (*CSC: complete! *)
     1592qed.
     1593(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
     1594Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
     1595e' come fetchare l'i-esimo bit dalla memoria.
     1596Concludere assembly_ok come semplice corollario.
     1597*)
    15761598lemma assembly_ok:
    15771599  ∀program.
     
    15801602  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    15811603  ∀assembled.
    1582   ∀costs'.
     1604  ∀costs': BitVectorTrie costlabel 16.
    15831605  let 〈preamble, instr_list〉 ≝ program in
    15841606  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
     
    15861608  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
    15871609    〈assembled,costs'〉 = assembly program sigma policy →
    1588       costs = costs' ∧
     1610      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    15891611        let code_memory ≝ load_code_memory assembled in
    15901612        let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 
     
    15971619                  sigma newppc = add … pc (bitvector_of_nat … len).
    15981620  #program #sigma #policy #sigma_policy_witness #assembled #costs'
    1599   @pair_elim #preamble #instr_list #program_refl
    1600   @pair_elim #labels #costs #create_label_cost_refl
    1601   #assembly_refl % cases daemon (*
    1602   [1:
    1603     (* XXX: lemma on BitVectorTries *)
    1604     cases daemon
    1605   |2:
    1606     #ppc #sigma_policy_specification_witness
    1607     @pair_elim #pi #newppc #fetch_pseudo_refl
    1608     cases pi
    1609     [2,3: (* Cost and Comment cases *)
    1610       #comment_or_cost normalize in ⊢ (% → ?); #absurd cases absurd
    1611     |1: (* PreInstruction cases *)
    1612       #preinstruction #_
    1613       @pair_elim #len #assembled' #assembly_1_pseudo_refl
    1614       normalize nodelta %
    1615       [1:
    1616         cases assembled' normalize
    1617       |2:
    1618       ]
    1619     ]
    1620   ]
    1621   cases daemon (* XXX: !!! *) *)
     1621  cases (assembly program sigma policy) * #assembled' #costs''
     1622  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
     1623  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
     1624  #assembly_ok #Pair_eq destruct(Pair_eq) whd
     1625  #ppc @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
     1626  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     1627  lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] -assembly_ok
     1628  >eq_fetch_pseudo_instruction
     1629  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
     1630  >(? : assembly_1_pseudoinstruction ????? pi = 〈len,assembled〉)
     1631   [2: (*CSC: Provable, isn't it?*) cases daemon
     1632   | whd in ⊢ (% → ?); #assembly_ok
     1633  %
     1634  [2: (*CSC: Use Jaap's invariant here *) cases daemon
     1635  | lapply (load_code_memory_ok assembled' ?) [(*CSC: Jaap?*) cases daemon]
     1636    #load_code_memory_ok
     1637    -eq_assembly_1_pseudoinstruction -program -policy -costs'' -labels -preamble -instr_list -costs -pi -newppc
     1638    cut (len=|assembled|) [(*CSC: provable before cleaning*) cases daemon] #EQlen
     1639    (* Nice statement here *)
     1640    cut (∀j. ∀H: j < |assembled|.
     1641          nth_safe Byte j assembled H =
     1642          \snd (next (load_code_memory assembled')
     1643          (bitvector_of_nat 16
     1644           (nat_of_bitvector …
     1645            (add … (sigma ppc) (bitvector_of_nat … j))))))
     1646    [(*CSC: is it provable?*) cases daemon
     1647    | -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
     1648      elim assembled
     1649       [ #pc #_ whd <add_zero %
     1650       | #hd #tl #IH #pc #H %
     1651         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
     1652           >H -H whd in ⊢ (??%?); <add_zero //
     1653         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
     1654           [2: (*CSC: TRUE, ARITHMETIC*) cases daemon]
     1655           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
     1656           <(nth_safe_prepend … [hd] … LTj) #IH >IH
     1657           (*CSC: TRUE, ARITHMETICS*)
     1658           cases daemon
     1659         ]
     1660    ]
    16221661qed.
    16231662
     
    16301669  ∀ppc.
    16311670  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1632   let 〈assembled, costs'〉 ≝ assembly program sigma policy in
     1671  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
    16331672  let code_memory ≝ load_code_memory assembled in
    16341673  let data_labels ≝ construct_datalabels (\fst program) in
     
    16491688  normalize nodelta
    16501689  @pair_elim #labels' #costs' #create_label_map_refl' #H
    1651   cases (H (sym_eq … assembled_refl))
    1652   #_
     1690  lapply (H (sym_eq … assembled_refl)) -H
    16531691  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
    16541692  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
     
    18141852  λsigma.
    18151853  λpolicy.
    1816     let p ≝ assembly pap sigma policy in
     1854    let p ≝ pi1 … (assembly pap sigma policy) in
    18171855      load_code_memory (\fst p).
    18181856
     
    23292367  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
    23302368  #fetch_pseudo_refl
    2331   letin assembled ≝ (\fst (assembly program sigma policy))
    2332   letin costs ≝ (\snd (assembly program sigma policy))
     2369  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
     2370  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
    23332371  lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs)
    23342372  @pair_elim #preamble #instr_list #program_refl
    23352373  @pair_elim #labels #costs' #create_label_cost_map_refl
    2336   <eq_pair_fst_snd #H cases (H (refl …)) -H #costs_refl #H
     2374  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
    23372375  lapply (H ppc) -H
    23382376  @pair_elim #pi' #newppc #fetch_pseudo_refl'
Note: See TracChangeset for help on using the changeset viewer.