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!
------------------------------------------------------------------------------
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
