CiaoPP: `trust' qualifier and predicate definition

[simonefulvio-rollini]

Let us consider the following example, which focuses on type checking in presence of built-in and user-defined predicates with 'trust' qualifiers:

:- module(test6, [p1/2], [assertions,nativeprops]).

:- use_module(library(numlists)).

:- entry p1(X,Y) : list(int,X).
:- check success p1(X,Y) => int(Y).

p1(X,Y) :-
    sum_list(X,Z),
    p2(Z,Y).

:- trust pred sum_list(X,Z) : list(int,X) => int(Z).
    
:- trust pred p2(Z,Y) : int(Z) => int(Y).
p2(Z,Y) :- Y is (Z + 1).

I see that the addition of `pred' assertions for built-in predicates is supported: this is very useful, when willing to check properties of user-defined predicates calling built-in predicates as in the example.

Something that I do not understand is the necessity of defining predicates for which 'trust' qualifiers are introduced.
For example, in 2005 paper 'Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation', it is stated that "Assertions can also be used to provide information to the analyzer in order to increase its precision or to describe predicates which have not been coded yet during program development. These assertions have a trust prefix".
I would like to employ 'trust' qualifiers exactly for this purpose, leaving p2 undefined in the example.
Currently, the best I can do is replacing its definition with a 'stub' like 'p2( _ , _ )' which does not seem a satisfactory solution to me; in absence of a definition for p2, the tool raises a 'Predicate p2/2 undefined in source' error.

Can you please clarify how to use 'trust' qualifiers about a predicate without defining that predicate?

Also, when verifying this example, CiaoPP reports that an assertion (one of those automatically placed by the tool) could not be verified:

{In /home/simonefulvio.rollini-a/Documents/logicprogramming/Examples/test6.pl
WARNING (ctchecks_pp_messages): (lns 15-15) At literal 1 could not verify assertion:
:- check calls A is B
   : ( var(A), nonvar(B), var(A), arithexpression(B)
     ; var(A), nonvar(B), var(A), intexpression(B)
     ; nonvar(A), nonvar(B), num(A), arithexpression(B)
     ; nonvar(A), nonvar(B), int(A), intexpression(B) ).
because on call A is B :
[eterms] term(A),rt1(B) 
with:
:- regtype rt1/1.
rt1(A+1) :-
    int(A).


[shfr]   mshare([[A]]),ground([B]) 
}

What is happening here? Why does the call not correspond to any of the accepted modes?

Thank you for your help,
Simone

[mherme]

Something that I do not understand is the necessity of defining
predicates for which 'trust' qualifiers are introduced.

This is indeed not really necessary. You can add:

:- trust pred sum_list(X,Z) : list(int,X) => int(Z).
:- impl_defined(sum_list/2).

to avoid warnings from the compiler.

Also, when verifying this example, CiaoPP reports that an assertion
(one of those automatically placed by the tool) could not be verified:

{In /home/simonefulvio.rollini-a/Documents/logicprogramming/Examples/test6.pl
WARNING (ctchecks_pp_messages): (lns 15-15) At literal 1 could not verify assertion:
:- check calls A is B
   : ( var(A), nonvar(B), var(A), arithexpression(B)
     ; var(A), nonvar(B), var(A), intexpression(B)
     ; nonvar(A), nonvar(B), num(A), arithexpression(B)
     ; nonvar(A), nonvar(B), int(A), intexpression(B) ).
because on call A is B :
[eterms] term(A),rt1(B) 
with:
:- regtype rt1/1.
rt1(A+1) :-
    int(A).

[shfr]   mshare([[A]]),ground([B]) 
}

What is happening here? Why does the call not correspond to any of the
accepted modes?

The message comes from CiaoPP checking the assertions for the is/2
predicate in the library (core/engine/arithmetic.pl) at the program point
when is/2 is called in p2/2:

:- trust pred is(-A, +B) : var * arithexpression
    => (num(A), arithexpression(B), size(A, int(B))) + (not_fails, eval).
:- trust pred is(-A, +B) : var * intexpression
    => (int(A), intexpression(B), size(A, int(B))) + (not_fails, eval).
