Code

Precise bitindex#23

Code

Merged

fschramka merged 56 commits intoateleris:masterateleris/asn1scc:masterfrom epfl-lara:precise-bitindexepfl-lara/asn1scc:precise-bitindexCopy head branch name to clipboardAug 6, 2024

+6,125-2,033

Commits

Commits on Jun 13, 2024

• verified appendNBits and appendNBitsLoops

  

  samuelchassot

  authored and

  mario-bucev

  committed
  6c40aa7

• remove lemma call

  

  samuelchassot

  authored and

  mario-bucev

  committed
  dfcd9fe

• working on the verification of bitstream

  

  samuelchassot

  authored and

  mario-bucev

  committed
  99e4d40

• - proved invertability of appendNLeastSignificantBits with its corresponding read function readNLeastSignificantBits

  Show description for 5700419
  

  samuelchassot

  authored and

  mario-bucev

  committed
  5700419

• verify invertibility appendBitsLSBFirst, with its corresponding lemma

  

  samuelchassot

  authored and

  mario-bucev

  committed
  05e9617

• working on proving appendBitsMSBFirstLoop, before moving to the list of bits specification, in place of the array of UByte

  

  samuelchassot

  authored and

  mario-bucev

  committed
  35a2f90

• proved invertibility of appendBitsMSBFirst but with a List specification (i.e. functions that read the bitstream and returns

  Show description for 0375f5e
  

  samuelchassot

  authored and

  mario-bucev

  committed
  0375f5e

• verification script + stainless conf

  

  samuelchassot

  authored and

  mario-bucev

  committed
  17c39dd

• verified BitStream

  

  samuelchassot

  authored and

  mario-bucev

  committed
  9a95132

Commits on Jun 20, 2024

• Inverse for byte writing functions in bitstream (#5)

  Show description for c6d6ec9
  samuelchassot

  authored
  c6d6ec9

Commits on Jun 21, 2024

• add scripts to verify and run genc

  samuelchassot

  committed
  457645a

Commits on Jul 11, 2024

• Sketching precise size computation

  mario-bucev

  committed
  c6db454

• Rework ProofAst

  mario-bucev

  committed
  106dacb

• Simplify size fns when size is invariant

  mario-bucev

  committed
  4cf40e0

• Add Asn1AcnAst type to SequenceChildProps, use precise size in post-conditions

  mario-bucev

  committed
  ee659d3

• Wrap inlined ACN encode/decode in opaque local functions

  mario-bucev

  committed
  9864425

• pre/postcondition for inner functions

  mario-bucev

  committed
  34dc554

• Size computation for options

  mario-bucev

  committed
  dee9a09

• Add class invariants and fix size computation

  mario-bucev

  committed
  7dd9b4e

• Do not add alignment when computing lower bound size

  mario-bucev

  committed
  0eddf35

• Bind field size computation in preparation for alignment computation

  mario-bucev

  committed
  bf77377

• Size lemmas, proofs to be done

  mario-bucev

  committed
  58c838b

• Proofs for size lemmas

  mario-bucev

  committed
  6f77b32

• Fixing size proof gen

  mario-bucev

  committed
  c3b5054

• Refactor code for sequence proof gen

  mario-bucev

  committed
  f5fc1a9

• Wrapping other inlined code

  mario-bucev

  committed
  f3afa3e

• Precise bitindex for sequences

  mario-bucev

  committed
  c70be08

• Sketching capability of generating auxiliary functions

  mario-bucev

  committed
  db8721f

• Transform while-loops of SequenceOf to outer recursive function

  mario-bucev

  committed
  67a21bc

• Rework a bit the proof gen for sequences

  mario-bucev

  committed
  4ca0777

• Extract optional fields into functions

  mario-bucev

  committed
  3cf2d3c

• Increase stack size

  mario-bucev

  committed
  c9464f0

• Remove unnecessary code and fix tests

  mario-bucev

  committed
  1fb6d98

• Sketching parameterizing ACN dependencies for decoding functions

  mario-bucev

  committed
  3cf07b2

• Parameterization for ACN encoding functions

  mario-bucev

  committed
  e595184

• Fixing some specs

  mario-bucev

  committed
  06bfde9

• Add IsConstraintValid to decode postcondition

  mario-bucev

  committed
  77d3318

• Loop into recursive functions for strings as well

  mario-bucev

  committed
  c9780c0

• Change Scala ATC to construct values instead of mutating them

  mario-bucev

  committed
  dc0156b

• Fix Scala UPER

  mario-bucev

  committed
  7dc38d7

• Sketching conversion to List

  mario-bucev

  committed
  8ff5dfa

• Replace List with Vector

  mario-bucev

  committed
  3541a6a

• Convert strings to use Vector as well

  mario-bucev

  committed
  7461979

• Generate apply methods for Sequence type alias

  mario-bucev

  committed
  145a51b

• Add more proof annotations for SequenceOf encoding functions

  mario-bucev

  committed
  d0bb1cc

• Use 0 as minimum size for size definitions

  mario-bucev

  committed
  13a8935

• Add some lemmas back

  mario-bucev

  committed
  107a6b7

Commits on Jul 12, 2024

• Add pre and postcondition for string types

  mario-bucev

  committed
  faea85e

• Make decodeUnconstrainedNumber return an option

  mario-bucev

  committed
  71d4238

• Validate number length in decodeUnconstrainedWholeNumber

  mario-bucev

  committed
  7be92b0

Commits on Jul 14, 2024

• Fix size offsetting for presence bits

  mario-bucev

  committed
  4d8bf33

Commits on Jul 17, 2024

• Do not emit size assertions for nested sequences

  mario-bucev

  committed
  9bbbbc7

• Merge remote-tracking branch 'maxime/master' into precise-bitindex

  Show description for 32a5d59
  mario-bucev

  committed
  32a5d59

• Fix wrapAcnFuncBody being called when it should not

  mario-bucev

  committed
  b7924dd

Commits on Jul 22, 2024

• Fix string enc/dec for Scala

  mario-bucev

  committed
  423619f

• Update Stainless library

  mario-bucev

  committed
  30990ad