I've run your code in Kananaskis 7 and applied e(RW_TAC std_ss [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,OUT_def,COUT_def,BIT_VAL_def,VALUE_def]);
directly on your step case. Then I got 22 subgoals, which are much less than your case ... Still it is too many ... the subgoals mainly come from the combinations of the assumptions. But I doubt the correctness of "NADDER_IMP_def". Please check it. If you really want to involve the uncertain state, like `Z`, `U`, `W`, then the type of the signals should be changed. Good Luck, Liya Quoting Yuntao Peng <[email protected]>: > I am practicing using HOL4. As a beginner, a lot of primary problems puzzle > me. > There is the code of n-bit adder I writed according the paper of "Hardware > verification using higher-order logic". I have proved the basis case, and > stopped at the step case. > > set_trace "Unicode" 0; > show_assums:=true; > open HolKernel boolLib Parse bossLib; > open listTheory; > load "listlib"; > open listlib; > open arithmeticTheory; > > (***********************************************************************) > (* > *) > (* n-bit adder > *) > (* > *) > (* Data structure: > *) > (* First input: bool list > *) > (* Second input: bool list > *) > (* Carry input: bool > *) > (* Sum output: bool list > *) > (* Carry output: bool > *) > (* > *) > (***********************************************************************) > > (***********************************************************************) > (* Get the n-th element of the bool list *) > (***********************************************************************) > > val NTH_BIT_def = Define `(NTH_BIT(n:num,[]) = F) /\ > (NTH_BIT(0,l:bool list) = HD l) /\ > (NTH_BIT(n:num,l:bool list) = NTH_BIT(n-1,TL l))`; > > (***********************************************************************) > (* Computing value of the n-th element of the list *) > (* ture then 1,or 0 > *) > (***********************************************************************) > > val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:bool list) = > if(NTH_BIT(n,l)) then 1 else 0`; > > (***********************************************************************) > (* Computing value of the bool element *) > (* ture then 1,or 0 > *) > (***********************************************************************) > > val BIT_VAL_def = Define `BIT_VAL(aBIT:bool) = if(aBIT) then 1 else 0`; > > (***********************************************************************) > (* Computing value of the whole list *) > (***********************************************************************) > > val VALUE_def = Define `(VALUE(0,l:bool list) = NTH_BIT_VAL(0,l)) /\ > (VALUE(SUC n:num,l:bool list)= (2 ** (SUC n)) * NTH_BIT_VAL(n,l) + > VALUE(n,l))`; > > (***********************************************************************) > (* Sum output of the n-th bit > *) > (***********************************************************************) > > val OUT_def = Define`OUT(n,inp1,inp2,cn,out) = (NTH_BIT(n,out) = > (~NTH_BIT(n,inp1) /\ ~NTH_BIT(n,inp2) /\ cn) \/ (~NTH_BIT(n,inp1) /\ > NTH_BIT(n,inp2) /\ ~cn) \/ (NTH_BIT(n,inp1) /\ ~(NTH_BIT(n,inp2)) /\ ~cn) > \/ (NTH_BIT(n,inp1) /\ NTH_BIT(n,inp2) /\ cn))`; > > (***********************************************************************) > (* Carry of the n-th bit > *) > (***********************************************************************) > > val COUT_def = Define`COUT(n,inp1,inp2,cn,cout) = (cout = (NTH_BIT(n,inp1) > /\ NTH_BIT(n,inp2)) \/ (NTH_BIT(n,inp1) /\ cn) \/ (NTH_BIT(n,inp2) /\ cn))`; > > (***********************************************************************) > (* The implementation of (n+1)-th full adder *) > (***********************************************************************) > > val FULL_ADDER_IMP_def = Define`FULL_ADDER_IMP(SUC n,inp1,inp2,cn,out,cout) > = (OUT(n,inp1,inp2,cn,out) /\ COUT(n,inp1,inp2,cn,cout))`; > > (***********************************************************************) > (* Implementation of n-bit adder > *) > (***********************************************************************) > > val NADDER_IMP_def = Define`(NADDER_IMP(0,inp1,inp2,cin,out,cout) = (cout = > cin)) /\ > (NADDER_IMP(SUC n,inp1,inp2,cin,out,cout) = (?cn:bool. > NADDER_IMP(n,inp1,inp2,cin,out,cn) /\ FULL_ADDER_IMP(SUC > n,inp1,inp2,cn,out,cout)))`; > > (***********************************************************************) > (* Specification of n-bit adder > *) > (***********************************************************************) > > val NADDER_SPEC_def = Define`NADDER_SPEC(SUC n,inp1,inp2,cin,out,cout) = > ((2**(SUC n))*BIT_VAL(cout) + VALUE(n,out) = > VALUE(n,inp1)+VALUE(n,inp2)+BIT_VAL(cin))`; > > (***********************************************************************) > (* Main goal > *) > (***********************************************************************) > > g`!n:num inp1:bool list inp2:bool list cin:bool out:bool list > cout:bool.((LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ > (LENGTH inp1 > n) /\ NADDER_IMP(SUC n,inp1,inp2,cin,out,cout)) ==> > NADDER_SPEC(SUC n,inp1,inp2,cin,out,cout)`; > > (***********************************************************************) > (* Basis case > *) > (***********************************************************************) > > e(Induct); > e(REPEAT GEN_TAC THEN REWRITE_TAC > [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,BIT_VAL_def,OUT_def,COUT_def,VALUE_def]); > e(SIMP_TAC bool_ss []); > e(Cases_on `cin`); > e(Cases_on `inp1`); > e(Cases_on `inp2`); > e(RW_TAC list_ss []); > e(RW_TAC list_ss []); > e(Cases_on `inp2`); > e(RW_TAC list_ss []); > e(Cases_on `h`); > e(Cases_on `h'`); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > e(Cases_on `h'`); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > e(Cases_on `inp1`); > e(Cases_on `inp2`); > e(RW_TAC list_ss []); > e(RW_TAC list_ss []); > e(Cases_on `inp2`); > e(RW_TAC list_ss []); > e(Cases_on `h`); > e(Cases_on `h'`); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > e(Cases_on `h'`); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > e(RW_TAC list_ss [NTH_BIT_def,NTH_BIT_VAL_def]); > > (***********************************************************************) > (* Step case > *) > (***********************************************************************) > > e(REPEAT GEN_TAC); > e(REWRITE_TAC > [NADDER_IMP_def,NADDER_SPEC_def,FULL_ADDER_IMP_def,OUT_def,COUT_def,BIT_VAL_def,VALUE_def]); > > > We will simple the goal as follows. > Question 1:How to eliminate the existential quantifier "cn"? > Question 2:How to use the following assumption in the hypothesis list? > > !inp1 inp2 cin out cout. > (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ > LENGTH inp1 > n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==> > NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) > I do not know how to apply the tactic to the assumption. > > >> val it = > > (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ > LENGTH inp1 > SUC n /\ > (?cn. > (?cn'. > NADDER_IMP (n,inp1,inp2,cin,out,cn') /\ > (NTH_BIT (n,out) <=> > ~NTH_BIT (n,inp1) /\ ~NTH_BIT (n,inp2) /\ cn' \/ > ~NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) /\ ~cn' \/ > NTH_BIT (n,inp1) /\ ~NTH_BIT (n,inp2) /\ ~cn' \/ > NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) /\ cn') /\ > (cn <=> > NTH_BIT (n,inp1) /\ NTH_BIT (n,inp2) \/ > NTH_BIT (n,inp1) /\ cn' \/ NTH_BIT (n,inp2) /\ cn')) /\ > (NTH_BIT (SUC n,out) <=> > ~NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) /\ cn \/ > ~NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) /\ ~cn \/ > NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) /\ ~cn \/ > NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) /\ cn) /\ > (cout <=> > NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) \/ > NTH_BIT (SUC n,inp1) /\ cn \/ NTH_BIT (SUC n,inp2) /\ cn)) ==> > (2 ** SUC (SUC n) * (if cout then 1 else 0) + > (2 ** SUC n * NTH_BIT_VAL (n,out) + VALUE (n,out)) = > 2 ** SUC n * NTH_BIT_VAL (n,inp1) + VALUE (n,inp1) + > (2 ** SUC n * NTH_BIT_VAL (n,inp2) + VALUE (n,inp2)) + > if cin then 1 else 0) > ------------------------------------ > !inp1 inp2 cin out cout. > (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ > LENGTH inp1 > n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==> > NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) > : proof > > So, I try to apply RW_TAC to the goal,then get 64 subgoals. > > e(RW_TAC list_ss > [BIT_VAL_def,OUT_def,COUT_def,VALUE_def,NTH_BIT_def,NTH_BIT_VAL_def,NADDER_SPEC_def,NADDER_IMP_def,FULL_ADDER_IMP_def]); > > The subgoal at the top goal stack as follows. > > VALUE (n,out) + (2 ** SUC n + 2 ** SUC (SUC n)) = > VALUE (n,inp1) + (VALUE (n,inp2) + (2 * 2 ** SUC n + 1)) > ------------------------------------ > 0. !inp1 inp2 cin out cout. > (LENGTH inp1 = LENGTH inp2) /\ (LENGTH inp2 = LENGTH out) /\ > LENGTH inp1 > n /\ NADDER_IMP (SUC n,inp1,inp2,cin,out,cout) ==> > NADDER_SPEC (SUC n,inp1,inp2,cin,out,cout) > 1. NTH_BIT (n,out) > 2. NTH_BIT (n,inp1) > 3. NTH_BIT (n,inp2) > 4. LENGTH inp1 = LENGTH inp2 > 5. LENGTH inp2 = LENGTH out > 6. LENGTH inp1 > SUC n > 7. NADDER_IMP (n,inp1,inp2,T,out,T) > 8. NTH_BIT (SUC n,out) <=> > ~NTH_BIT (SUC n,inp1) /\ ~NTH_BIT (SUC n,inp2) \/ > NTH_BIT (SUC n,inp1) /\ NTH_BIT (SUC n,inp2) > 9. NTH_BIT (SUC n,inp1) > 10. NTH_BIT (SUC n,inp2) > : proof > > I can not move forward. > > thx! > -- Regards, Liya ------------------------------------------------------------------------------ AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
