{"id":156413,"date":"2012-10-29T07:43:03","date_gmt":"2012-10-29T03:43:03","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=156413"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=156413","title":{"rendered":"<span class=\"post_title\">\u0412\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043d\u0430 ARM \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u0435<\/span>"},"content":{"rendered":"<div class=\"content html_format\">   \t\u0412 \u0441\u0432\u043e\u0435\u0439 \u043f\u0440\u043e\u0448\u043b\u043e\u0439 <a href=\"http:\/\/habrahabr.ru\/post\/148709\/\">\u0441\u0442\u0430\u0442\u044c\u0435<\/a> \u044f \u043e\u043f\u0438\u0441\u0430\u043b \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u0438\u043c\u0438\u0442\u0438\u0432\u043d\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043d\u0430 \u0421\u0438. \u041f\u0430\u0440\u0430\u043b\u043b\u0435\u043b\u044c\u043d\u043e \u043f\u0440\u0438\u0432\u0435\u043b \u0441\u043e\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u044f, \u043f\u043e\u0447\u0435\u043c\u0443 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0421\u0438 \u043a\u043e\u0434\u0430 \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u0430 \u0434\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431 \u0441\u0447\u0438\u0442\u0430\u0442\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443 \u0431\u0435\u0437\u043e\u0448\u0438\u0431\u043e\u0447\u043d\u043e\u0439. \u0412 \u043e\u0441\u043d\u043e\u0432\u043d\u043e\u043c \u044d\u0442\u0438 \u0441\u043e\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u0441\u0432\u043e\u0434\u044f\u0442\u0441\u044f \u043a \u043c\u044b\u0441\u043b\u0438, \u0447\u0442\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043a\u043e\u0434 \u2014 \u044d\u0442\u043e \u0442\u043e\u043b\u044c\u043a\u043e \u0447\u0430\u0441\u0442\u044c \u0438\u0441\u0442\u043e\u0440\u0438\u0438 \u043e \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u0438\u0438 \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0449\u0435\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b. \u0421\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043f\u0440\u0438\u0431\u043b\u0438\u0436\u0435\u043d\u0438\u0435\u043c \u043a \u0442\u043e\u043c\u0443, \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0431\u0435\u0437\u043e\u0448\u0438\u0431\u043e\u0447\u043d\u0443\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443, \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u043d\u044b\u0445 \u043a\u043e\u0434\u043e\u0432, \u0438\u0445 \u0443\u0436\u0435 \u043d\u0435 \u043d\u0443\u0436\u043d\u043e \u0431\u0443\u0434\u0435\u0442 \u0442\u0440\u0430\u043d\u0441\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0438 \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u0438\u0441\u043a\u043b\u044e\u0447\u0438\u0442\u0441\u044f \u043e\u0431\u0448\u0438\u0440\u043d\u043e\u0435 \u043f\u043e\u043b\u0435 \u0434\u043b\u044f \u0432\u043e\u0437\u043d\u0438\u043a\u043d\u043e\u0432\u0435\u043d\u0438\u044f \u043e\u0448\u0438\u0431\u043e\u043a. \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043e\u043f\u0438\u0448\u0443 \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u0443\u0436\u0435 \u0434\u043b\u044f \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043d\u0430 \u043f\u043e\u0440\u044f\u0434\u043e\u043a \u043f\u0440\u0438\u043c\u0438\u0442\u0438\u0432\u043d\u0435\u0439, \u0447\u0435\u043c \u0434\u0430\u0436\u0435 \u043f\u0440\u043e\u0441\u0442\u0435\u0439\u0448\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u043d\u0430 \u0421\u0438, \u043e \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0433\u043e\u0432\u043e\u0440\u0438\u043b\u043e\u0441\u044c \u0432 \u043f\u0440\u043e\u0448\u043b\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435. <br \/>  <a name=\"habracut\"><\/a>\u0412\u043e\u0442 \u044d\u0442\u043e\u0442 \u043a\u043e\u0434:<\/p>\n<pre><code>0x00: subs r0, r0, #1 0x04: bne 0x0C 0x08: mov r1, #0 0x0C: mov r1, #1 <\/code><\/pre>\n<p>  \u041f\u043e\u0441\u043b\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u044d\u0442\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u0432 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0438 \u043e\u0442 \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0430 <code>r0<\/code> \u0435\u0434\u0438\u043d\u0438\u0446\u0435 \u0432 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0435 <code>r1<\/code> \u043e\u043a\u0430\u0436\u0435\u0442\u0441\u044f \u043b\u0438\u0431\u043e \u043e\u0434\u0438\u043d, \u043b\u0438\u0431\u043e \u043d\u043e\u043b\u044c.<\/p>\n<p>  \u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u0441\u043a\u0430\u0436\u0443 \u0435\u0449\u0435 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u043b\u043e\u0432 \u043e \u0441\u0430\u043c\u043e\u043c \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u043d\u043e\u043c \u043a\u043e\u0434\u0435. \u0412 \u0434\u0430\u043d\u043d\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u0440\u0435\u0447\u044c \u0438\u0434\u0435\u0442 \u043d\u0435 \u043e\u0431 \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u0435 \u043a\u0430\u043a \u044f\u0437\u044b\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u0430 \u043e \u043c\u0430\u0448\u0438\u043d\u043d\u044b\u0445 \u043a\u043e\u0434\u0430\u0445. \u0422\u043e \u0435\u0441\u0442\u044c \u0437\u0434\u0435\u0441\u044c \u0431\u0443\u0434\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u0430\u043d\u043e \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435 \u043e \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0435 \u0432 \u0431\u0438\u043d\u0430\u0440\u043d\u043e\u043c \u0432\u0438\u0434\u0435:<\/p>\n<pre><code>0xE2500001 0x1A000000 0xE3A01000 0xE3A01001 <\/code><\/pre>\n<p>  \u0415\u0441\u043b\u0438 \u0431\u044b \u043c\u044b \u0433\u043e\u0432\u043e\u0440\u0438\u043b\u0438 \u043e\u0431 \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u0435, \u0442\u043e \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0439 \u043e \u043a\u043e\u0434\u0435 \u043d\u0430 \u0432\u044b\u0441\u043e\u043a\u043e\u0443\u0440\u043e\u0432\u043d\u0435\u0432\u044b\u0445 \u044f\u0437\u044b\u043a\u0430\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043e\u0441\u0442\u0430\u043b\u0438\u0441\u044c \u0431\u044b \u0432 \u0441\u0438\u043b\u0435. \u0410 \u0438\u043c\u0435\u043d\u043d\u043e \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e\u0441\u0442\u044c \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u0438\u043c\u0435\u0442\u044c \u0438 \u0434\u043e\u0432\u0435\u0440\u044f\u0442\u044c \u0438\u043c\u0435\u044e\u0449\u0435\u0439\u0441\u044f \u043c\u043e\u0434\u0435\u043b\u0438 \u044f\u0437\u044b\u043a\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u043d\u043e \u0438 \u0434\u043e\u0432\u0435\u0440\u044f\u0442\u044c \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440\u0443, \u0430 \u0432 \u0438\u0434\u0435\u0430\u043b\u0435 \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0435\u0433\u043e. \u0421\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u044b \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u044e\u0442 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u0435\u0439, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043c\u043e\u0434\u0443\u043b\u044c\u043d\u043e\u0433\u043e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u0430 \u0437\u043d\u0430\u0447\u0438\u0442 \u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u0441\u044f \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u0430 \u043a\u043e\u043c\u043f\u043e\u043d\u043e\u0432\u043a\u0430. \u0417\u0434\u0435\u0441\u044c \u0436\u0435 \u0441\u0442\u0430\u0434\u0438\u044f \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0446\u0438\u0438 \u0438 \u043a\u043e\u043c\u043f\u043e\u043d\u043e\u0432\u043a\u0438 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442.<\/p>\n<p>  \u0414\u043b\u044f \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u044f \u0431\u0443\u0434\u0443 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c\u0441\u044f \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e\u043c \u0434\u043b\u044f \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/HOL\/\">HOL<\/a> (\u0438\u043b\u0438 \u043d\u0430 <a href=\"https:\/\/github.com\/mn200\/HOL\/\">github&#8217;\u0435<\/a>) \u0438 \u0441\u043e\u0437\u0434\u0430\u043d\u043d\u043e\u0439 \u0434\u043b\u044f \u043d\u0435\u0433\u043e <a href=\"https:\/\/github.com\/mn200\/HOL\/blob\/master\/examples\/ARM\/v4\/\">\u043c\u043e\u0434\u0435\u043b\u044c\u044e<\/a> \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u043d\u044b\u0445 \u0438\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u0438 \u0434\u043b\u044f ARMv4. \u041f\u043e\u0441\u043b\u0435 \u0442\u043e\u0433\u043e \u043a\u0430\u043a \u0432\u044b \u043f\u043e\u043b\u0443\u0447\u0438\u043b\u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u044e\u044e \u0432\u0435\u0440\u0441\u0438\u044e HOL, \u0441\u043a\u043e\u043c\u043f\u0438\u043b\u0438\u0440\u043e\u0432\u0430\u043b\u0438 \u0435\u0451 \u0438 \u043c\u043e\u0434\u0435\u043b\u044c ARMv4 \u2014 \u043c\u043e\u0436\u0435\u0442\u0435 \u043f\u0440\u043e\u0434\u0435\u043b\u0430\u0442\u044c \u0432\u0441\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430. \u041a\u043e\u0434 \u044f \u043f\u0440\u0438\u0432\u0435\u0434\u0443 \u0446\u0435\u043b\u0438\u043a\u043e\u043c, \u0447\u0442\u043e\u0431\u044b \u0443 \u0442\u0435\u0445, \u043a\u043e\u043c\u0443 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e, \u0431\u044b\u043b\u0430 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u043f\u043e\u0432\u0442\u043e\u0440\u0438\u0442\u044c \u0432\u0441\u0435 \u0448\u0430\u0433\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430.<\/p>\n<p>  \u0411\u0443\u0434\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u0430\u043d\u043e \u0434\u0432\u0435 \u0442\u0435\u043e\u0440\u0435\u043c\u044b. \u041f\u0435\u0440\u0432\u0430\u044f <code>goal_eq1<\/code> \u043e \u0442\u043e\u043c, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0430 <code>r0<\/code> \u0440\u0430\u0432\u043d\u043e 1, \u0442\u043e \u0447\u0435\u0440\u0435\u0437 \u0442\u0440\u0438 \u0448\u0430\u0433\u0430 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0432 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0435 <code>r1<\/code> \u0431\u0443\u0434\u0435\u0442 0, \u0442\u0430\u043a\u0436\u0435 \u043a\u0430\u043a \u0438 \u0432\u043e \u0432\u0441\u0435\u0445 \u043e\u0441\u0442\u0430\u043b\u044c\u043d\u044b\u0445 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0430\u0445 \u043e\u0431\u0449\u0435\u0433\u043e \u043d\u0430\u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f:<\/p>\n<pre><code class=\"haskell\">|- ((x :bool[32]) = (1w :bool[32])) \u21d2    (STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)       &lt;|registers := (r0 =+ x) (\u03bb(n :register). (0w :bool[32]));         psrs :=           (\u03bb(x :psr).              SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));         memory :=           ((0w :bool[30]) |:            [             enc               (SUB AL T (0w :bool[4]) (0w :bool[4])                  (Dp_immediate (0w :bool[4]) (1w :bool[8])) :                  arm_instruction);             enc (B NE (0w :bool[24]));             enc               (MOV AL F (1w :bool[4])                  (Dp_immediate (0w :bool[4]) (0w :bool[8])));             enc               (MOV AL F (1w :bool[4])                  (Dp_immediate (0w :bool[4]) (1w :bool[8])))             ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32]));         undefined := F; cp_state := ()|&gt; =     &lt;|registers :=         (pc =+ (12w :bool[32])) (\u03bb(n :register). (0w :bool[32]));       psrs :=         (CPSR =+ SET_NZCV (F,T,T,F) (SET_IFMODE F F usr (0w :bool[32])))           (\u03bb(x :psr).              SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));       memory :=         ((0w :bool[30]) |:          [           enc             (SUB AL T (0w :bool[4]) (0w :bool[4])                (Dp_immediate (0w :bool[4]) (1w :bool[8])) :                arm_instruction);           enc (B NE (0w :bool[24]));           enc             (MOV AL F (1w :bool[4])                (Dp_immediate (0w :bool[4]) (0w :bool[8])));           enc             (MOV AL F (1w :bool[4])                (Dp_immediate (0w :bool[4]) (1w :bool[8])))           ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;       cp_state := ()|&gt;) <\/code><\/pre>\n<p>  \u0412\u0442\u043e\u0440\u0430\u044f \u0442\u0435\u043e\u0440\u0435\u043c\u0430 <code>goal_ne1<\/code>, \u043e \u0442\u043e\u043c \u0435\u0441\u043b\u0438 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0430 <code>r0<\/code> \u043d\u0435 \u0440\u0430\u0432\u043d\u043e 1, \u0442\u043e \u0447\u0435\u0440\u0435\u0437 \u0442\u0440\u0438 \u0448\u0430\u0433\u0430 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0432 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0435 <code>r1<\/code> \u0431\u0443\u0434\u0435\u0442 1:<\/p>\n<pre><code class=\"haskell\">|- (x :bool[32]) \u2260 (1w :bool[32]) \u21d2    \u2203(a :bool) (c :bool) (d :bool).      STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)        &lt;|registers := (r0 =+ x) (\u03bb(n :register). (0w :bool[32]));          psrs :=            (\u03bb(x :psr).               SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));          memory :=            ((0w :bool[30]) |:             [              enc                (SUB AL T (0w :bool[4]) (0w :bool[4])                   (Dp_immediate (0w :bool[4]) (1w :bool[8])) :                   arm_instruction);              enc (B NE (0w :bool[24]));              enc                (MOV AL F (1w :bool[4])                   (Dp_immediate (0w :bool[4]) (0w :bool[8])));              enc                (MOV AL F (1w :bool[4])                   (Dp_immediate (0w :bool[4]) (1w :bool[8])))              ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32]));          undefined := F; cp_state := ()|&gt; =      &lt;|registers :=          (pc =+ (16w :bool[32]))            ((r1 =+ (1w :bool[32]))               ((r0 =+                 (n2w                    (MOD_2EXP (32 :num)                       (w2n x + (4294967294 :num) + (1 :num))) :                    bool[32])) (\u03bb(n :register). (0w :bool[32]))));        psrs :=          (CPSR =+           SET_NZCV (a,F,c,d) (SET_IFMODE F F usr (0w :bool[32])))            (\u03bb(x :psr).               SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));        memory :=          ((0w :bool[30]) |:           [            enc              (SUB AL T (0w :bool[4]) (0w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])) :                 arm_instruction);            enc (B NE (0w :bool[24]));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (0w :bool[8])));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])))            ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;        cp_state := ()|&gt; <\/code><\/pre>\n<p>  \u041a\u043e\u0434 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u044d\u0442\u0438\u0445 \u0442\u0435\u043e\u0440\u0435\u043c \u044f \u043f\u043e\u0447\u0442\u0438 \u043d\u0435 \u0431\u0443\u0434\u0443 \u043a\u043e\u043c\u043c\u0435\u043d\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u2014 \u044f\u0441\u043d\u043e, \u0447\u0442\u043e \u043f\u043e \u0441\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044e \u0441, \u043a\u0430\u0437\u0430\u043b\u043e\u0441\u044c \u0431\u044b, \u043f\u0440\u043e\u0441\u0442\u043e\u0442\u043e\u0439 \u0438 \u043f\u043e\u0447\u0442\u0438 \u043e\u0447\u0435\u0432\u0438\u0434\u043d\u043e\u0441\u0442\u044c\u044e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u043a\u043e\u0434 \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043c\u0430\u0448\u0438\u043d\u043e\u0439 \u0434\u043e\u043b\u0436\u0435\u043d \u0431\u044b\u0442\u044c \u043d\u0435\u0441\u0443\u0440\u0430\u0437\u043d\u043e \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u044b\u043c.<\/p>\n<p>  \u0412\u043d\u0430\u0447\u0430\u043b\u0435 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0437\u0430\u0433\u0440\u0443\u0437\u0438\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u044c ARMv4, \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0435 \u043a\u043e\u043d\u0441\u0442\u0430\u043d\u0442\u044b \u0438 \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u043e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443.<\/p>\n<pre><code class=\"haskell\">FileSys.chDir &quot;\/home\/path\/to\/your\/HOL\/examples\/ARM\/v4&quot;; load &quot;arm_evalLib&quot;; open arm_evalLib;  val _ = overload_on(&quot;sp&quot;, ``r13``); val _ = overload_on(&quot;lr&quot;, ``r14``); val _ = overload_on(&quot;pc&quot;, ``r15``);  fun evaluate_st n state = \tlet val memory = (rhs o concl) (SIMP_CONV (srw_ss()) [] ``^(state).memory``) \t    val registers = (rhs o concl) (SIMP_CONV (srw_ss()) [] ``^(state).registers``) \t    val psrs = (rhs o concl) (SIMP_CONV (srw_ss()) [] ``^(state).psrs``) \tin evaluate(n, memory, registers, psrs) end; fun evaluate_CONV state = evaluate_st 1 state;  val reg_r0_x = set_registers empty_registers `[(r0,x)]`; val reg_r0_1 = set_registers empty_registers `[(r0,1w)]`;  val psr = set_status_registers empty_psrs  `[(CPSR,SET_NZCV (F,F,F,F) (SET_IFMODE F F usr 0w))]`;  val prog = list_assemble empty_memory    [&quot;0x00: subs r0, r0, #1&quot;,     &quot;0x04: bne 0x0C&quot;,     &quot;0x08: mov r1, #0&quot;,     &quot;0x0C: mov r1, #1&quot;]; <\/code><\/pre>\n<p>  \u0422\u0435\u043f\u0435\u0440\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043f\u0435\u0440\u0432\u043e\u0439 \u0438\u0437 \u0442\u0435\u043e\u0440\u0435\u043c \u0438 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u044b\u0445 \u043b\u0435\u043c\u043c. \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0442\u0430\u043a: \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f, \u0447\u0442\u043e \u043f\u043e\u0441\u043b\u0435 \u043e\u0434\u043d\u043e\u0433\u043e \u0448\u0430\u0433\u0430 \u0431\u0443\u0434\u0435\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u043a\u043e\u043d\u043a\u0440\u0435\u0442\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u043e\u0432, \u0437\u0430\u0442\u0435\u043c \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f, \u0447\u0442\u043e \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u044b\u0439 \u0431\u0438\u0442 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0430 \u0441\u0442\u0430\u0442\u0443\u0441\u0430 \u0431\u0443\u0434\u0435\u0442 \u0440\u0430\u0432\u0435\u043d 1, \u0437\u0430\u0442\u0435\u043c \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u043f\u0440\u043e \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0435 \u0434\u0432\u0430 \u0448\u0430\u0433\u0430 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f, \u0438 \u044d\u0442\u0438 \u0434\u0432\u0430 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u0434\u043b\u044f \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0446\u0435\u043b\u0435\u0432\u043e\u0439 \u0442\u0435\u043e\u0440\u0435\u043c\u044b.<\/p>\n<pre><code class=\"haskell\">val f1vx = evaluate(1,prog,reg_r0_x,psr); val f1vx_lhsc = (lhs o concl) f1vx; val f1vx_rhsc = (rhs o concl) f1vx; val f1v1 = evaluate(1,prog,reg_r0_1,psr); val f1v1_rhsc = (rhs o concl) f1v1; val f1v_thm = prove(``(x = 1w) ==&gt; (^(f1vx_lhsc) = ^(f1v1_rhsc))``, SIMP_TAC (srw_ss()) [f1vx, combinTheory.UPDATE_def]);  val f2v1 = evaluate_CONV f1v1_rhsc; val f2v1_rhsc = (rhs o concl) f2v1; val f2vx = evaluate_CONV f1vx_rhsc; val f2vx_lhsc = (lhs o concl) f2vx; val f2v_thm = prove(``(x = 1w) ==&gt; (^(f2vx_lhsc) = ^(f2v1_rhsc))``, SIMP_TAC (srw_ss()) [f2vx, combinTheory.UPDATE_def]); val f2v_thm_rhsc = (rhs o concl) (UNDISCH f2v_thm);  val f2f1v_thm = prove(``STATE_ARM_MMU (NO_CP :unit coproc) (2 :num) x = STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) (STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) x)``, REWRITE_TAC [systemTheory.STATE_ARM_MMU_def, numLib.num_CONV ``2``, numLib.num_CONV ``1``]); val subgoal_eq1 = prove(``(x = 1w) ==&gt; (STATE_ARM_MMU (NO_CP :unit coproc) (2 :num)      &lt;|registers :=          (r0 =+ (x :bool[32])) (\u03bb(n :register). (0w :bool[32]));        psrs :=          (\u03bb(x :psr).             SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));        memory :=          ((0w :bool[30]) |:           [            enc              (SUB AL T (0w :bool[4]) (0w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])) :                 arm_instruction);            enc (B NE (0w :bool[24]));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (0w :bool[8])));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])))            ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;        cp_state := ()|&gt; = ^(f2v1_rhsc))``, REWRITE_TAC [f1vx, f2v_thm, f2f1v_thm]);  val f3v1 = evaluate_CONV f2v_thm_rhsc; val f3v1_rhsc = (rhs o concl) f3v1; val f3f2v_thm = prove(``STATE_ARM_MMU (NO_CP :unit coproc) (3 :num) x = STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) (STATE_ARM_MMU (NO_CP :unit coproc) (2 :num) x)``, REWRITE_TAC [systemTheory.STATE_ARM_MMU_def, numLib.num_CONV ``3``, numLib.num_CONV ``1``]); val goal_eq1 = prove(``(x = 1w) ==&gt; (STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)      &lt;|registers :=          (r0 =+ (x :bool[32])) (\u03bb(n :register). (0w :bool[32]));        psrs :=          (\u03bb(x :psr).             SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));        memory :=          ((0w :bool[30]) |:           [            enc              (SUB AL T (0w :bool[4]) (0w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])) :                 arm_instruction);            enc (B NE (0w :bool[24]));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (0w :bool[8])));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])))            ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;        cp_state := ()|&gt; = ^(f3v1_rhsc))``, DISCH_TAC THEN REWRITE_TAC [f3v1, UNDISCH subgoal_eq1, f3f2v_thm]); <\/code><\/pre>\n<p>  \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u0432\u0442\u043e\u0440\u043e\u0439 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u043b\u043e\u0436\u043d\u0435\u0439, \u0442\u0430\u043a \u043a\u0430\u043a \u0442\u0430\u043c \u0443\u0447\u0430\u0441\u0442\u0432\u0443\u0435\u0442 \u043e\u0442\u0440\u0438\u0446\u0430\u043d\u0438\u0435. \u041e\u0442\u043b\u0438\u0447\u0438\u044f \u043e\u0442 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043f\u0435\u0440\u0432\u043e\u0439 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0434\u043b\u044f \u0442\u043e\u0433\u043e \u0447\u0442\u043e\u0431 \u043d\u0435 \u0442\u044f\u043d\u0443\u0442\u044c \u0437\u0430 \u0441\u043e\u0431\u043e\u0439 \u0441\u0438\u043c\u0432\u043e\u043b\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u0434\u043b\u044f \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 \u043d\u0435\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0445 \u0431\u0438\u0442\u043e\u0432 \u0440\u0435\u0433\u0438\u0441\u0442\u0440\u0430 \u0441\u0442\u0430\u0442\u0443\u0441\u0430 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u043a\u0432\u0430\u043d\u0442\u043e\u0440\u044b \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043e\u0432\u0430\u043d\u0438\u044f.<\/p>\n<pre><code class=\"haskell\">val ef1vx = prove(``?a c d. ^(f1vx_lhsc) =  &lt;|registers :=        (pc =+ (4w :bool[32]))          ((r0 =+            (n2w               (MOD_2EXP (32 :num)                  (w2n x + (4294967294 :num) + (1 :num))) :bool[32]))             (\u03bb(n :register). (0w :bool[32])));      psrs :=        (CPSR =+         SET_NZCV           (a,            MOD_2EXP (32 :num) (w2n x + (4294967294 :num) + (1 :num)) =            (0 :            num),            c,            d)           (SET_IFMODE F F usr (0w :bool[32])))          (\u03bb(x :psr).             SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));      memory :=        ((0w :bool[30]) |:         [          enc            (SUB AL T (0w :bool[4]) (0w :bool[4])               (Dp_immediate (0w :bool[4]) (1w :bool[8])) :               arm_instruction);          enc (B NE (0w :bool[24]));          enc            (MOV AL F (1w :bool[4])               (Dp_immediate (0w :bool[4]) (0w :bool[8])));          enc            (MOV AL F (1w :bool[4])               (Dp_immediate (0w :bool[4]) (1w :bool[8])))          ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;      cp_state := ()|&gt;``, EXISTS_TAC ``(BIT (31 :num) (MOD_2EXP (32 :num) (w2n (x :bool[32]) + (4294967294 :num) + (1 :num))))`` THEN EXISTS_TAC ``ODD  (DIV_2EXP (32 :num) (w2n (x :bool[32]) + (4294967294 :num) + (1 :num)))`` THEN EXISTS_TAC ``word_msb (x :bool[32]) \/\\ (BIT (31 :num) (MOD_2EXP (32 :num) (w2n x + (4294967294 :num) + (1 :num))) &lt;&gt; word_msb x)`` THEN REWRITE_TAC [f1vx]);  val MODlem1 = prove(``!x. (x MOD 4294967296 = 0) ==&gt; (?k. (x = 4294967296*k))``, RW_TAC arith_ss [] THEN ASSUME_TAC (SPEC ``x :num`` (SIMP_RULE (srw_ss()) [] (SPEC ``4294967296`` arithmeticTheory.DIVISION))) THEN EXISTS_TAC ``x DIV (4294967296 :num)`` THEN RW_TAC arith_ss []);  val CPSRlem1 = prove(``((x :bool[32]) &lt;&gt; 1w) ==&gt; ((MOD_2EXP (32 :num) (w2n x + (4294967294 :num) + (1 :num)) = (0 : num)) = F)``, SIMP_TAC (arith_ss) [arithmeticTheory.MOD_2EXP_def] THEN DISCH_TAC THEN SPOSE_NOT_THEN ASSUME_TAC THEN UNDISCH_TAC ``(x :bool[32]) &lt;&gt; (1w :bool[32])`` THEN RW_TAC bool_ss [] THEN  SIMP_TAC arith_ss [MODlem1] THEN ASSUME_TAC (SPEC ``w2n (x :bool[32]) + (4294967295 :num)``  MODlem1) THEN `?(k :num). w2n x + (4294967295 :num) = (4294967296 :num) * k` by (RW_TAC arith_ss []) THEN `(k :num) &gt; 0` by FULL_SIMP_TAC arith_ss [] THEN `?(r :num). w2n (x :bool[32]) =  (4294967296 :num) * (r :num) + 1` by EXISTS_TAC ``(k :num) - 1`` THEN ASM_SIMP_TAC arith_ss [] THEN ` w2n (x :bool[32]) = (1 :num)` by ASSUME_TAC (SPEC ``(x :bool[32])`` (INST_TYPE [alpha |-&gt; ``:32``] wordsTheory.w2n_lt)) THEN FULL_SIMP_TAC (arith_ss ++ wordsLib.SIZES_ss) [] THEN PROVE_TAC [wordsTheory.n2w_w2n]);  val subgoal_ne1 = prove(``((x :bool[32]) &lt;&gt; 1w) ==&gt; (?a c d. ^(f1vx_lhsc) =  &lt;|registers :=        (pc =+ (4w :bool[32]))          ((r0 =+            (n2w               (MOD_2EXP (32 :num)                  (w2n x + (4294967294 :num) + (1 :num))) :bool[32]))             (\u03bb(n :register). (0w :bool[32])));      psrs :=        (CPSR =+         SET_NZCV           (a,            F,            c,            d)           (SET_IFMODE F F usr (0w :bool[32])))          (\u03bb(x :psr).             SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));      memory :=        ((0w :bool[30]) |:         [          enc            (SUB AL T (0w :bool[4]) (0w :bool[4])               (Dp_immediate (0w :bool[4]) (1w :bool[8])) :               arm_instruction);          enc (B NE (0w :bool[24]));          enc            (MOV AL F (1w :bool[4])               (Dp_immediate (0w :bool[4]) (0w :bool[8])));          enc            (MOV AL F (1w :bool[4])               (Dp_immediate (0w :bool[4]) (1w :bool[8])))          ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;      cp_state := ()|&gt;)``, DISCH_TAC THEN ASSUME_TAC (UNDISCH CPSRlem1) THEN ASSUME_TAC ef1vx THEN FULL_SIMP_TAC pure_ss [] THEN EXISTS_TAC ``a :bool`` THEN EXISTS_TAC ``c :bool`` THEN  EXISTS_TAC ``d :bool`` THEN REWRITE_TAC []);  val f3f1v_thm = prove(``STATE_ARM_MMU (NO_CP :unit coproc) (3 :num) x = STATE_ARM_MMU (NO_CP :unit coproc) (2 :num) (STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) x)``, REWRITE_TAC [systemTheory.STATE_ARM_MMU_def, numLib.num_CONV ``3``, numLib.num_CONV ``2``, numLib.num_CONV ``1``]); val f32vx = evaluate_st 2 (rhs (# 2 (strip_exists (concl (UNDISCH subgoal_ne1))))); val f32vx_rhsc = (rhs o concl) f32vx; val goal_ne1 = prove(``((x :bool[32]) &lt;&gt; 1w) ==&gt; (?a c d. (STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)      &lt;|registers :=          (r0 =+ (x :bool[32])) (\u03bb(n :register). (0w :bool[32]));        psrs :=          (\u03bb(x :psr).             SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));        memory :=          ((0w :bool[30]) |:           [            enc              (SUB AL T (0w :bool[4]) (0w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])) :                 arm_instruction);            enc (B NE (0w :bool[24]));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (0w :bool[8])));            enc              (MOV AL F (1w :bool[4])                 (Dp_immediate (0w :bool[4]) (1w :bool[8])))            ]) (\u03bb(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;        cp_state := ()|&gt; = ^(f32vx_rhsc)))``, DISCH_TAC THEN ASSUME_TAC (UNDISCH subgoal_ne1) THEN FULL_SIMP_TAC pure_ss [f3f1v_thm] THEN EXISTS_TAC ``a :bool`` THEN EXISTS_TAC ``c :bool`` THEN EXISTS_TAC ``d :bool`` THEN REWRITE_TAC [f32vx]); <\/code><\/pre>\n<p>  \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430, \u043d\u0430 \u043c\u043e\u0439 \u0432\u0437\u0433\u043b\u044f\u0434, \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0442\u0440\u0443\u0434\u043e\u0435\u043c\u043a\u0438\u0435, \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e \u0435\u0441\u043b\u0438 \u0438\u0445 \u043f\u0440\u043e\u0432\u043e\u0434\u0438\u0442\u044c \u0434\u043b\u044f \u0447\u0435\u0433\u043e-\u0442\u043e \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e, \u043d\u043e \u0442\u0435 \u0430\u0441\u043f\u0438\u0440\u0430\u043d\u0442\u044b, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0434\u0435\u043b\u0430\u043b\u0438 \u043c\u043e\u0434\u0435\u043b\u044c, \u043f\u0438\u0448\u0443\u0442 \u0432 \u0441\u0432\u043e\u0438\u0445 \u0441\u0442\u0430\u0442\u044c\u044f\u0445, \u0447\u0442\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u044b\u0445 \u0438\u043c\u0438 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 \u043e\u043d\u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043b\u0438 \u043a\u0430\u043a\u0438\u0435-\u0442\u043e \u043d\u0435\u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u044b\u0435 \u0432\u0435\u0449\u0438. \u0422\u0430\u043a \u0447\u0442\u043e, \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c, \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u044d\u0442\u043e \u0431\u0443\u0434\u0443\u0449\u0435\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0445 \u0434\u043b\u044f \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438.    \t   \t<\/p>\n<div class=\"clear\"><\/div>\n<\/p><\/div>\n<p> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"http:\/\/habrahabr.ru\/post\/156413\/\"> http:\/\/habrahabr.ru\/post\/156413\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<div class=\"content html_format\">   \t\u0412 \u0441\u0432\u043e\u0435\u0439 \u043f\u0440\u043e\u0448\u043b\u043e\u0439 <a href=\"http:\/\/habrahabr.ru\/post\/148709\/\">\u0441\u0442\u0430\u0442\u044c\u0435<\/a> \u044f \u043e\u043f\u0438\u0441\u0430\u043b \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u0438\u043c\u0438\u0442\u0438\u0432\u043d\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043d\u0430 \u0421\u0438. \u041f\u0430\u0440\u0430\u043b\u043b\u0435\u043b\u044c\u043d\u043e \u043f\u0440\u0438\u0432\u0435\u043b \u0441\u043e\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u044f, \u043f\u043e\u0447\u0435\u043c\u0443 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0421\u0438 \u043a\u043e\u0434\u0430 \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u0430 \u0434\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431 \u0441\u0447\u0438\u0442\u0430\u0442\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443 \u0431\u0435\u0437\u043e\u0448\u0438\u0431\u043e\u0447\u043d\u043e\u0439. \u0412 \u043e\u0441\u043d\u043e\u0432\u043d\u043e\u043c \u044d\u0442\u0438 \u0441\u043e\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u0441\u0432\u043e\u0434\u044f\u0442\u0441\u044f \u043a \u043c\u044b\u0441\u043b\u0438, \u0447\u0442\u043e \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043a\u043e\u0434 \u2014 \u044d\u0442\u043e \u0442\u043e\u043b\u044c\u043a\u043e \u0447\u0430\u0441\u0442\u044c \u0438\u0441\u0442\u043e\u0440\u0438\u0438 \u043e \u043f\u043e\u043b\u0443\u0447\u0435\u043d\u0438\u0438 \u0440\u0430\u0431\u043e\u0442\u0430\u044e\u0449\u0435\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b. \u0421\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043f\u0440\u0438\u0431\u043b\u0438\u0436\u0435\u043d\u0438\u0435\u043c \u043a \u0442\u043e\u043c\u0443, \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0431\u0435\u0437\u043e\u0448\u0438\u0431\u043e\u0447\u043d\u0443\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0443, \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u043d\u044b\u0445 \u043a\u043e\u0434\u043e\u0432, \u0438\u0445 \u0443\u0436\u0435 \u043d\u0435 \u043d\u0443\u0436\u043d\u043e \u0431\u0443\u0434\u0435\u0442 \u0442\u0440\u0430\u043d\u0441\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0438 \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u0438\u0441\u043a\u043b\u044e\u0447\u0438\u0442\u0441\u044f \u043e\u0431\u0448\u0438\u0440\u043d\u043e\u0435 \u043f\u043e\u043b\u0435 \u0434\u043b\u044f \u0432\u043e\u0437\u043d\u0438\u043a\u043d\u043e\u0432\u0435\u043d\u0438\u044f \u043e\u0448\u0438\u0431\u043e\u043a. \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u044f \u043e\u043f\u0438\u0448\u0443 \u043f\u0440\u043e\u0446\u0435\u0441\u0441 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u0443\u0436\u0435 \u0434\u043b\u044f \u0430\u0441\u0441\u0435\u043c\u0431\u043b\u0435\u0440\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043d\u0430 \u043f\u043e\u0440\u044f\u0434\u043e\u043a \u043f\u0440\u0438\u043c\u0438\u0442\u0438\u0432\u043d\u0435\u0439, \u0447\u0435\u043c \u0434\u0430\u0436\u0435 \u043f\u0440\u043e\u0441\u0442\u0435\u0439\u0448\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u043d\u0430 \u0421\u0438, \u043e \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0433\u043e\u0432\u043e\u0440\u0438\u043b\u043e\u0441\u044c \u0432 \u043f\u0440\u043e\u0448\u043b\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435.   <\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-156413","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/156413","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=156413"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/156413\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=156413"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=156413"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=156413"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}