...

What CiaoPP is saying is that for those calls to A is B it cannot prove that
either A is a variable (var(A)) or that, if B is nonvar, then it is either
an int or a num. Btw, you can see what is inferred at the program point just
before the call to A is B by turning on the "Include program point info"
(pp_info) flag in the options menu.

It is easy to ensure that the calls to is/2 are correct by just stating in the entry
that Y is a variable (or an int or num):

:- entry p1(X,Y) : (list(int,X),var(Y)). % or int or num

Then:

ciaopp ?- auto_analyze('/Users/herme/clip/Systems/tests/test6_b.pl').
{NOTE (frontend_driver): uncached library sources (enable with 'ciaopp --gen-lib-cache')}
{Loading current module from /Users/herme/clip/Systems/tests/test6_b.pl
{loaded in 67.057 msec.}
}
{Analyzing (eterms): [/Users/herme/clip/Systems/tests/test6_b.pl]
{init for the plai fixpoint in 0.046 msec.}
{preprocessed for the plai fixpoint in 0.076 msec.}
{fixpoint reached by plai using eterms with local-control off in 3.826 msec.}
{analyzed by plai in 4.005 msec.}
}
{Analyzing (shfr): [/Users/herme/clip/Systems/tests/test6_b.pl]
{init for the plai fixpoint in 0.015 msec.}
{preprocessed for the plai fixpoint in 0.055 msec.}
{fixpoint reached by plai using shfr with local-control off in 0.321 msec.}
{analyzed by plai in 0.432 msec.}
}
{Checking assertions 
{Checking assertions of
/Users/herme/clip/Systems/tests/test6_b.pl
{NOTE (ctchecks_pred_messages): (lns 8-9) Verified assertion:
:- check success p1(X,Y)
   => int(Y).
}
{NOTE (ctchecks_pred_messages): (lns 18-19) Verified assertion:
:- check calls p2(Z,Y)
   : int(Z).
}
{In /Users/herme/clip/Systems/tests/test6_b.pl
NOTE (ctchecks_pp_messages): (lns 10-13) At literal 1 successfully verified assertion:
:- check success sum_list(A,B)
   : numlist(A)
   => num(B).

}
{In /Users/herme/clip/Systems/tests/test6_b.pl
NOTE (ctchecks_pp_messages): (lns 20-20) At literal 1 successfully checked assertion:
:- check calls A is B
   : ( var(A), nonvar(B), var(A), arithexpression(B)
     ; var(A), nonvar(B), var(A), intexpression(B)
     ; nonvar(A), nonvar(B), num(A), arithexpression(B)
     ; nonvar(A), nonvar(B), int(A), intexpression(B) ).

}
}
{assertions checked in 1.992 msec.}
}
{NOTE (analysis_stats): Assertion checking summary:
[Predicate-level] Checked: 2 (100.00%) False: 0 (0.00%) Check: 0 (0.00%) Total: 2
[Call site-level] Checked: 2 (100.00%) False: 0 (0.00%) Check: 0 (0.00%) Total: 2
}
{written file /Users/herme/clip/Systems/tests/test6_b_eterms_shfr_co.pl}

yes
ciaopp ?- 

Also, you can replace the entry and the success assertions for p1/2 with a single
pred:

:- pred p1(X,Y) : (list(int,X),var(Y)) => int(Y).

By default entry declarations are automatically inserted from the preconditions of the
exported predicates (this can be changed).

Btw what environment are you using CiaoPP from (Emacs, VSC, playground, terminal, ...)?
(Just curious)

Cheers,
Manuel

[simonefulvio-rollini]

Thank you very much for your advice, Manuel, the use of impl_defined is indeed the solution I needed, and I had underestimated the difference that explicitly declaring an argument as var makes when inferring types.
As you can guess from this discussion and the other one ongoing, I am getting familiar with Prolog and CiaoPP for modular verification, possibly of problems involving linear constraints.

I am currently using Emacs, which I find having a very friendly interface, and sometimes terminal, in a Linux Ubuntu environment.