23.07.25 (inclusive)

Monetary

MVP

ICT tasks

Media sphere

Technologies in telecommunications

Mobile app

Let's imagine the application as a directed graph G(V, E), the vertices are standalone modules (Flutter widgets, Unity scripts, Go services), the edges are RPC/FFI calls. A patch is a set of operations (ΔV, ΔE): adding/removing/replacing vertices or edges. The Verify(G, Δ) algorithm is required, satisfying: 1. Soundness - if Verify=SAFE, the system will never fall into a deadlock/loop, will not damage data and will not lose crypto‑invariants, regardless of future patches. 2. Termination - Verify is always completed in the end time. Reducing point 1 to the classic Halting Problem shows that it is undecidable in the general case: an algorithm that checks "whether an application will ever enter an infinite loop" is equivalent to a complete solver of the halting problem.

The customer has formulated the following acceptance criteria: • The Verify(G, Δ) algorithm returns {SAFE, UNSAFE} for the application structure in the form of graph G and patch Δ. • If the answer is SAFE, then the application remains correct for any subsequent patches. • The response time is less than 200 ms on a device of the "average smartphone 2022" class (6 GB RAM, Snapdragon 778G). • No remote back‑end: all calculations are performed on the client for privacy reasons.

Sergeev I. A.