1. Си / Говнокод #24807

    +1

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 26
    27. 27
    28. 28
    29. 29
    30. 30
    31. 31
    32. 32
    33. 33
    34. 34
    35. 35
    36. 36
    37. 37
    38. 38
    39. 39
    40. 40
    41. 41
    42. 42
    43. 43
    44. 44
    45. 45
    46. 46
    47. 47
    48. 48
    49. 49
    50. 50
    51. 51
    52. 52
    53. 53
    54. 54
    55. 55
    56. 56
    57. 57
    58. 58
    59. 59
    #include <stdio.h>
#include <inttypes.h>

static const uint32_t pow2[511] ={
0, 1, 4, 9, 16, 25, 36, 49, 64, 81, 100, 121, 144, 169, 196, 225, 256,
289, 324, 361, 400, 441, 484, 529, 576, 625, 676, 729, 784, 841, 900, 961, 1024, 1089, 1156,
1225, 1296, 1369, 1444, 1521, 1600, 1681, 1764, 1849, 1936, 2025, 2116, 2209, 2304, 2401,
2500, 2601, 2704, 2809, 2916, 3025, 3136, 3249, 3364, 3481, 3600, 3721, 3844, 3969, 4096,
4225, 4356, 4489, 4624, 4761, 4900, 5041, 5184, 5329, 5476, 5625, 5776, 5929, 6084, 6241,
6400, 6561, 6724, 6889, 7056, 7225, 7396, 7569, 7744, 7921, 8100, 8281, 8464, 8649, 8836,
9025, 9216, 9409, 9604, 9801, 10000, 10201, 10404, 10609, 10816, 11025, 11236, 11449, 11664,
11881, 12100, 12321, 12544, 12769, 12996, 13225, 13456, 13689, 13924, 14161, 14400, 14641,
14884, 15129, 15376, 15625, 15876, 16129, 16384, 16641, 16900, 17161, 17424, 17689, 17956,
18225, 18496, 18769, 19044, 19321, 19600, 19881, 20164, 20449, 20736, 21025, 21316, 21609,
21904, 22201, 22500, 22801, 23104, 23409, 23716, 24025, 24336, 24649, 24964, 25281, 25600,
25921, 26244, 26569, 26896, 27225, 27556, 27889, 28224, 28561, 28900, 29241, 29584, 29929,
30276, 30625, 30976, 31329, 31684, 32041, 32400, 32761, 33124, 33489, 33856, 34225, 34596,
34969, 35344, 35721, 36100, 36481, 36864, 37249, 37636, 38025, 38416, 38809, 39204, 39601,
40000, 40401, 40804, 41209, 41616, 42025, 42436, 42849, 43264, 43681, 44100, 44521, 44944,
45369, 45796, 46225, 46656, 47089, 47524, 47961, 48400, 48841, 49284, 49729, 50176, 50625,
51076, 51529, 51984, 52441, 52900, 53361, 53824, 54289, 54756, 55225, 55696, 56169, 56644,
57121, 57600, 58081, 58564, 59049, 59536, 60025, 60516, 61009, 61504, 62001, 62500, 63001,
63504, 64009, 64516, 65025, 65536, 66049, 66564, 67081, 67600, 68121, 68644, 69169, 69696,
70225, 70756, 71289, 71824, 72361, 72900, 73441, 73984, 74529, 75076, 75625, 76176, 76729,
77284, 77841, 78400, 78961, 79524, 80089, 80656, 81225, 81796, 82369, 82944, 83521, 84100,
84681, 85264, 85849, 86436, 87025, 87616, 88209, 88804, 89401, 90000, 90601, 91204, 91809,
92416, 93025, 93636, 94249, 94864, 95481, 96100, 96721, 97344, 97969, 98596, 99225, 99856,
100489, 101124, 101761, 102400, 103041, 103684, 104329, 104976, 105625, 106276, 106929,
107584, 108241, 108900, 109561, 110224, 110889, 111556, 112225, 112896, 113569, 114244,
114921, 115600, 116281, 116964, 117649, 118336, 119025, 119716, 120409, 121104, 121801,
122500, 123201, 123904, 124609, 125316, 126025, 126736, 127449, 128164, 128881, 129600,
130321, 131044, 131769, 132496, 133225, 133956, 134689, 135424, 136161, 136900, 137641,
138384, 139129, 139876, 140625, 141376, 142129, 142884, 143641, 144400, 145161, 145924,
146689, 147456, 148225, 148996, 149769, 150544, 151321, 152100, 152881, 153664, 154449,
155236, 156025, 156816, 157609, 158404, 159201, 160000, 160801, 161604, 162409, 163216,
164025, 164836, 165649, 166464, 167281, 168100, 168921, 169744, 170569, 171396, 172225,
173056, 173889, 174724, 175561, 176400, 177241, 178084, 178929, 179776, 180625, 181476,
182329, 183184, 184041, 184900, 185761, 186624, 187489, 188356, 189225, 190096, 190969,
191844, 192721, 193600, 194481, 195364, 196249, 197136, 198025, 198916, 199809, 200704,
201601, 202500, 203401, 204304, 205209, 206116, 207025, 207936, 208849, 209764, 210681,
211600, 212521, 213444, 214369, 215296, 216225, 217156, 218089, 219024, 219961, 220900,
221841, 222784, 223729, 224676, 225625, 226576, 227529, 228484, 229441, 230400, 231361,
232324, 233289, 234256, 235225, 236196, 237169, 238144, 239121, 240100, 241081, 242064,
243049, 244036, 245025, 246016, 247009, 248004, 249001, 250000, 251001, 252004, 253009,
254016, 255025, 256036, 257049, 258064, 259081, 260100 };

