General updates#1

Merged

ArquintL merged 19 commits into

mainfrom

migrate-latest-commits

Sep 21, 2025

Commits on Sep 16, 2025

Adds support for non-linear restrictions e.g. Neq(x,x) ==> F, where arguments of a fact are literals. Non-linear arguments are linearized e.g. the above restriction becomes Neq(x, y) ==> (x == y) =…

swiesner
authored and
ArquintL
committed
Adds support for restriction definitions with pattern matching to Gobra backend (error message for verifast).

swiesner
authored and
ArquintL
committed
Fixes bug: changes restrExists to restrForALl.

swiesner
authored and
ArquintL
committed
Generalize ppFunSym, and ppRule (Tern function encoding and equality encoding) to not just work for type 'Term' but for any given type (changes argument and return type).

swiesner
authored and
ArquintL
committed
Update generated code: Adds enum for integers and variations of enum.

swiesner
authored and
ArquintL
committed
Adds inline formatting for quantified expressions e.g. forall.

swiesner
authored and
ArquintL
committed
Adds 'fst' and 'snd' to reserved words since they are already used in VeriFast's java.lang.javaspec.

swiesner
authored and
ArquintL
committed
Replaces inconsistent use of enum defined in CommonFunctions with the isabelle generated versions.

swiesner
authored and
ArquintL
committed
Generalizes functions printing declarations, equations, AC lemmas, etc. so they can be used with types other than 'Term'(e.g. when we later want to use them with bytes).

swiesner
authored and
ArquintL
committed
Adds Gobra encoding for 'Bytes' (analogous to functions and constants used with 'Term'/'Pub') and 'Gamma' (homomorphism).

swiesner
authored and
ArquintL
committed
Adds VeriFast encoding for functions/constants defined on bytes (analogous to the ones defined on 'Term's). Adds gamma function (Term to bytes) and homomorphism.

swiesner
authored and
ArquintL
committed
Simplify TamiglooConfig by unnecessary hardcoded removing path info from config.

swiesner
authored and
ArquintL
committed
Moves Gobra file path methods to utils.

swiesner
authored and
ArquintL
committed
Simplify TamiglooConfig by removing unnecessary mod_ entries in config.

swiesner
authored and
ArquintL
committed
Resolves majority of warnings due to unused variables, non-exhaustive patterns, redundant imports, shadowing bindings, etc.

swiesner
authored and
ArquintL
committed
updates I/O spec generator to latest syntax changes in Gobra
ArquintL
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

General updates#1

General updates#1
ArquintL merged 19 commits into
mainfrom
migrate-latest-commits

Commits on Sep 16, 2025

Adds support for non-linear restrictions e.g. Neq(x,x) ==> F, where arguments of a fact are literals. Non-linear arguments are linearized e.g. the above restriction becomes Neq(x, y) ==> (x == y) =…

Adds support for restriction definitions with pattern matching to Gobra backend (error message for verifast).

Fixes bug: changes restrExists to restrForALl.

Generalize ppFunSym, and ppRule (Tern function encoding and equality encoding) to not just work for type 'Term' but for any given type (changes argument and return type).

Update generated code: Adds enum for integers and variations of enum.

Adds inline formatting for quantified expressions e.g. forall.

Adds 'fst' and 'snd' to reserved words since they are already used in VeriFast's java.lang.javaspec.

Replaces inconsistent use of enum defined in CommonFunctions with the isabelle generated versions.

Generalizes functions printing declarations, equations, AC lemmas, etc. so they can be used with types other than 'Term'(e.g. when we later want to use them with bytes).

Adds Gobra encoding for 'Bytes' (analogous to functions and constants used with 'Term'/'Pub') and 'Gamma' (homomorphism).

Adds VeriFast encoding for functions/constants defined on bytes (analogous to the ones defined on 'Term's). Adds gamma function (Term to bytes) and homomorphism.

Simplify TamiglooConfig by unnecessary hardcoded removing path info from config.

Moves Gobra file path methods to utils.

Simplify TamiglooConfig by removing unnecessary mod_ entries in config.

Resolves majority of warnings due to unused variables, non-exhaustive patterns, redundant imports, shadowing bindings, etc.

updates I/O spec generator to latest syntax changes in Gobra

Commits on Sep 21, 2025

updates WireGuard oracle to Python3, updates Dockerfile such that it builds again

adds dependabot

fixes scripts for running Tamarin to disables timeouts while checking well-formedness