Villager Bを解いたのでその記録 大まかな方針だけ書くようにしますが自力で解きたい人は見ないでください 問題の確認 To be more secure I enabled several security options as follows: Randomized addresses of the program (-pie) Protected the stack …

今まで何となく使っていたcoqのタクティックの動作を少し詳しく見てみることにした。ソースコードを読むべきかもしれないけど、まずは実際どう動くかを観察して解釈することにした 以下はその記録 destruct and(/\)のdestruct Goal forall P Q: Prop, P/\Q -…