#define SQR(x) pow2[x]

uint16_t mul8b(uint8_t a, uint8_t b)
{
  return (SQR((uint16_t)a+(uint16_t)b) - (SQR(a) + SQR(b))) >> 1;
}

int main(void)
{
  uint8_t a = 255, b = 255;
  printf("%" PRIu8 " * " "%"PRIu8 " = "  "%"PRIu16, a, b, mul8b(a, b));
  return 0;
}

    Мегаинновационный алгоритм умножения двух чисел на основе таблицы поиска с предвычисленными квадратами.
    По формуле ab = ((a+b)^2 - (a^2+b^2))/2
    Можно упихать в какой-нибудь дохлый контроллер без инструкций умножения

    Запостил: j123123, 24 Сентября 2018

    Комментарии (86) RSS

    • ava OBEH 24.09.2018 22:56 # −2

      Какое небо голубое...
      Ответить

    • ava Elvenfighter 24.09.2018 22:59 # 0

      > #include <inttypes.h>

      Думаю ималось ввиду 
      #include <stdint.h>


      UPD А нет, вижу printf. Сорри
      Ответить

    • ava guest8 24.09.2018 23:16 # −999

      показать все, что скрытоvanished
      Ответить

    • ava guest8 25.09.2018 00:39 # −999

      показать все, что скрытоvanished
      Ответить

      • ava guest8 25.09.2018 01:39 # −999

        показать все, что скрытоvanished
        Ответить

      • ava j123123 25.09.2018 21:28 # +2

        В таблице пифагора избыточности много, а тут-то всего-навсего надо хранить значения квадратов
        Ответить

        • ava guest8 26.09.2018 04:37 # −999

          показать все, что скрытоvanished
          Ответить

          • ava guest8 26.09.2018 04:39 # −999

            показать все, что скрытоvanished
            Ответить

          • ava bormand 26.09.2018 07:01 # +2

            > делить
            На степени двойки же, это легко. Сдвигаешь на бит вправо и готово.
            Ответить

            • ava bormand 26.09.2018 07:04 # 0

              З.Ы. Ну и можно сделать таблицу полуквадратов. Тогда делить не надо.
              Ответить

          • ava j123123 26.09.2018 08:16 # +1

            Размер таблицы поиска кстати можно сильно сократить, воспользовавшись формулой
            x^2=(x-1)^2+2*x-1 или
            x^2=(x+1)^2-2*x-1
            т.е. хранить можно каждый четвертый квадрат, а всё что между - считать по такой вот формуле относительно них
            Ответить

            • ava bormand 26.09.2018 08:56 # +1

              > каждый пятый
              Не заебешься делить на 5? Каждый четвертый наверное лучше, хоть и не так компактно.

              З.Ы. А, лол, ты уже исправил.
              Ответить

              • ava j123123 26.09.2018 11:50 # +2

                Можно каждый восьмой. А потом еще нам каждый раз пересчитывать формулу не надо.
                Вот например у нас есть знание, что 8^2 = 64, а нам надо 11^2.
                Тогда находим 2*x-1 для x = 9 -> 17. Формула 2*x-1 для x = 10 -> 19 (ровно на 2 больше)
                т.е. 11^2 = 8^2 + 17+19+21
                Ответить

                • ava j123123 26.09.2018 12:01 # 0

                  11^2 = 8^2 + 17*3 + предвычисленная_питушня_https://oeis.org/A002378
                  >>> 0
