Fr_bnot.ini

rdi := nondet as dst            ## initialize the first argument
rsi := nondet as src            ## initialize the second argument
#rdx := nondet as temp
assume dst & 0b111 = 0          ## alignment constraint
assume src & 0b111 = 0          ## alignment constraint

assume 0x3000 <= dst <= 0x4000  ## arbitrary range  
assume 0x5000 <= src <= 0x6000  ## arbitrary range  

starting from <Fr_bnot> with
    assume 0x7ffff000000 <= rsp <= 0x7ffff800000 
    #assume 0 <=u rdx <=u 0xffffffffffffffff
    #assume 0 <= rdx <= 0x0000000000000100

    #assume @[src, 40] = 0x0000000000000000000000000000000000000000000000000000000000001000800000008fffffff


    #assume @[dst, 40] = 0x07359fa88c59c9e89f6e5c105a695dd60d0e939ee8c1e556e4a771fc5ab5b8ba0000000001000000
    #assume @[src+8, 32] = 0x0000000000000000000000000000000000000000000000000000000000000000
    #assume @[dst+8, 32] = 0x0000000000000000000000000000000000000000000000000000000000000000
    @[rsp, 8] := <Fr_bnot:last>
    q[0, 32] := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
    @[0x7ffff8aaaa1, 8] := <Fr_toLongNormal>
    @[0x7ffffbbbbb1, 8] := <Fr_toNormal>


end
replace <Fr_toLongNormal> by

    if @[src, 40]{63} = 0 then
        if (@[src, 4]{31}) = 0 then
            @[src + 8, 4] := @[src, 4]
            @[src + 12, 4] := 0
            @[src + 16, 8] := 0
            @[src + 24, 8] := 0
            @[src + 32, 8] := 0
        else
            @[src + 8, 32] := sext256 @[src, 4] + q[0, 32]
        end
    end
    @[src, 8] := 0x8000000000000000
    return
end
replace <Fr_toNormal> by
    print @[src, 40]
    if @[src, 40]{63} = 1 && @[src, 40]{62} = 1 then
        Rr[0, 32]:= 0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e
        reverse[0,64] := uext512 @[src+8, 32] * uext512 Rr[0, 32] % uext512 q[0, 32]
        @[src + 8, 32] := reverse[0,32]
    end

    @[src, 8] := 0x8000000000000000
    return
end
replace <Fr_bnot:last> by
  eq<1> := true
  eq := eq && @[dst+4, 4] = 0x80000000
      print @[src, 40]
    print ~@[src+8, 32]
    print ~@[src+8, 32] - q[0,32]

    print @[dst+8, 32]
    if ~@[src+8, 32] >= q[0, 32] then
        before[0, 32] := ~@[src+8, 32]
        mask[0, 8] := 0x3fffffffffffffff
        before[24, 8] := mask[0, 8] & before[24, 8]

        after[0, 32] := ~@[src+8, 32] - q[0, 32]
        after[24, 8] := mask[0, 8] & after[24, 8]
        if before[0,32] >= q[0, 32] then
            eq := eq && after[0,32] = @[dst+8, 32]
        else
            eq := eq && before[0,32] = @[dst+8, 32]
        end       
    end
    if ~@[src+8, 32] < q[0, 32] then
        eq := eq && ~@[src+8, 32] = @[dst+8, 32]
    end
  if eq = false then
    print @[src, 40]
    print ~@[src+8, 32]
    print ~@[src+8, 32] - q[0,32]
    print @[dst+8, 32]
  end
  assert eq
  halt

end

explore all