Ignore:
Timestamp:
Jun 28, 2012, 4:47:42 PM (8 years ago)
Author:
sacerdot
Message:

Invariant exported from proof of assembly_ok.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2136 r2138  
    377377  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
    378378  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
    379   * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
     379  * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
    380380  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
    381381  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     
    10511051*)
    10521052
    1053 (*CSC: ???*)
    1054 (* XXX: we need a precondition here stating that the PPC is within the
    1055         bounds of the instruction list in order for Jaap's specification to
    1056         apply.
    1057 *)
    10581053lemma snd_assembly_1_pseudoinstruction_ok:
    10591054  ∀program: pseudo_assembly_program.
Note: See TracChangeset for help on using the changeset viewer.