Source code formal
reasoning copilot

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

from imandra.u.agents import get_remote_graph, create_thread_sync
from imandra.u.agents.code_logician_formalizer import InputState as FInput
from imandra.u.agents.code_logician_reasoner import InputState as RInput, ReasonerAction

# Convert Python code to IML code
code_logician_formalizer = get_remote_graph(agent_name='code_logician_python')

# verify that the result of g(x) is always larger than 0
create_thread_sync(code_logician_formalizer)
src_code = """
def g(x: int):
    if x > 22:
        return 9
    else:
        return 100 + x
"""

res = code_logician_formalizer.invoke(FInput(src_lang='python', src_code=src_code))
print(res['end_result']['result'])
# 'success'

iml_code = res['formalizations'][-1]['iml_code']
print(iml_code)
# --------------------------
# let g (x : int) : int = 
#   if x > 22 then        
#     9                   
#   else                  
#     100 + x             
# --------------------------

# Verify some property about the code, or find a counter-example if the property does not hold.
code_logician_reasoner = get_remote_graph(agent_name='code_logician_reasoner')
create_thread_sync(code_logician_reasoner)
res = code_logician_reasoner.invoke(
    RInput(
        src_code=src_code,
        iml_code=iml_code,
        action=ReasonerAction(type="extract_verify_reqs"),
    )
)

create_thread_sync(code_logician_reasoner)
res = code_logician_reasoner.invoke(
    RInput(
        src_code=src_code,
        iml_code=iml_code,
        verify_req=res["verify_req"],
        action=ReasonerAction(type="run_verify"),
    )
)

print(res['verify_req'][0]['extra']['instance_res']['sat']['model']['src'])
# --------------------------    
# module M = struct
#
#   let x = (-100.0)
#
#  end
# --------------------------