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

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')
create_thread_sync(code_logician_formalizer)
src_code = """
# verify that the result of g(x) is always larger than 0
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