Code

Sequence invertibility#27

Code

Merged

mario-bucev merged 37 commits intoateleris:masterateleris/asn1scc:masterfrom epfl-lara:sequence-invertibilityepfl-lara/asn1scc:sequence-invertibilityCopy head branch name to clipboardSep 9, 2024

+3,504-1,106

Commits

Commits on Aug 4, 2024

• ICD improvements

  usr3-1415

  committed
  e3fa3d7

Commits on Aug 28, 2024

• rename checkByteArrayBitContent to byteArrayBitContentSame

  

  samuelchassot

  authored and

  mario-bucev

  committed
  426cec5

• rename 2 functions of bistream

  

  samuelchassot

  authored and

  mario-bucev

  committed
  d0b904e

• renaming

  

  samuelchassot

  authored and

  mario-bucev

  committed
  cea317b

• with lemma

  

  samuelchassot

  authored and

  mario-bucev

  committed
  b6b234b

• new annotations for proof to pass

  

  samuelchassot

  authored and

  mario-bucev

  committed
  f344672

• ACN lemmas uncommented + update to prove safety again

  

  samuelchassot

  authored and

  mario-bucev

  committed
  6f5fcaa

• prove inverse of encodeUnsignedInteger

  

  samuelchassot

  authored and

  mario-bucev

  committed
  4ff6994

• proved enc_Int_PositiveInteger_ConstSize

  

  samuelchassot

  authored and

  mario-bucev

  committed
  48b4e73

• prove some invertibility in Codec ACN

  

  samuelchassot

  authored and

  mario-bucev

  committed
  9db4238

Commits on Aug 31, 2024

• Update IcdPdus handling and validation

  Show description for 42f4480
  usr3-1415

  committed
  42f4480

• ICD, null types now show the bit or octet pattern

  usr3-1415

  committed
  2e457b0

Commits on Sep 1, 2024

• ICD improvements. Links to ACN definitions

  usr3-1415

  committed
  8a3db57

Commits on Sep 5, 2024

• Update Makefile in test case

  Show description for e3fed24
  maxime-esa

  authored
  e3fed24

• Update Makefile of example test case

  maxime-esa

  authored
  792d1f1

• Merge remote-tracking branch 'ateleris/master'

  samuelchassot

  committed
  203b54f

Commits on Sep 6, 2024

• Prove invertibility of more functions in ACN (#7)

  Show description for d9b60a8
  samuelchassot

  authored
  d9b60a8

Commits on Sep 7, 2024

• Add ACN dependencies to encoding function as well in preparation for inversion property

  mario-bucev

  committed
  bd28e3a

• Add invertibility property in postcondition

  mario-bucev

  committed
  817970b

• Generate prefix lemmas (without proof) for sequences

  mario-bucev

  committed
  2709d47

• Sketching parts of proof for Sequence prefix lemma

  mario-bucev

  committed
  f58740d

• More on prefix lemma proofs

  mario-bucev

  committed
  01411c4

• Add an option to generate invertibility conditions and lemmas

  mario-bucev

  committed
  f16c5d9

• Prefix lemma subproofs

  mario-bucev

  committed
  3255f5b

• Proofs for Sequence prefix lemma

  mario-bucev

  committed
  b8e93d5

• Expand prefix lemma proofs and add support for presence bits

  mario-bucev

  committed
  96f7fea

• Sketching Sequence invertibility proof gen

  mario-bucev

  committed
  bd2d738

• Add prefix lemma proof for optional

  mario-bucev

  committed
  dfb61de

• prefix lemma proof: add intermediate inner function to prove decoding success

  mario-bucev

  committed
  dad93c3

• prefix lemma: bind size computation in specs instead of duplicating it in body and postcond

  mario-bucev

  committed
  5ed043c

• Add proof for Choice prefix lemma

  mario-bucev

  committed
  08700c2

• prefix lemma: add further assertions to help prove decoding success

  mario-bucev

  committed
  61dba86

• Fix resetAtEqLemma not being applied to the correct codecs

  mario-bucev

  committed
  065edef

• Forward 'deps' to fetch ACN dependencies

  mario-bucev

  committed
  27cacc3

• Do not generate lemmas for encodings other than ACN, dedup dependencies

  mario-bucev

  committed
  fcebb1d

Commits on Sep 8, 2024

• Fix reference to prefix lemma for 'PositiveInteger_ConstSize'

  mario-bucev

  committed
  af4ddef

• Merge remote-tracking branch 'origin/master' into sequence-invertibility

  Show description for 5405d7f
  mario-bucev

  committed
  5405d7f