補足：
・N >= 1 を仮定しても構いません。
・C言語でなくても構いません。
本題
下記のコードの正当性を示していきます。
fn plus1(x: i32) -> i32 { (x as f64).sqrt().atan().cos().powi(2).recip().round() as _ }
disclaimer: cos などの内部実装では + や - がハチャメチャに使われていると思いますが、それは見なかったことにします。
たとえば、x == 2147483646.0 のとき、
x.sqrt().atan().cos().powi(2).recip() == 2147483647.005644321441650390625
となります。
証明
Claim 1: 任意の実数 $x\ge 0$ に対し、 $$ \frac1{\cos(\arctan(\sqrt{x}) )^2} = x+1 $$ が成り立つ。
Proof
$x = 0$ のときは明らかに成り立つので、以下 $x\gt 0$ とする。
底辺の長さを $1$、対辺の長さを $\sqrt x$ とする直角三角形を考え、底辺と斜辺の成す角を $\theta$ とする。このとき、$\tan(\theta) = \sqrt x$ であるから、$\theta = \arctan(\sqrt x)$ が成り立つ。 また、$\tan(\theta)^2 + 1 = 1/{\cos(\theta)^2}$ であるから、総合して $$ x+1 = \frac1{\cos(\arctan(x) )^2} $$ を得る。$\qed$
無限精度では成り立つことがわかったので、あとは f64 向けの議論です。
Corollary 2: 任意の実数 $x\ge 0$ に対し、 $$ \sin(\arctan(\sqrt{x}) )^2 = \frac{x}{x+1} $$ が成り立つ。
Lemma 3: 任意の実数 $|x|\le \pi\cdot 2^{-53}$ について $$ \begin{aligned} |{\sin(x)}| &\lt \pi\cdot 2^{-53}, \\ |{\cos(x)}| & \gt 1-\tfrac12(\pi\cdot 2^{-53})^2 \end{aligned} $$ が成り立つ。
Lemma 4: 任意の実数 $x\gt 0$ について $$ \begin{aligned} \frac{\sqrt{x}}{\sqrt{x+1}} \lt 1 \end{aligned} $$ が成り立つ。
$\gdef\libmsqrt#1{\operatorname{\texttt{s\hspace{-.03em}q\hspace{-.03em}r\hspace{-.03em}t}}(#1)}$ $\gdef\libmatan#1{\operatorname{\texttt{a\hspace{-.03em}t\hspace{-.03em}a\hspace{-.03em}n}}(#1)}$ $\gdef\libmcos#1{\operatorname{\texttt{c\hspace{-.03em}o\hspace{-.03em}s}}(#1)}$
数学関数の誤差評価は下記の表が正しいことを前提とします。また、x86_64 を使います。
この前提で、下記が成り立ちます。
$0\le n\lt 2^{31}$ を固定すると、ある実数 $\delta_{\texttt{sqrt}} \le 2^{-53}$ が存在して $$ \libmsqrt{n} = \sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) $$ が成り立つ。ある実数 $\delta_{\texttt{atan}} \le 2\cdot 2^{-53}$ が存在して $$ \libmatan{\libmsqrt{n}} = \arctan(\libmsqrt{n})\cdot (1+\delta_{\texttt{atan}}) $$ が成り立つ。ある実数 $\delta_{\texttt{cos}} \le 2\cdot 2^{-53}$ が存在して $$ \libmcos{\libmatan{\libmsqrt{n}}} = \cos(\libmatan{\libmsqrt{n}})\cdot (1+\delta_{\texttt{cos}}) $$ が成り立つ。すなわち、 $$ \begin{aligned} &\phantom{{}={}} {\libmcos{\libmatan{\libmsqrt{n}}}} \\ &= \cos(\libmatan{\libmsqrt{n}})\cdot (1+\delta_{\texttt{cos}}) \\ &= \cos(\arctan(\libmsqrt{n})\cdot (1+\delta_{\texttt{atan}}) )\cdot (1+\delta_{\texttt{cos}}) \\ &= \cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot (1+\delta_{\texttt{atan}}) )\cdot (1+\delta_{\texttt{cos}}) \end{aligned} $$ が成り立つ。
Lemma 5: 任意の実数 $x\ge 0$, $|\delta_{\texttt{sqrt}}|\le 2^{-53}$, $|\delta_{\texttt{atan}}|\le 2\cdot 2^{-53}$ に対して $$ \begin{aligned} |{\arctan(\sqrt{x}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot \delta_{\texttt{atan}}}| &\lt \pi\cdot 2^{-53} % &\lt \frac{\pi}2 \cdot 2\cdot 2^{-53} \\ % &= \pi\cdot 2^{-53} \end{aligned} $$ が成り立つ。
Proof. 任意の実数 $y\ge 0$ に対して $\arctan(y)\lt \frac{\pi}2$ であることより従う。$\qed$
Claim 6: 任意の整数 $0\le n\lt 2^{31}$ に対して $$ \begin{aligned} \libmcos{\libmatan{\libmsqrt{n}}} &\gt \left(\frac{1-\tfrac12(\pi\cdot 2^{-53})^2}{\sqrt{n(1+2^{-53})^2+1}} - \pi\cdot 2^{-53}\right) \cdot (1-2^{-52}), \\ \libmcos{\libmatan{\libmsqrt{n}}} &\lt \left(\frac1{\sqrt{n(1-2^{-53})^2+1}} + \pi\cdot 2^{-53}\right) \cdot (1+2^{-52}) \end{aligned} $$ が成り立つ。
Proof
$$ \begin{aligned} &\phantom{{}={}} {\cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot (1+\delta_{\texttt{atan}}) )} \\ &= \cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) ) + \arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot \delta_{\texttt{atan}}) \\ &= \cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) ) ) \cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot \delta_{\texttt{atan}}) \\ & \qquad\quad{} - \sin(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) ) ) \sin(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot \delta_{\texttt{atan}}) \\ &= \frac1{\sqrt{n(1+\delta_{\texttt{sqrt}})^2+1}} \cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot \delta_{\texttt{atan}}) \\ & \qquad\quad{} - \frac{\sqrt{n(1+\delta_{\texttt{sqrt}})^2}}{\sqrt{n(1+\delta_{\texttt{sqrt}})^2+1}} \sin(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot \delta_{\texttt{atan}}) \\ &\gt \frac1{\sqrt{n(1+\delta_{\texttt{sqrt}})^2+1}} \cdot (1-\tfrac12(\pi\cdot 2^{-53})^2) - \frac{\sqrt{n(1+\delta_{\texttt{sqrt}})^2}}{\sqrt{n(1+\delta_{\texttt{sqrt}})^2+1}} \cdot \pi\cdot 2^{-53} \\ &\gt \frac{1-\tfrac12(\pi\cdot 2^{-53})^2}{\sqrt{n(1+2^{-53})^2+1}} - \pi\cdot 2^{-53} \end{aligned} $$ より、 $$ \begin{aligned} &\phantom{{}={}} {\libmcos{\libmatan{\libmsqrt{n}}}} \\ &= {\cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot (1+\delta_{\texttt{atan}}) )\cdot (1+\delta_{\texttt{cos}})} \\ &\gt \left(\frac{1-\tfrac12(\pi\cdot 2^{-53})^2}{\sqrt{n(1+2^{-53})^2+1}} - \pi\cdot 2^{-53}\right) \cdot (1-2^{-52}) \end{aligned} $$ が成り立つ。上界も同様にして、 $$ \begin{aligned} &\phantom{{}={}} {\cos(\arctan(\sqrt{n}\cdot (1+\delta_{\texttt{sqrt}}) )\cdot (1+\delta_{\texttt{atan}}) )} \\ &\lt \frac1{\sqrt{n(1+\delta_{\texttt{sqrt}})^2+1}} \cdot 1 + \frac{\sqrt{n(1+\delta_{\texttt{sqrt}})^2}}{\sqrt{n(1+\delta_{\texttt{sqrt}})^2+1}} \cdot \pi\cdot 2^{-53} \\ &\lt \frac1{\sqrt{n(1-2^{-53})^2+1}} + \pi\cdot 2^{-53} \end{aligned} $$ より従う。$\qed$
Claim 7: 任意の整数 $0\le n\lt 2^{31}$ に対して、 $$ n+0.5 \lt 1\oslash(\libmcos{\libmatan{\libmsqrt{n}}} \otimes \libmcos{\libmatan{\libmsqrt{n}}}) \lt n+1.5 $$ が成り立つ。
Proof
$$ \begin{aligned} &\phantom{{}={}} {\libmcos{\libmatan{\libmsqrt{n}}} \otimes \libmcos{\libmatan{\libmsqrt{n}}}} \\ &\gt \left(\left(\frac{1-\tfrac12(\pi\cdot 2^{-53})^2}{\sqrt{n(1+2^{-53})^2+1}} - \pi\cdot 2^{-53}\right) \cdot (1-2^{-52})\right)^2 (1-2^{-53}) \end{aligned} $$ および $$ \begin{aligned} \left(\frac{1-\tfrac12 a^2}{\sqrt{n(1+2^{-53})^2+1}}-a\right)^{-2} &= \left(\frac{1-\tfrac12 a^2 - a\sqrt{n(1+2^{-53})^2+1}}{\sqrt{n(1+2^{-53})^2+1}}\right)^{-2} \\ &= \frac{n(1+2^{-53})^2+1}{\left(1-\tfrac12 a^2 - a\sqrt{n(1+2^{-53})^2+1}\right)^2} \end{aligned} $$ を踏まえ、 $$ \begin{aligned} &\phantom{{}={}} {1\oslash(\libmcos{\libmatan{\libmsqrt{n}}} \otimes \libmcos{\libmatan{\libmsqrt{n}}})} \\ &\lt \left(\left(\frac{1-\tfrac12(\pi\cdot 2^{-53})^2}{\sqrt{n(1+2^{-53})^2+1}} - \pi\cdot 2^{-53}\right) \cdot (1-2^{-52})\right)^{-2} \frac{1+2^{-53}}{1-2^{-53}} \\ &= \left(\frac{1-\tfrac12(\pi\cdot 2^{-53})^2}{\sqrt{n(1+2^{-53})^2+1}} - \pi\cdot 2^{-53}\right)^{-2} \cdot \frac{1+2^{-53}}{(1-2^{-52})^2 (1-2^{-53})} \\ &\lt \left(\frac{1-\tfrac12(\pi\cdot 2^{-53})^2}{\sqrt{n(1+2^{-53})^2+1}} - \pi\cdot 2^{-53}\right)^{-2} \cdot (1+7\cdot 2^{-53}) \\ &= \frac{n(1+2^{-53})^2+1}{\left(1-\tfrac12 (\pi\cdot 2^{-53})^2 - \pi\cdot 2^{-53}\sqrt{n(1+2^{-53})^2+1}\right)^2} \cdot (1+7\cdot 2^{-53}) \\ &\lt \frac{(n+1)(1+2^{-53})^2}{\left(1-\tfrac12 (\pi\cdot 2^{-53})^2 - \pi\cdot 2^{-53}\sqrt{2^{31}\cdot(1+2^{-53})^2+1}\right)^2} \cdot (1+7\cdot 2^{-53}) \\ &\lt \frac{(n+1)(1+2^{-53})^2}{1-1.1108\cdot 2^{-35}} \cdot (1+7\cdot 2^{-53}) \\ &\lt (n+1)\cdot (1+1.1109\cdot 2^{-35}) \\ &= (n+1) + (n+1)\cdot(1.1109\cdot 2^{-35}) \\ &\le (n+1) + 2^{31}\cdot(1.1109\cdot 2^{-35}) \\ &= (n+1) + 1.1109\cdot 2^{-4} \\ &\lt (n+1) + 0.5 \end{aligned} $$ を得る。下界も同様に、 $$ \begin{aligned} &\phantom{{}={}} {1\oslash(\libmcos{\libmatan{\libmsqrt{n}}} \otimes \libmcos{\libmatan{\libmsqrt{n}}})} \\ &\gt \left(\left(\frac1{\sqrt{n(1-2^{-53})^2+1}} + \pi\cdot 2^{-53}\right) \cdot (1+2^{-52})\right)^{-2} \cdot \frac{1-2^{-53}}{1+2^{-53}} \\ &\gt \left(\frac1{\sqrt{n(1-2^{-53})^2+1}} + \pi\cdot 2^{-53}\right)^{-2} \cdot (1-7\cdot 2^{-53}) \\ % &= \left(\frac{1+\pi\cdot 2^{-53}\cdot \sqrt{n(1-2^{-53})^2+1}}{\sqrt{n(1-2^{-53})^2+1}}\right)^{-2} \cdot (1-7\cdot 2^{-53}) \\ &= \frac{n(1-2^{-53})^2+1}{\left(1+\pi\cdot 2^{-53}\cdot \sqrt{n(1-2^{-53})^2+1}\right)^2} \cdot (1-7\cdot 2^{-53}) \\ &\gt \frac{(n+1)(1-2^{-53})^2}{\left(1+\pi\cdot 2^{-53}\cdot \sqrt{2^{31}\cdot(1-2^{-53})^2+1}\right)^2} \cdot (1-7\cdot 2^{-53}) \\ &\gt \frac{(n+1)(1-2^{-53})^2}{1+1.1108\cdot 2^{-35}} \cdot (1-7\cdot 2^{-53}) \\ &\gt (n+1)\cdot (1-1.1109\cdot 2^{-35}) \\ &\ge (n+1) - 2^{-31}\cdot (1.1109\cdot 2^{-35}) \\ &= (n+1) - 1.1109\cdot 2^{-4} \\ &\gt (n+1) - 0.5. \quad\qed \end{aligned} $$
Corollary 8: 下記のコードは、x >= 0 かつ x < i32::MAX に対して x + 1 を返す。
fn plus1(x: i32) -> i32 { (x as f64).sqrt().atan().cos().powi(2).recip().round() as _ }
なお、$2^{31}$ 個程度なので全部のテストを回すことはできます。2.5 分くらいで終わりました。
？？？
探してみたらなんとか見つかった。 x+1=exp(tan(arcsin(cos(arctan(log(√(exp(tan(arcsin(cos(arctan(log(tan(arcsin(cos(arctan(cos(arctan(√(x)))))))))))))))))))) らしいです。
— くりんぺっと (@climpet) 2024年4月10日
え、これもやるんですか......？ round を除いて 20 個のチェーンになっていてやばい。
fn plus1_20chain(x: f64) -> f64 { x.sqrt().atan().cos().atan().cos().asin().tan() .ln().atan().cos().asin().tan().exp().sqrt() .ln().atan().cos().asin().tan().exp().round() }
plus1_20chain(67112958.0) が 67112958.0 を返したので、f64 だと正当ではなさそうです。（示す必要がなくて）よかった〜。
$67112958 = 2^{26}+2^{12}-2^1$ です。$(2^{53-1})^{1/2}$ くらいで反例ありがち（？）。
Twitter を漁ったところ、（よくある）数字 4 つで 10 を作るみたいなやつの文脈で 2011 年頃に言及されているのが見つかりました。
一応示します。
Claim 9: 実数 $x\gt 0$ に対して $S(x)$ を下記に基づいて定義する。
exp(tan(arcsin(cos(arctan(log(√(exp(tan(arcsin(cos(arctan(log(tan(arcsin(cos(arctan(cos(arctan(√(x))))))))))))))))))
このとき、$S(x) = x+1$ が成り立つ。
Proof
$$ \begin{aligned} \cos(\arctan(x) ) &= \frac1{\sqrt{1+x^2}}, \\ \tan(\arcsin(x) ) &= \frac x{\sqrt{1-x^2}}, \\ \log(\sqrt{\exp(x)}) &= \frac x2 \end{aligned} $$ を踏まえ、 $$ \begin{aligned} f(x) &= \frac1{\sqrt{1+x^2}}, \\ g(x) &= \frac x{\sqrt{1-x^2}}, \\ h(x) &= \frac x2 \end{aligned} $$ とすると、 $$ \begin{aligned} S(x) &=\exp(g(f(h(g(f(\log(g(f(f(\sqrt{x}) ) ) ) ) ) ) ) ) ) \\ &= ({\exp}\circ g\circ f\circ h\circ g\circ f\circ {\log}\circ g\circ f\circ f)(\sqrt x) \end{aligned} $$ となる。 $$ \begin{aligned} (g\circ f)(x) &= \frac{1/\sqrt{1+x^2}}{\sqrt{1-1/(1+x^2)}} \\ &= \frac{1/\sqrt{1+x^2}}{\sqrt{x^2/(1+x^2)}} \\ &= \frac{1/\sqrt{1+x^2}}{x\sqrt{1+x^2}} \\ &= \frac1x \end{aligned} $$ より、 $$ r(x) = \frac1x $$ とすると、 $$ S(x) = ({\exp}\circ r\circ h\circ r\circ {\log}\circ r\circ f)(\sqrt x) $$ となる。 $$ \begin{aligned} (r\circ f)(\sqrt x) &= (x+1)^{1/2}, \\ (r\circ h\circ r)(x) &= 2x \end{aligned} $$ を踏まえ、 $$ \begin{aligned} S(x) &= \exp(2\log( (x+1)^{1/2}) ) \\ &= \exp(\log(x+1) ) \\ &= x+1 \end{aligned} $$ を得る。$\qed$
初見だと面喰らいますが、「初等関数の組み合わせで $1/x$ や $x/2$ などを作るよ〜」という前提で考えるとわりと自然に作れるかもしれません？ $$ \begin{aligned} \tan(\arcsin(\cos(\arctan(x) ) ) ) &= \tan(\arcsin(\sin(\tfrac\pi2-\arctan(x) ) ) ) \\ &= \tan(\tfrac\pi2-\arctan(x) ) \\ &= 1/{\tan(\arctan(x) )} \\ &= 1/x \end{aligned} $$ と考えると、そこまで突飛でもないような気がします。そうかな、どうでしょう*1。
ということで、（Claim 9 の証明の中での定義を用いると）$f(\sqrt x)$ に相当する部分の評価は Claim 6 で済んでいる*2ので、$r$ や $h$ や $r\circ h\circ r$ の評価ができれば、それらの組み合わせでどうにかなる気がします。f64 では反例があったので、$2^{-53}$ の部分を $2^{-64}$ や $2^{-113}$ などに適宜置き換える想定です。
$\tan(x+\delta) = \tan(x) + \varepsilon_{\delta}$ みたいなのをうまく押さえられるのかがよくわかりません。 $r\circ h\circ r$ の入力は $\log$ の出力であり、その前に平方根もついていることを考えると、入力としては高々 $21.488$ 程度の実数を想定すればよさそうです。 とはいえ最後に $\exp$ に入れるので、少しの誤差でとんでもないことになりそうな気がします。 $$ \begin{aligned} \log(2^{31}) - \log(2^{31}-0.5) &= -\log(1-2^{-32}) \\ &\approx 2^{-32} \end{aligned} $$ なので、$2^{-32}$ くらいずれるとだめになっちゃいそうです。
$53$-bit 精度での最小反例が $2^{26}$ 付近だったことから予想すると、$64$-bit 精度なら足りることが示せるんじゃないかな〜という気はしますが、あまり自信はありません。 たいへんそうなので今回はここで投げ出します。気が向いたらまた考えるかもしれません。
$64$-bit 精度版について、全量テストはパスしたので正当ではあると思います（？？）。エミュレートが重いのか、$2^{31}-1$ 未満を試すのに手元環境で半日くらいかかりました。
$3036970419$ のとき、round の入力が $3036970420.5{\small 000031315721571}{\footnotesize 445465087890625}$ となっていました。
これが最小反例で、$3036970419 \approx 2^{31.5} - 2^{14.875}$ くらいです。
$2^{(p-1)/2}$ くらい以下の範囲では大丈夫なことが示せたりしますか？ 適当にしゃべっています。 libm のバージョンやその他諸々が違うと変わる気もします。
あとがき
Claim 1 の方法については、15 年くらい前のえびちゃんも見つけていたような気がしますが、あまり覚えていません。記憶の改竄があるかもしれません。そのときも make 10 の文脈だったような気がします。
Claim 9 に関しては 1 年前に投げ出したっきりだったので、今回ちゃんと納得できてよかったです。
これに対しても $(S\circ\cdots\circ S)( (2-2)\cdot 2)$ でできますね。コメント欄では
exp(exp(-ln(-ln(√(exp(-exp(-ln(-ln(cos(arctan(√(n))))))))))))=n+1
が言及されていました。自分の頭が「単項マイナスが使えるとかヌルゲーすぎるだろ（？？？）」のような思考になっていて、あぶないです*3。
$$ \begin{aligned} N(x) &= ({\log}\circ{\tan}\circ{\arcsin}\circ{\cos}\circ{\arctan}\circ{\exp})(x) \\ &= ({\log}\circ r\circ{\exp})(x) \\ &= \log(e^{-x}) \\ &= -x \end{aligned} $$ を用いて、負数についても $(N\circ S\circ\cdots\circ S)( (2-2)\cdot 2)$ とできます。 あるいは、$(N\circ S^n\circ N)(x) = x-n$ も成り立つので、減らしたい問題設定のときにも便利ですね。
最近は別のトピックの記事を書くのをがんばっていたのですが、「あ、そういえば！💡」と思って浮動小数点型の記事に戻ってきてしまい、ヒ〜という感じです。
おわり
おわりです。