0
>>> 2
2
>>> 2+4
6
>>> 2+4+6
12
>>> 2+4+6+8
20
>>> 2+4+6+8+10
30
                  Ответить

                • ava gost 26.09.2018 12:44 # 0

                  Да, в принципе, можно и вообще никаких элементов не хранить:
                  uint64_t sqr(uint64_t x)
{
    uint64_t sum = 0;
    while (x > 0) {
        sum += --x * 2 + 1;
    }
    return sum;
}
                  Ответить

                  • ava gost 26.09.2018 15:13 # 0

                    Забавно: gcc не распознал здесь квадрата и честно складывает-умножает. А вот такое:
                    uint64_t sqr2(uint64_t x)
{
    uint64_t sum = 0;
    for (uint64_t i = 0; i < x; i++) {
        sum += x;
    }
    return sum;
}

                    уже вырезается до «imul rdi, rdi».
                    Ответить

                    • ava gost 26.09.2018 15:18 # 0

                      MSVC на примере с «sum += x;» творит какую-то хуйню:
                      unsigned long sqr2(unsigned long) PROC                                  ; sqr2, COMDAT
        test    ecx, ecx
        je      SHORT $LN10@sqr2
        imul    ecx, ecx
        mov     eax, ecx
        ret     0
$LN10@sqr2:
        xor     eax, eax
        ret     0
unsigned long sqr2(unsigned long) ENDP
                      Ответить

                  • ava gost 26.09.2018 15:33 # 0

                    Некий «Zapcc 190308» очень интересно откомпилировал sqr(x):
                    sqr(unsigned long):    # @sqr(unsigned long)
        test    rdi, rdi
        je      .LBB0_1
        lea     rax, [rdi - 1]
        lea     rcx, [rdi + rdi - 3]
        imul    rcx, rax
        lea     rdx, [rdi - 2]
        imul    rdx, rax
        and     rdx, -2
        lea     rax, [rcx + 2*rdi - 1]
        sub     rax, rdx
        ret
.LBB0_1:
        xor     eax, eax
        ret


                    В переводе на «PHP»:
                    lea     rax, [rdi - 1]
    rax = x - 1
lea     rcx, [rdi + rdi - 3]
    rcx = 2*x - 3
imul    rcx, rax
    rcx = (x - 1) * (2*x - 3) = 2*x^2 - 5*x + 3
lea     rdx, [rdi - 2]
    rdx = x - 2
imul    rdx, rax
    rdx = (x - 2) * (x - 1) = x^2 - 3*x + 2
and     rdx, -2
    rdx = rdx & 0x1111..1110
    многочлен в rdx всегда чётный, поэтому эта операция ничего не делает
lea     rax, [rcx + 2*rdi - 1]
    rax = 2*x^2 - 5*x + 3 + 2*x - 1 = 2*x^2 - 3*x + 2
