Carl's questions

Como você verifica se um pedaço alinhado de 16 u32é consecutivo (e crescente)?

Por exemplo: [100, 101, 102, ..., 115]é. E [100, 99, 3 ...]não é.

Estou no AVX512f. Isto é o que tenho até agora:

Algo A:

* predefine DECREASE_U32, a u32x16 of [15,14,13,...0]
* let a = input + DECREASE_32 // wrapping is OK
* compare a to u32x16::splat(first_item(a))
* Return whether all true

Alterativa (Algo B)

* let b = copy of A
* permute the elements of b by one position
* let b = a-b
* Is b all 1's (except for 1st position)

Estou fazendo isso em Rust com a packed_simdcaixa, mas qualquer linguagem/pseudocódigo está bem. (Gostaria que houvesse uma operação SIMD para subtrair itens adjacentes.)

Estou tentando depurar o tempo de verificação variável no Dafny. Tento executar o verifyLogger, mas não obtenho saída.

• Estou no Windows (mas ficaria feliz com uma solução Linux)

• Defino meu caminho para a versão do Dafny instalada pelo complemento VSCode, assim:

  definir caminho=C:\Usuários\carlk.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%caminho%

• Eu corro:

  dafny verify --verification-time-limit:15 --cores:6 --boogie -randomSeedIterations:10 --boogie -verificationLogger:csv repro1.dfy

mas não vejo nenhuma saída CSV.

Eu criei um SortedMap verificado em Dafny. É uma sequência de pares (chave, valor). As chaves são números inteiros distintos e classificados. Não consigo descobrir como mostrar que o comprimento do "KeySet" deve ser igual ao comprimento da sequência.

-- Carl

Erro:

this is the postcondition that could not be proved
  |
7 |   ensures |KeySet(sorted_seq)| == |sorted_seq|

Código simplificado:

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  set i | i in sorted_seq :: i.0
}


method Main()
{
  var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
  print KeySet(s);

}

Estou aberto a qualquer forma de escrever CountLessThan que seja verificável. Aqui está o que eu tenho:

function SetLessThan(numbers: set<int>, threshold: int): set<int>
{
  set i | i in numbers && i < threshold
}
method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |SetLessThan(numbers, threshold)|
{
  count := 0;
  var shrink := numbers;
  var grow := {};
  while |shrink | > 0
    decreases shrink
    invariant shrink + grow == numbers
    invariant count == |SetLessThan(grow, threshold)|
  {
    var i: int :| i in shrink;
    shrink := shrink - {i};
    grow := grow + {i};
    if i < threshold {
      count := count + 1;
    }
  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  // assert c == 3;

}

Este é um pequeno passo para definir um conjunto classificado, depois um mapa classificado e, por fim, um conjunto de intervalos.

Eu gostaria de contar os elementos em um Dafny que são definidos abaixo de um limite, mas não consigo descobrir o 'garantir'.

method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |{i in numbers | i < threshold}|
{
  count := 0;
  var ss := numbers;
  while ss != {}
    decreases |ss|
  {
    var i: int :| i in ss;
    ss := ss - {i};
    if i < threshold {
      count := count + 1;
    }

  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  // assert c == 3;

}

O erro é:this operator chain cannot continue with an ascending operator