Verified Programming
by José M. Rodríguez Caballero
by José M. Rodríguez Caballero
Update. February 3, 2021
Statement of the problem
Statement of the problem
□
P is an untrusted prover (either open-source or closed-source), i.e., a heuristic rule, a random function following a given probability distribution, a quantum algorithm, a closed-source function, a simple rule that inexplicably solves a given problem (NKS empiricism). The prover can be any function.
□
V is a trusted verifier of P (always open-source). The verifier is a Boolean-valued function (x, y) V[x, y] of two variables x and y, where x is of the same type as the input of P and y is of the same type as the output of P. We accept that y is a good candidate to be a good approximation of P[x] (including the possibility of equality) if and only if V[x, P[x]] is True.
□
We want to evaluate P at a given input x and use the result y = P[x] of this evaluation in further computations, provided that it is accepted by the verifier V, i.e., that V[x, y] is true.
Data structure
Data structure
The main data structure of verified programming is a pattern PV[P,V], called verified function, where P is the prover and V is the verifier.
In[]:=
PV[]:=Failure["PVFailure",<|"Message""PV can't accept zero arguments"|>]
In[]:=
PV[_]:=Failure["PVFailure",<|"Message""PV can't accept exactly one argument"|>]
In[]:=
PV[_,_,__]:=Failure["PVFailure",<|"Message""PV can't accept more than two arguments"|>]
Example
Example
We define the verified square root as
In[]:=
VSqrt := PV[Function[x,Nest[0.5(#+x/#)&,x,10]],Function[{x,y},Abs[x - y^2] < 0.001]]
where the prover is the function assigns to x the result of applying 10 interactions to the rule
t↦t+
1
2
x
t
and the verifier accepts the pair (x, y) if and only if
x-<0.001
2
y
Verified evaluation
Verified evaluation
The verified evaluation of a verified function PV[P, V] at an input x is defined as
In[]:=
VEval[Verbatim[PV][P_, V_], x_]:=If[V[x,#],#,$Aborted]&[P[x]]
where
P is the prover,
V is the verifier of P,
t is the time of the execution (in seconds), and
x is the input of P.
P is the prover,
V is the verifier of P,
t is the time of the execution (in seconds), and
x is the input of P.
Example
Example
The verified function VSqrt is capable of computing square root of 2
In[]:=
VEval[VSqrt,2.]
Out[]=
1.41421
but it is not capable of computing the square root of 200000000000000000
In[]:=
VEval[VSqrt,200000000000000000.]
Out[]=
$Aborted
Composition
Composition
Given two verified functions PV[P1,V1] and PV[P2,V2], we define their composition as the following verified function
In[]:=
VComp[Verbatim[PV][P1_,V1_],Verbatim[PV][P2_,V2_]]:=PV[P1[P2[#]]&,Function[{x,y},If[V2[x,#],V1[#,y],False]&[P2[x]]]]
Example
Example
We define the verified division by Zeta[2] as
In[]:=
VZeta2:=PV[Function[x,Length[Select[Range[Round[100000*x]],SquareFreeQ]]/100000],Function[{x,y},Abs[x-Zeta[2]*y]<0.001]]
where the prover is based of the number theoretic fact that the asymptotic density of square free numbers is the multiplicative inverse of Zeta[2].
We will evaluate the two possible compositions between VZeta2 and VSqrt and evaluate it at 0.25.
In[]:=
VEval[VComp[VZeta2,VSqrt],0.25]//N
Out[]=
0.30401
In[]:=
VEval[VComp[VSqrt,VZeta2],.25]//N
Out[]=
0.389833
Remark
Remark
Whenever all computations are accepted by the verifiers, the evaluation of the composition of deterministic verified functions is associative. For example, consider the verified logarithm
In[]:=
VLog:=PV[(#^(0.0000001)-1)*10000000&,Function[{x,y},0.99<x/Exp[y]<1.01]]
we can check that
In[]:=
VEval[VComp[VLog,VComp[VSqrt,VZeta2]],5]
Out[]=
0.55586
In[]:=
VEval[VComp[VComp[VLog,VSqrt],VZeta2],5]
Out[]=
0.55586
Notice that if some of the functions is random, associativity may be violated.
Multiway verified functions
Multiway verified functions
A multiway evaluation is an evaluation of the function
In[]:=
WEval[Verbatim[PV][{},V_],x_]:=$Aborted
In[]:=
WEval[Verbatim[PV][{P_},V_],x_]:=VEval[PV[P,V],x]
In[]:=
WEval[Verbatim[PV][P_List,V_],x_]:=If[#===$Aborted,WEval[PV[Rest[P],V],x],#]&[VEval[PV[First[P],V],x]]
where P is a list of provers and V is a common verifier.
Example 1
Example 1
First prover works
In[]:=
WEval[PV[{Function[x,1+x+x^2+x^3+x^4+x^5](*prover1*)},Function[{x,y},Abs[1/(1-x)-y]<0.01](*commonverifier*)],0.25(*input*)]
Out[]=
1.33301
Second prover fails
In[]:=
WEval[PV[{Function[x,-x^(-1)-x^(-2)-x^(-3)-x^(-4)-x^(-5)](*prover2*)},Function[{x,y},Abs[1/(1-x)-y]<0.01](*commonverifier*)],0.25(*input*)]
Out[]=
$Aborted
Multiway evaluation works
In[]:=
WEval[PV[{Function[x,1+x+x^2+x^3+x^4+x^5](*prover1*),Function[x,-x^(-1)-x^(-2)-x^(-3)-x^(-4)-x^(-5)](*prover2*)},Function[{x,y},Abs[1/(1-x)-y]<0.01](*commonverifier*)],0.25(*input*)]
Out[]=
1.33301
Example 2
Example 2
First prover fails
In[]:=
WEval[PV[{Function[x,1+x+x^2+x^3+x^4+x^5](*prover1*)},Function[{x,y},Abs[1/(1-x)-y]<0.01](*commonverifier*)],4(*input*)]
Out[]=
$Aborted
Second prover works
In[]:=
WEval[PV[{Function[x,-x^(-1)-x^(-2)-x^(-3)-x^(-4)-x^(-5)](*prover2*)},Function[{x,y},Abs[1/(1-x)-y]<0.01](*commonverifier*)],4(*input*)]
Out[]=
-
341
1024
Multiway evaluation works
In[]:=
WEval[PV[{Function[x,1+x+x^2+x^3+x^4+x^5](*prover1*),Function[x,-x^(-1)-x^(-2)-x^(-3)-x^(-4)-x^(-5)](*prover2*)},Function[{x,y},Abs[1/(1-x)-y]<0.01](*commonverifier*)],4(*input*)]
Interpretation in the Wolfram Model
Interpretation in the Wolfram Model
Any evaluation of a verified function F at an input x can be interpreted as a spacetime event, denoted (F, x). Given two events (F, x) and (G, y), we say that (F, x) causally influences (G, y) if the evaluation of G at y requires the previous evaluation of F at x according to a fixed implementation (we are considering the internal structure of the functions, not just the abstract correspondences).
The multiway evaluation can be interpreted as the merging of several branches of the multiway causal graph, where each branch corresponds to a prover.
Applications
Applications
Connections with NKS
Connections with NKS
Considering a conventional verifier and several provers consisting of empirically found functions (simple programs), it is possible to use these resources for doing conventional programming even if there is not mathematical proof that the simple programs do what they empirically seem to do.
Closed-source programming
Closed-source programming
Some people do not trust closed source programming. Using verified programming, where the prover is closed-source and the verifier is open-source, there is no reason to distrust the outputs of closed-source programs.
Quantum and probabilistic computing
Quantum and probabilistic computing
Sometimes in quantum and probabilistic computing, there is a small probability of error. The verified programming approach may use a deterministic verified combined with a quantum or probabilistic prover in order to avoid the errors.
References
References
Wolfram, Stephen. A New Kind of Science. Vol. 5. Champaign, IL: Wolfram media, 2002.
S. Wolfram, “A Class of Models with the Potential to Represent Fundamental Physics,” Complex Systems, 29(2), 2020 pp. 107–536.
https://doi.org/10.25088/ComplexSystems.29.2.107
https://doi.org/10.25088/ComplexSystems.29.2.107