Changeset 2142


Ignore:
Timestamp:
Jun 29, 2012, 10:09:10 AM (5 years ago)
Author:
sacerdot
Message:

Down to one daemon that requires one lemma (monotonicity of sigma).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2138 r2142  
    406406    [1: #j #H <load_code_memory_ok
    407407        [ @assembly_ok
    408         | cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))) ≤ |assembled'|)
    409           [ cases sigma_policy_witness #_ #sigma_ok cases daemon
    410             (*CSC: True, propagate already proved invariant*)
    411           | #LE @(lt_to_le_to_lt … LE)
    412             @lt_to_lt_nat_of_bitvector_add
    413             [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
    414               / by /
    415             | @(transitive_le ???? assembly_ok1) change with (? < ?) cases daemon
    416               (*CSC: Same as before*)
    417             | assumption
    418             ]   
     408        | cases (le_to_or_lt_eq … assembly_ok1)
     409          [ #assembly_ok1'
     410            cut (nat_of_bitvector 16 (sigma ppc)+|assembled|≤|assembled'|)
     411            [ <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok
     412              cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
     413              #sigma_ok1 #sigma_ok2
     414              cases daemon (*CSC: True, apply lemma above + monotonicity of sigma *)
     415            | #LE2
     416              cut (|assembled| < 2^16)
     417               [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction) / by /] #LTassembled
     418              cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))) ≤ |assembled'|)
     419              [ >nat_of_bitvector_add
     420                >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     421                @(le_to_lt_to_lt … LE2 assembly_ok1')
     422              | #LE @(lt_to_le_to_lt … LE)
     423                @lt_to_lt_nat_of_bitvector_add
     424                [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
     425                  / by /
     426                | @(le_to_lt_to_lt ???? assembly_ok1') @LE2
     427                | assumption
     428                ]
     429              ]
     430            ]
     431          | #assembly_ok1' >assembly_ok1' / by /
    419432          ]
    420433        ]
Note: See TracChangeset for help on using the changeset viewer.