I am trying to use Spoq framework (and on GitHub) to translate code from C to Coq. I faced problem - I am getting only low-level specifications for my functions (just AST), but I want to get high-level specifications (functions with parameters, fixpoints...).
I successfully compiled my C code to LLVM IR, and managed to create Coq project with
python3 AutoV/main.py build TestFactorialProof/proof.v
Obviously my configuration file proof.v is not good enough. I should manually write definitions for each fixpoint, like this
Definition rank (i: nat) := MAX_PAGE - i.(*user input*)
but where exactly should I write them? in the configuration (proof.v) file?
Couldn't find any documentation for Spoq with simple demonstrative examples.
This is my simple C code which I desire to translate to Coq
int factorial (int a);
void epow(int *, int);
int hello();
int main()
{
factorial(5);
int x = 34, y = 6;
epow(&x, 3);
epow(&y, 1);
hello();
hello();
hello();
return 0;
}
int factorial (int a) {
int i, fact=1;
for (i = 1; i <= a; i++) {
fact=fact*i;
}
return fact;
hello();
}
void epow(int *base, int pow) {
while (pow > 0) {
*base = *base * 10;
pow--;
}
}
int hello () {
static int count = 1;
return count++;
}
and this is my configuration file proof.v
Definition PROJ_NAME: string := "TestFactorial".
Definition PROJ_BASE: string := "./ProofGen".
(* Include "datatypes.v". *)
(* Include "constant.v". *)
(* Include "load_store.v". *)
Section Bottom.
Definition LAYER_DATA := RData.
Definition LAYER_CODE: string := "./factorial.json".
(* Definition LAYER_LOAD: string := "load_RData". *)
(* Definition LAYER_STORE: string := "store_RData". *)
(* Definition LAYER_GET_REG: string := "get_reg_RData". *)
(* Definition LAYER_SET_REG: string := "set_reg_RData". *)
Definition LAYER_PRIMS: list string :=
"epow" :: "hello" :: "factorial" :: nil.
End Bottom.
Section InlineAsms.
Definition LAYER_DATA := RData.
Definition LAYER_CODE: string := "./factorial.json".
(* Definition LAYER_LOAD: string := "load_RData". *)
(* Definition LAYER_STORE: string := "store_RData". *)
(* Definition LAYER_GET_REG: string := "get_reg_RData". *)
(* Definition LAYER_SET_REG: string := "set_reg_RData". *)
Definition LAYER_PRIMS: list string :=
nil.
End InlineAsms.
in file Code.v I am having AST
Require Import String.
Require Import ZArith.
Require Import List.
Require Import LayerSem.Libs.SMap.
Require Import LayerSem.IR.
Require Import LayerSem.IRSem.
Require Import LayerSem.Asm.AsmInsn.
Local Open Scope Z_scope.
Local Open Scope string_scope.
(************ Structures ************)
Definition structures : list (string * typ) :=
nil.
(************ Global Variables ************)
Definition v_hello_count :=
{| vname := "hello.count";
vtype := (TInt TI32);
vconst := false;
vinitializer := (Some (VInt (1)));
valign := 4 |}.
Definition globvars : list (string * global_var) :=
(("hello.count", v_hello_count)
:: nil).
(************ Functions ************)
Definition f_factorial :=
{| fname := "factorial";
rettype := (TInt TI32);
fargs :=
(("v_0", (TInt TI32))
:: nil);
falloca_vars := ("v_4" :: "v_2" :: "v_3" :: nil);
fbody :=
(Some
((IAlloca (TPtr (TInt TI32)) "v_2" 4)
:: (IAlloca (TPtr (TInt TI32)) "v_3" 4)
:: (IAlloca (TPtr (TInt TI32)) "v_4" 4)
:: (IStore (TInt TI32) (VLocal "v_2") (VLocal "v_0") 4)
:: (IStore (TInt TI32) (VLocal "v_4") (VInt (1)) 4)
:: (IStore (TInt TI32) (VLocal "v_3") (VInt (1)) 4)
:: (ILoop
((ILoad (TInt TI32) "v_6" (VLocal "v_3") 4)
:: (ILoad (TInt TI32) "v_7" (VLocal "v_2") 4)
:: (IBinOp TBool "v_8" Csle (VLocal "v_6") (VLocal "v_7"))
:: (IIf (VLocal "v_8")
((ILoad (TInt TI32) "v_10" (VLocal "v_4") 4)
:: (ILoad (TInt TI32) "v_11" (VLocal "v_3") 4)
:: (IBinOp (TInt TI32) "v_12" OMul (VLocal "v_10") (VLocal "v_11"))
:: (IStore (TInt TI32) (VLocal "v_4") (VLocal "v_12") 4)
:: (ILoad (TInt TI32) "v_14" (VLocal "v_3") 4)
:: (IBinOp (TInt TI32) "v_15" OAdd (VLocal "v_14") (VInt (1)))
:: (IStore (TInt TI32) (VLocal "v_3") (VLocal "v_15") 4)
:: nil)
((ILoad (TInt TI32) "v_17" (VLocal "v_4") 4)
:: (IReturn (TInt TI32) (Some (VLocal "v_17")))
:: nil))
:: IContinue
:: nil))
:: nil)) |}.
Definition f_main :=
{| fname := "main";
rettype := (TInt TI32);
fargs :=
nil;
falloca_vars := ("v_1" :: "v_2" :: "v_3" :: nil);
fbody :=
(Some
((IAlloca (TPtr (TInt TI32)) "v_1" 4)
:: (IAlloca (TPtr (TInt TI32)) "v_2" 4)
:: (IAlloca (TPtr (TInt TI32)) "v_3" 4)
:: (IStore (TInt TI32) (VLocal "v_1") (VInt (0)) 4)
:: (ICall (TInt TI32) (Some "v_4") (VGlobal "factorial") [(VInt (5))])
:: (IStore (TInt TI32) (VLocal "v_2") (VInt (34)) 4)
:: (IStore (TInt TI32) (VLocal "v_3") (VInt (6)) 4)
:: (ICall TVoid None (VGlobal "epow") [(VLocal "v_2"); (VInt (3))])
:: (ICall TVoid None (VGlobal "epow") [(VLocal "v_3"); (VInt (1))])
:: (ICall (TInt TI32) (Some "v_5") (VGlobal "hello") [ ])
:: (ICall (TInt TI32) (Some "v_6") (VGlobal "hello") [ ])
:: (ICall (TInt TI32) (Some "v_7") (VGlobal "hello") [ ])
:: (IReturn (TInt TI32) (Some (VInt (0))))
:: nil)) |}.
Definition f_hello :=
{| fname := "hello";
rettype := (TInt TI32);
fargs :=
nil;
falloca_vars := nil;
fbody :=
(Some
((ILoad (TInt TI32) "v_1" (VGlobal "hello.count") 4)
:: (IBinOp (TInt TI32) "v_2" OAdd (VLocal "v_1") (VInt (1)))
:: (IStore (TInt TI32) (VGlobal "hello.count") (VLocal "v_2") 4)
:: (IReturn (TInt TI32) (Some (VLocal "v_1")))
:: nil)) |}.
Definition f_epow :=
{| fname := "epow";
rettype := TVoid;
fargs :=
(("v_0", (TPtr (TInt TI32)))
:: ("v_1", (TInt TI32))
:: nil);
falloca_vars := ("v_4" :: "v_3" :: nil);
fbody :=
(Some
((IAlloca (TPtr (TPtr (TInt TI32))) "v_3" 8)
:: (IAlloca (TPtr (TInt TI32)) "v_4" 4)
:: (IStore (TPtr (TInt TI32)) (VLocal "v_3") (VLocal "v_0") 8)
:: (IStore (TInt TI32) (VLocal "v_4") (VLocal "v_1") 4)
:: (ILoop
((ILoad (TInt TI32) "v_6" (VLocal "v_4") 4)
:: (IBinOp TBool "v_7" Csgt (VLocal "v_6") (VInt (0)))
:: (IIf (VLocal "v_7")
((ILoad (TPtr (TInt TI32)) "v_9" (VLocal "v_3") 8)
:: (ILoad (TInt TI32) "v_10" (VLocal "v_9") 4)
:: (IBinOp (TInt TI32) "v_11" OMul (VLocal "v_10") (VInt (10)))
:: (ILoad (TPtr (TInt TI32)) "v_12" (VLocal "v_3") 8)
:: (IStore (TInt TI32) (VLocal "v_12") (VLocal "v_11") 4)
:: (ILoad (TInt TI32) "v_13" (VLocal "v_4") 4)
:: (IBinOp (TInt TI32) "v_14" OAdd (VLocal "v_13") (VInt (-1)))
:: (IStore (TInt TI32) (VLocal "v_4") (VLocal "v_14") 4)
:: nil)
((IReturn TVoid None)
:: nil))
:: IContinue
:: nil))
:: nil)) |}.
Definition funcs :=
(("factorial", f_factorial)
:: ("main", f_main)
:: ("hello", f_hello)
:: ("epow", f_epow)
:: nil).
(************ AsmProcs ************)
Definition asm_procs :=
nil.
(************ IR Module ************)
Definition code :=
{| structs := structures;
global_vars := globvars;
functions := funcs;
asm_procedures := asm_procs |}.
and /LAYER_NAME/Spec.v -- is not giving me any high-level specifications of the functions (auto-generated) just this
Require Import CommonDeps.
Require Import DataTypes.
Require Import GlobalDefs.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Section InlineAsms_Spec.
Context `{int_ptr: IntPtrCast}.
End InlineAsms_Spec.
Thank you!