[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Could I don't deliver prf file ?



Hi Zengbo,

I downloaded your files, and was able to prove all but two lemmas (not TCCs) using `privet -cisf` for the 3 files that had .prf files checked in (assuming that these were the theories that were causing issues), even after deleting the .prf files first. The two unproven lemmas were in implementation_rewrites_1, namely Rewrite_ex_alu_wb_1 and Rewrite_ex_alu_wb_2. I do not know why those two lemmas fail to prove - in both cases, when I do ‘M-x show-proof’ for them, I see that they failed to run the final (case-analysis) in your ProofLite script. They did do the other steps, however.

Basically, instead of:
%|- Rewrite_ex_alu_wb_* : PROOF                                                                                                                                                                           
%|- (then (skosimp) (impl-defs) (assert)                                                                                                                                                                  
%|-  (auto-rewrite-theory decoder_props) (assert) (case-analysis))                                                                                                                                        
%|- QED 

They acted as if the script said:
%|- Rewrite_ex_alu_wb_* : PROOF                                                                                                                                                                           
%|- (then (skosimp) (impl-defs) (assert)                                                                                                                                                                  
%|-  (auto-rewrite-theory decoder_props) (assert))                                                                                                                                        
%|- QED 

In looking further, I see right underneath that you have:
%|- Rewrite_ex_* : PROOF
%|- Rewrite_id_* : PROOF
%|- (then (skosimp) (impl-defs) (assert)
%|-  (auto-rewrite-theory decoder_props) (assert))
%|- QED

Note that “Rewrite_ex*” also matches “Rewrite_ex_alu_wb_*”. If I switch the order of those two ProofLite scripts, the problem goes away.

Here are details from my Terminal window before the edit:
=========
~Tools/mips-pipeline-proof
▶ rm -rf pvsbin .pvscontext *.prf

~Tools/mips-pipeline-proof
▶ proveit -cisf instructions
Removing ./.pvscontext ./pvsbin/ ./instructions.summary ./instructions.log
Processing ./instructions.pvs. Writing output to file ./instructions.summary
Proving chain of imported theories
Forcing all proofs
 Proof summary for theory abstract_instructions
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.32 s)
 Proof summary for theory instructions
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.20 s)
 Proof summary for theory stores
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.22 s)
 Proof summary for theory bvconsts
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Grand Totals: 8 proofs, 8 attempted, 8 succeeded (0.74 s)

~Tools/mips-pipeline-proof
▶ proveit -cisf implementation_invariants
Removing ./.pvscontext ./pvsbin/ ./implementation_invariants.summary ./implementation_invariants.log
Processing ./implementation_invariants.pvs. Writing output to file ./implementation_invariants.summary
Proving chain of imported theories
Forcing all proofs
 Proof summary for theory implementation_invariants
    Theory totals: 17 formulas, 17 attempted, 17 succeeded (3.46 s)
 Proof summary for theory implementation_rewrites_1
    Rewrite_ex_alu_wb_1...................unfinished          [shostak](0.34 s)
    Rewrite_ex_alu_wb_2...................unfinished          [shostak](0.33 s)
    Theory totals: 63 formulas, 63 attempted, 61 succeeded (8.60 s)
 Proof summary for theory implementation_trans_1
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
 Proof summary for theory implementation_state_1_signal
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (15.54 s)
 Proof summary for theory implementation_state_1_sync
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
 Proof summary for theory implementation_state_1
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (3.65 s)
 Proof summary for theory specification_state
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
 Proof summary for theory instructions
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.21 s)
 Proof summary for theory stores
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.22 s)
 Proof summary for theory bvconsts
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
 Proof summary for theory specification_muxers
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
 Proof summary for theory datapath
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.14 s)
 Proof summary for theory datapath_ctrl_signals
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
 Proof summary for theory abstract_instructions
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.30 s)
 Proof summary for theory decoder_props
    Theory totals: 52 formulas, 52 attempted, 52 succeeded (88.24 s)
 Proof summary for theory instruction_decoder
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (6.66 s)
 Proof summary for theory abstraction_rewrites
    Theory totals: 60 formulas, 60 attempted, 60 succeeded (2.01 s)
 Proof summary for theory abstraction
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (21.40 s)
Grand Totals: 215 proofs, 215 attempted, 213 succeeded (150.43 s)

~Tools/mips-pipeline-proof
▶ proveit -cisf stores                       
Removing ./.pvscontext ./pvsbin/ ./stores.summary ./stores.log
Processing ./stores.pvs. Writing output to file ./stores.summary
Proving chain of imported theories
Forcing all proofs
 Proof summary for theory stores
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.26 s)
 Proof summary for theory bvconsts
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Grand Totals: 5 proofs, 5 attempted, 5 succeeded (0.26 s)
=========

After the edit, all 215 proofs are successful for implementation_invariants, namely the 2 in implementation_rewrites_1 that failed before now work.

Best Regards,
Ben Hocking


On May 16, 2015, at 3:24 AM, 张增波 <zengbo.zhang@xxxxxxxxx> wrote:

Hi all,

    I am thinking something about delivery of pvs context. I don't like prf file, because it is generated and will always change when re-run. In contrast, ProofLite script is clean. But I found that  tcc  and judgment script can't be installed by ProofLite when there is no prf file there, is it a bug for pvs or I just did something wrong ? I pushed my context to https://github.com/pluswave/mips-pipeline-proof , but there are two prf files because of this.  Could somebody help me ? Thanks in advance.

Best Regards,
Zengbo