Dhanurbhanga: The Fractured Invariant

By Team Cryptonite · 2 min read

About the CTF: Pinaka CTF

Produce a well-formed Pinaka Tension Machine (PTM) program whose final register equals TARGET = 3205865151537252764. A formal proof says that's impossible over unbounded integers, but the real checker does its…

**Pinaka CTF 2026** · Reverse engineering · Team Cryptonite · All 44 Pinaka write-ups

Category: reverse engineering / logic

Flag: PINAKA{dhanurbhangaasingleuint64wrapshattersshivasunbreakablebow}

Overview

Produce a well-formed Pinaka Tension Machine (PTM) program whose final register equals TARGET = 3205865151537252764. A formal proof says that's impossible over unbounded integers, but the real checker does its arithmetic in uint64.

Files:

• pinaka_check.c: the real checker
• formal_model.py: Python-bignum model that implements the proof

Analysis

The machine:

• State: one non-negative integer register x, starting at X0 = 0.
• Opcodes: HALT, TRPL (x3), SQ (xx), ADDK imm (x+imm), MULK imm (x*imm). Immediates are little-endian unsigned 64-bit.
• Well-formed means: valid opcodes, complete 8-byte immediates, every imm % 3 == 0, at most 4096 bytes, at most 1024 steps.
• Accept if and only if the program is well-formed and the halting register equals TARGET.

Why the proof says no. With X0 = 0 and every immediate divisible by 3, "x == 0 (mod 3)" survives every opcode:

• TRPL: 3x -> preserves it (x3)
• SQ: x*x -> preserves it
• ADDK: x+imm with imm == 0 -> preserves it
• MULK: x*imm -> preserves it

Every reachable x is divisible by 3, but TARGET == 2 (mod 3), so it's unreachable over Z. formal_model.py implements exactly this and rejects every attempt.

The crack. The proof assumed exact integers, but the checker works mod 2^64, and:

2^64  ==  1 (mod 3)     (not 0)

Every wraparound subtracts a multiple of 2^64, and because that isn't divisible by 3, it shifts the residue of x mod 3. One overflow is enough to escape the invariant.

Solution

We need a true-integer sum S divisible by 3 (so every immediate is legal) and congruent to TARGET mod 2^64:

S = TARGET + k*2^64 ,   need S  ==  0 (mod 3)
   =>  (TARGET + k)  ==  0 (mod 3)   =>   k  ==  -TARGET  ==  1 (mod 3)

With k = 1:

S = TARGET + 2^64 = 21652609225246804380      (S % 3 == 0, S mod 2^64 == TARGET)

Split S into two ADDK immediates, each below 2^64 and divisible by 3 (2^64 - 1 == 0 mod 3):

10 ffffffffffffffff   ADDK 18446744073709551615   (= 2^64-1,  ==  0 mod 3)
10 9d892eb35e857d2c   ADDK  3205865151537252765    ( ==  0 mod 3)
00                    HALT

Program hex (19 bytes): 10ffffffffffffffff109d892eb35e857d2c00

Under uint64: 0 + (2^64-1) = 2^64-1, then adding 3205865151537252765 overflows once and wraps to exactly TARGET.

Local verification:

• formal_model.py: final = 21652609225246804380, REJECT (well-formed but unreachable over Z, as proven)
• compiled pinaka_check.c: ACCEPT x=3205865151537252764 == TARGET

Submission

POST /mithila/dhanurbhanga   {"program":"10ffffffffffffffff109d892eb35e857d2c00"}
 ->  {"status":"bow-broken",
   "checker":"ACCEPT x=3205865151537252764 == TARGET",
   "flag":"PINAKA{dhanurbhanga_a_single_uint64_wrap_shatters_shivas_unbreakable_bow}"}

Notes

• A formal proof is only as sound as its model of the machine. The proof reasoned over Z; the implementation ran over Z/2^64Z.
• Because 2^64 isn't divisible by 3, a single overflow breaks the "x is always a multiple of 3" invariant.

Read this post on CyberHx →