sub     rax, rdx
    rax = 2*x^2 - 5*x + 3 + 2*x - 1 = 2*x^2 - 3*x + 2 - x^2 + 3*x - 2 = x^2
                    Ответить

                    • ava roman-kashitsyn 26.09.2018 15:36 # +1

                      если ты так любишь извращения, перевёл тебе на «Common Lisp»
                      (defun sqr2 (n) (declare (optimize (speed 3) (safety 0)) (type fixnum n)) (loop for x from 1 to n summing n)

;; SBCL
(disassemble #'sqr2)

; disassembly for SQR2
; Size: 85 bytes. Origin: #x1001BF005A
; 5A:       BB01000000       MOV EBX, 1                       ; no-arg-parsing entry point
; 5F:       31C9             XOR ECX, ECX
; 61:       EB38             JMP L1
; 63:       660F1F840000000000 NOP
; 6C:       0F1F4000         NOP
; 70: L0:   48895DF8         MOV [RBP-8], RBX
; 74:       488975F0         MOV [RBP-16], RSI
; 78:       488BFE           MOV RDI, RSI
; 7B:       488BD1           MOV RDX, RCX
; 7E:       41BBE004B021     MOV R11D, #x21B004E0             ; GENERIC-+
; 84:       41FFD3           CALL R11
; 87:       488BCA           MOV RCX, RDX
; 8A:       488B75F0         MOV RSI, [RBP-16]
; 8E:       488B5DF8         MOV RBX, [RBP-8]
; 92:       488BC3           MOV RAX, RBX
; 95:       48FFC0           INC RAX
; 98:       488BD8           MOV RBX, RAX
; 9B: L1:   488BD6           MOV RDX, RSI
; 9E:       48D1FA           SAR RDX, 1
; A1:       4839D3           CMP RBX, RDX
; A4:       7ECA             JLE L0
; A6:       488BD1           MOV RDX, RCX
; A9:       488BE5           MOV RSP, RBP
; AC:       F8               CLC
; AD:       5D               POP RBP
; AE:       C3               RET
NIL
                      Никаких умножений
                      Ответить

                      • ava j123123 26.09.2018 16:15 # 0

                        Переведи лучше на Хаскель
                        Ответить

                        • ava roman-kashitsyn 26.09.2018 17:04 # +1

                          Я уже перевёл, но GHC не осилил, даже с -O2, хвастаться особо нечем:
                          sqr2 :: Int -> Int
sqr2 n = sum $ replicate n n
main = print $ sqr2 5
                          Он догадался заинлайнить 5, но цикл никуда не делся
                          Rec {
-- RHS size: {terms: 16, types: 3, coercions: 0}
Main.$wxs [InlPrag=[0], Occ=LoopBreaker]
  :: GHC.Prim.Int# -> GHC.Prim.Int# -> GHC.Prim.Int#
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType <S,1*U><S,U>]
Main.$wxs =
  \ (ww_s4Md :: GHC.Prim.Int#) (ww1_s4Mh :: GHC.Prim.Int#) ->
    case ww_s4Md of ds1_a2ke {
      __DEFAULT ->
        Main.$wxs (GHC.Prim.-# ds1_a2ke 1#) (GHC.Prim.+# ww1_s4Mh 5#);
      1# -> GHC.Prim.+# ww1_s4Mh 5#
    }
end Rec }
                          Можно руками правила оптимизации подогнать, но это не спортивно.
                          {-# RULES "stupid/mul" forall n. sum (rep n n) = n * n ; #-}

rep = replicate
{-# NOINLINE[0] rep #-}

sqr2 :: Int -> Int
sqr2 n = sum (rep n n)
 -- посчитает 25 во время компиляции
main = print $ sqr2 5
                          Ответить

                          • ava j123123 26.09.2018 17:52 # 0

                            Попробуй с -fllvm
                            и асмовыхлоп покаж
                            Ответить

                            • ava roman-kashitsyn 26.09.2018 18:47 # +1

                              > -fllvm

                              Это влияет только на кодогенерацию, Core от этого не изменится. Как всегда, в дебиане ghc не совместим с версией llvm из репы, и у меня недостаточно мотивации, чтобы с этим бороться. Смотри на выхлоп дефолтного кодогенератора (надеюсь, я правильно нашёл кусок, GHC не оставляет толком аннотаций):
                              ==================== Asm code ====================
.section .text
.align 8
.align 8
        .quad   8589934604
        .quad   0
        .quad   15
.globl Main.$wxs_info
.type Main.$wxs_info, @object
Main.$wxs_info:
_c4NC:
_c4Nv:
        cmpq $1,%r14
        jne _c4NA
_c4NB:
        leaq 5(%rsi),%rbx
        jmp *(%rbp)
_c4NA:
        addq $5,%rsi
        decq %r14
        jmp _c4Nv
        .size Main.$wxs_info, .-Main.$wxs_info
                              Ответить

                              • ava bormand 26.09.2018 19:08 # +1

                                Пиздец у него асм, конечно. Куча каких-то обрывков с косвенными переходами... Походу, хаскелю даже обфускатор нинужен.
                                Ответить

                                • ava roman-kashitsyn 26.09.2018 19:59 # +1

                                  у окамла попонятней, конечно, но worker/wrapper кучу какого-то бойлерплейта генерит
                                  let sqr1 n =
  let acc = ref 0
  in for i = 1 to n do acc := !acc + n done;
     !acc

let sqr2 n =
  let rec go acc i = if i == 0 then acc else go (acc+n) (i-1)
  in go 0 n

let _ =
  Printf.printf "%d\n" (sqr1 10);
  Printf.printf "%d\n" (sqr2 10)
                                  ocamlopt -S <name>.ml
                                  camlSqr__go_1014:
	.cfi_startproc
.L101:
	cmpq	$1, %rbx
	jne	.L100
	ret
	.align	4
.L100:
	addq	$-2, %rbx
	movq	24(%rdi), %rsi
	leaq	-1(%rax, %rsi), %rax
	jmp	.L101
	.cfi_endproc
	.type	camlSqr__go_1014,@function
	.size	camlSqr__go_1014,.-camlSqr__go_1014
	.text
	.align	16
	.globl	camlSqr__sqr1_1008
camlSqr__sqr1_1008:
	.cfi_startproc
.L104:
	movq	%rax, %rbx
	movq	$1, %rax
	movq	$3, %rdi
	cmpq	%rbx, %rdi
	jg	.L102
.L103:
	leaq	-1(%rax, %rbx), %rax
	movq	%rdi, %rsi
	addq	$2, %rdi
	cmpq	%rbx, %rsi
	jne	.L103
.L102:
	ret
	.cfi_endproc
	.type	camlSqr__sqr1_1008,@function
	.size	camlSqr__sqr1_1008,.-camlSqr__sqr1_1008
	.text
	.align	16
	.globl	camlSqr__sqr2_1012
camlSqr__sqr2_1012:
	.cfi_startproc
	subq	$8, %rsp
	.cfi_adjust_cfa_offset	8
.L105:
	movq	%rax, %rbx
.L106:	subq	$40, %r15
	movq	caml_young_limit@GOTPCREL(%rip), %rax
	cmpq	(%rax), %r15
	jb	.L107
	leaq	8(%r15), %rdi
	movq	$4343, -8(%rdi)
	movq	caml_curry2@GOTPCREL(%rip), %rax
	movq	%rax, (%rdi)
	movq	$5, 8(%rdi)
	movq	camlSqr__go_1014@GOTPCREL(%rip), %rax
	movq	%rax, 16(%rdi)
	movq	%rbx, 24(%rdi)
	movq	$1, %rax
	addq	$8, %rsp
	.cfi_adjust_cfa_offset	-8
	jmp	camlSqr__go_1014@PLT
	.cfi_adjust_cfa_offset	8
.L107:	call	caml_call_gc@PLT
.L108:	jmp	.L106
	.cfi_endproc
	.type	camlSqr__sqr2_1012,@function
	.size	camlSqr__sqr2_1012,.-camlSqr__sqr2_1012
	.text
	.align	16
	.globl	camlSqr__entry
                                  Ответить

                              • ava j123123 27.09.2018 04:22 # 0

                                >Как всегда, в дебиане ghc не совместим с версией llvm из репы, и у меня недостаточно мотивации, чтобы с этим бороться

                                Поэтому я за Gentoo
                                Ответить

                                • ava bormand 27.09.2018 07:39 # +1

                                  Думаешь если на сборку одной проги мотивации не хватает, то на сборку всего дистриба внезапно хватит?
                                  Ответить

                                  • ava j123123 27.09.2018 08:04 # 0

                                    На генте она б уже была собрана как надо, а не как в некродебиане
                                    https://packages.gentoo.org/packages/dev-haskell/binary
                                    Ответить

                      • ava gost 26.09.2018 17:43 # 0

                        Так это sqr2(). «Zapcc» соптимизировал sqr() с циклом «while (x > 0) { sum += (--x << 1) + 1; }», только очень странно.
                        Ответить

    • ava govnokod3r 25.09.2018 23:02 # 0

      >Можно упихать в какой-нибудь дохлый контроллер без инструкций умножения

      2К таблица + 32 битная арифметика, 8 битные говноконтроллеры будут страдать. Умножение сдвигами, по времени наверное не намного медленнее.
      Ответить

      • ava bormand 26.09.2018 07:16 # 0

        > 32-битная
        24. Да и сложение и сдвиг на 1 бит на 8-битках нормально пилятся.

        А вот размер таблицы - да, очень большой. Даже если до 1.5К ужать.
        Ответить

      • ava j123123 26.09.2018 12:21 # 0

        > 2К таблица + 32 битная арифметика, 8 битные говноконтроллеры будут страдать.

        На ассемблере можно нахерачить это легко делается, а таблицу урезать методом, описанным выше.
        Ответить

    • ava Morgoth 26.09.2018 07:51 # 0

      > дохлый контроллер без инструкций умножения
      Упихай в 4004.
      Ответить

      • ava j123123 26.09.2018 14:11 # 0

        А внешнюю флеш-память можно прикрутить?
        Ответить

        • ava Morgoth 27.09.2018 08:35 # 0

          Я нехнаю, я знаю только, что он был убогий 4 битный проц для цанцуляторов.
          Ответить

    • ava j123123 11.01.2022 14:02 # 0

      https://stackoverflow.com/questions/29935050/tinyavr-best-known-multiplication-routines-for-8-bit-and-16-bit-factors/31074276
      ;**********************************************************
;*
;* "mpy8T" - 8x8->16 Bit Unsigned Multiplication
;*                                using table lookup
;* (mpy8u: 34 words/cycles (avr200b.asm))
;* Multiplies two 8-bit register values a and b.
;* The result is placed in p1:p0.
;*  
;* Number of words  : 17 + 512(table)=553 + return
;* Number of cycles : 25 + return (table coming preset ...)
;* Low  registers used  : None
;* High registers used  : 5+2 (a, b, p1:p0, sq;
;*                             + Z(r31:r30))    
;*
;*********************************************************
mpy8T:
; p = a * b = Squares[a+b] - Squares[a-b]
    ldi     ZH, 2       ; 1 0   0   squares table / 2
    mov     ZL, a       ; 1 1
    add     ZL, b       ; 1 2       a+b
    rol     ZH          ; 1 3       9 bit offset
    lpm     p0, Z       ; 3 4       a+bl            1
    sbr     ZH, 1       ; 1 7
    lpm     p1, Z       ; 1 8   11  a+bh            2*

    ldi     ZH, 4       ; 1 0   11  squares table

    mov     ZL, a       ; 1 0   12
    sub     ZL, b       ; 1 1       a-b
    brcc    pos         ; 1 2
    neg     ZL          ; 1 3
pos:
    lpm     sq, Z       ; 3 4       a-bl            3
    sub     p0, sq      ; 1 7
    sbr     ZH, 1       ; 1 8       (ldi ZH, 6)
    lpm     sq, Z       ; 3 9       a-bh            4*
    sbc     p1, sq      ; 1 12  13

    ret                 ; 3 25
      Ответить

      • ava j123123 11.01.2022 14:20 # 0

        Вообще, младшие биты квадратов чисел можно относительно легко зожать
        https://wandbox.org/permlink/ubGAJWPdWnfZf76M
                |
#               |
  #             |
#  #            |
    #           |
#  ##           |
  #  #          |
#   ##          |
      #         |
#   # #         |
  #  ##         |
#  ####         |
    #  #        |
#  # # #        |
  #   ##        |
#    ###        |
        #       |
#    #  #       |
  #   # #       |
#  # ## #       |
    #  ##       |
#  ### ##       |
  #  ####       |


        Предлагаю ма-те-ма-тикам говнокода ма-те-ма-тически доказать (на Coq), что любой битик в ряде квадратов чисел будет периодическим
        Ответить

        • ava bormand 11.01.2022 18:12 # 0

          > будет периодическим

          А куда ему деваться? Бит N в произведении зависит только от битов 0..N. Очевидно, что после их переполнения всё будет повторяться.
          Ответить

          • ava j123123 11.01.2022 18:17 # 0

            Не, ну это-то понятно, а на Coq доказать сможешь?
            Ответить

            • ava bormand 11.01.2022 18:26 # 0

              Не, я даже теорему не могу сформулировать...
              forall bit_pos : nat,
  exists n : nat,
    forall a : nat, take_bit bit_pos ((a + n) * (a + n)) = take_bit bit_pos a
              Как-то так что ли это условие записывается?
              Ответить

              • ava j123123 11.01.2022 18:35 # 0

                ну допустим есть функция f(x) = x*x
                Надо доказать, что для любых x : nat, N : nat всегда есть такой a : nat при котором всегда выполняется условие (f(x) >> N) & 1 == (f(x+a) >> N) & 1
                Ответить

                • ava bormand 11.01.2022 18:39 # 0

                  А ну да, у меня в конце косяк, надо a * a вместо a (take_bit x y обозначает (y >> x) & 1).
                  Ответить

          • ava Soul_re@ver 11.01.2022 18:17 # 0

            > А куда ему деваться?
            Это такой солвер в coq есть?
            Ответить

            • ava j123123 11.01.2022 18:21 # 0

              Есть еще солвер "в самом деле, легко заметить, что":
              https://i.imgur.com/kKUCvdh.png

              Источник: http://math.sfu-kras.ru/sites/default/files/lectures.pdf
              Ответить

              • ava CHayT 11.01.2022 19:21 # 0

                sauto.
                Ответить

              • ava j123123 19.01.2022 01:55 # 0

                Самый мощный солвер у Ферма был, он им доказал свою Великую теорему

                > Наоборот, невозможно разложить куб на два куба, биквадрат на два биквадрата и вообще никакую степень, большую квадрата, на две степени с тем же показателем. Я нашёл этому поистине чудесное доказательство, но поля книги слишком узки для него.
                Ответить

                • ava bormand 19.01.2022 19:01 # +1

                  Поля его книги были разработаны настолько, что могли вместить поистине чудесное доказательство.
                  Ответить

                • ava 3.14159265 19.01.2022 21:13 # 0

                  > Самый мощный солвер у Ферма был

                  Сишный компилятор тоже ничего.

                  https://govnokod.ru/27645#comment668746

                  За доли секунды опровергает теорему в конечном поле.
                  Ответить

                  • ava HoBorogHuu_nemyx 19.01.2022 21:22 # 0

                    Как можно пользоваться компилятором, оптимизатор которого основан на гипотезах об UB, причём по стандарту?

                    В каких ещё ЯП принято выкидывать код по аналогичным алгоритмам?
                    Ответить

                    • ava 3.14159265 19.01.2022 21:23 # 0

                      Если почитать тот тред дальше, там видно что Сишка всё делает правильно.

                      Я даже указал валидность найденного контр-примера.
                      4³ + 5³ =  1360988357³

64 + 125 = 189
                      Ответить

    Добавить комментарий