jasmin-lang/jasmin issues and pull requests

#1053 - Fix failing smt in proof of JWord.bits_divmod

Pull Request - State: open - Opened by cassiersg 5 days ago - 2 comments

#1052 - Use elpi.derive instead of "Scheme Equality"

Pull Request - State: open - Opened by eponier 6 days ago - 1 comment

#1051 - CHANGELOG: improve formatting

Pull Request - State: open - Opened by eponier 6 days ago

#1050 - Minor fixes for recent Coq / math-comp

Pull Request - State: closed - Opened by vbgl 7 days ago

#1049 - Broken in Coq CI

Issue - State: closed - Opened by SkySkimmer 7 days ago - 4 comments

#1048 - Pretyping: remove dead code

Pull Request - State: closed - Opened by vbgl 8 days ago
Labels: ocaml

#1047 - ToEC: deprecate mode CTG

Pull Request - State: closed - Opened by vbgl 13 days ago

#1046 - Target EasyCrypt release 2025.02

Pull Request - State: closed - Opened by vbgl 13 days ago - 3 comments

#1045 - Gimli proof: fix for latest EasyCrypt

Pull Request - State: closed - Opened by vbgl 14 days ago - 2 comments
Labels: EasyCrypt

#1044 - Fix allocation of dead stack variables

Pull Request - State: closed - Opened by vbgl 14 days ago
Labels: bug, ocaml

#1043 - Add ext_eq for words in JByte_array

Pull Request - State: closed - Opened by cassiersg 14 days ago - 1 comment

#1042 - Add support for the -I parameter to jasmin2ec, jasmin-ct and jasmin2tex.

Pull Request - State: open - Opened by cassiersg 15 days ago - 1 comment

#1041 - CI: update nixpkgs & use mathcomp-dev in job coq-master

Pull Request - State: closed - Opened by vbgl 16 days ago - 2 comments
Labels: CI

#1040 - Instruction request: SHA256RNDS2, SHA256MSG1 and SHA256MSG2

Issue - State: open - Opened by ruipedro16 16 days ago - 2 comments

#1039 - Make compatible with current mathcomp

Pull Request - State: closed - Opened by vbgl 16 days ago - 1 comment

#1038 - Migrate CI to github

Pull Request - State: open - Opened by clebreto 16 days ago

#1037 - Homogeneise risc-v test script with arm-m4 testing

Pull Request - State: open - Opened by clebreto 16 days ago - 1 comment

#1036 - broken in Coq CI

Issue - State: closed - Opened by SkySkimmer 17 days ago - 3 comments

#1035 - OCaml: remove dead code

Pull Request - State: closed - Opened by vbgl 20 days ago
Labels: ocaml

#1034 - check-risc-v: avoid non-POSIX (bash) constructions

Pull Request - State: closed - Opened by vbgl 20 days ago - 5 comments

#1033 - ARM semantics of carry flag is wrong for shift instructions

Issue - State: open - Opened by vbgl 20 days ago
Labels: bug, arm

#1032 - EC: add unit tests for extraction

Pull Request - State: closed - Opened by vbgl 21 days ago - 1 comment
Labels: EasyCrypt

#1031 - Location: remove dead code

Pull Request - State: closed - Opened by vbgl 22 days ago
Labels: ocaml

#1030 - x86: add support for VPSIGN (AVX) instructions

Pull Request - State: closed - Opened by vbgl 22 days ago - 1 comment

#1029 - AVX2 instruction request: VPSIGN

Issue - State: closed - Opened by xvzcf 22 days ago

#1028 - Fixing type checking of function return storage type

Pull Request - State: closed - Opened by MrDaiki 23 days ago - 3 comments
Labels: bug, type-checking

#1027 - Regalloc: improve printing of equiv. traces

Pull Request - State: closed - Opened by vbgl 24 days ago
Labels: register-allocation

#1026 - Register allocation error shows useless wrong line information

Issue - State: closed - Opened by vbgl 24 days ago
Labels: register-allocation

#1026 - Register allocation error shows useless wrong line information

Issue - State: closed - Opened by vbgl 24 days ago
Labels: register-allocation

#1025 - Utils: remove dead functions

Pull Request - State: closed - Opened by vbgl 24 days ago
Labels: ocaml

#1024 - reg/stack mismatch at function boundaries

Issue - State: open - Opened by vbgl 24 days ago - 1 comment

#1024 - reg/stack mismatch at function boundaries

Issue - State: open - Opened by vbgl 24 days ago - 1 comment

#1023 - Changing some prettyping errors to be able to ignore them (preparation to fix bug #727)

Pull Request - State: closed - Opened by MrDaiki 26 days ago

#1022 - Adding code editor config directories to .gitignore

Pull Request - State: closed - Opened by MrDaiki 27 days ago

#1021 - Adding info to function

Pull Request - State: closed - Opened by MrDaiki 27 days ago
Labels: ocaml

#1020 - eclib: add [rigid] to hints on 'modulus'

Pull Request - State: closed - Opened by bacelar 27 days ago - 1 comment
Labels: EasyCrypt

#1019 - CI: update nixpkgs

Pull Request - State: closed - Opened by vbgl 28 days ago - 2 comments
Labels: CI

#1018 - minor fix in JWord.ec

Pull Request - State: closed - Opened by bacelar 28 days ago - 5 comments
Labels: bug, EasyCrypt

#1017 - Extending `ptr` semantics to designate specifically memory pointer

Issue - State: closed - Opened by MrDaiki 28 days ago
Labels: enhancement, feature request

#1016 - Adding info to gfunc record type

Issue - State: closed - Opened by MrDaiki 28 days ago - 2 comments
Labels: feature request

#1015 - updating printer `pp_iprog` function to print Cwhile Info

Pull Request - State: closed - Opened by MrDaiki 28 days ago - 7 comments
Labels: bug

#1014 - SCT checker: kill dead vars

Pull Request - State: closed - Opened by vbgl 29 days ago
Labels: SCT checker

#1013 - RISC-V: CT and doit are wrong

Issue - State: open - Opened by eponier 29 days ago
Labels: constant-time, risc-v

#1012 - SCT: drop support for implicit spilling

Pull Request - State: closed - Opened by vbgl 29 days ago
Labels: SCT checker

#1011 - CI: use why3 1.8.0 to build EasyCrypt (dev)

Pull Request - State: closed - Opened by vbgl about 1 month ago
Labels: CI

#1010 - x86: add BLENDV intrinsics

Pull Request - State: closed - Opened by vbgl about 1 month ago

#1009 - x86: add support for VPABS (AVX) instructions

Pull Request - State: closed - Opened by vbgl about 1 month ago

#1008 - AVX2 instruction request: VPABS

Issue - State: closed - Opened by xvzcf about 1 month ago - 2 comments

#1007 - Cryptoline examples fix + tobytes

Pull Request - State: closed - Opened by JoaoDiogoDuarte about 1 month ago

#1006 - CI/coq-master: pin stdlib

Pull Request - State: closed - Opened by vbgl about 1 month ago
Labels: CI

#1005 - Require Ztac to use it in lang/utils.v (for coq/coq#19997)

Pull Request - State: closed - Opened by andres-erbsen about 1 month ago

#1004 - Cryptoline fix examples

Pull Request - State: closed - Opened by JoaoDiogoDuarte about 1 month ago

#1003 - Check in Coq that #[inline]-annotated instructions are gone after unrolling

Pull Request - State: closed - Opened by vbgl about 1 month ago

#1002 - CI: update nixpkgs

Pull Request - State: closed - Opened by vbgl about 1 month ago
Labels: CI

#1001 - fix avx2 shift semantics

Pull Request - State: closed - Opened by bacelar about 2 months ago
Labels: EasyCrypt

#1000 - Add support for translation of AVX2 code

Pull Request - State: open - Opened by MQuaresma about 2 months ago
Labels: cryptoline

#999 - Ec extraction: cleanup leak aux variables

Pull Request - State: closed - Opened by cassiersg 2 months ago - 1 comment

#998 - CI: disable the “cache dependencies” job

Pull Request - State: closed - Opened by vbgl 2 months ago

#997 - CI: disable the “cache dependencies” job

Pull Request - State: closed - Opened by vbgl 2 months ago - 6 comments
Labels: CI

#996 - CI: fix coq-master job

Pull Request - State: closed - Opened by vbgl 2 months ago - 1 comment
Labels: CI

#995 - use byte array in extraction

Pull Request - State: closed - Opened by bgregoir 2 months ago
Labels: EasyCrypt

#994 - Add non-regression test-case for the Easycrypt extraction

Issue - State: open - Opened by lyonel2017 2 months ago

#993 - Printing double semicolons clashes with double underscores

Issue - State: open - Opened by sarranz 2 months ago
Labels: bug

#992 - CI: update nixpkgs

Pull Request - State: closed - Opened by vbgl 2 months ago - 3 comments
Labels: CI

#991 - Update warnings

Pull Request - State: closed - Opened by eponier 2 months ago - 14 comments
Labels: enhancement

#990 - (S)CT checkers: all variables have flow-sensitive (flex) type

Pull Request - State: closed - Opened by vbgl 2 months ago - 1 comment
Labels: constant-time, SCT checker

#989 - SCT-checker: consider variable sharing

Pull Request - State: closed - Opened by vbgl 2 months ago - 1 comment
Labels: bug, SCT checker

#988 - eclib: small refactoring in JWord

Pull Request - State: closed - Opened by vbgl 2 months ago
Labels: EasyCrypt

#987 - Array extraction: use only byte arrays

Issue - State: open - Opened by cassiersg 2 months ago
Labels: refactoring, EasyCrypt

#986 - latex_printer: do not print a blank line

Pull Request - State: closed - Opened by vbgl 2 months ago
Labels: bug

#985 - Make _CoqProject compatible with ProofGeneral

Pull Request - State: closed - Opened by vbgl 2 months ago - 1 comment
Labels: bug

#984 - Unexpected inline int behavior

Issue - State: open - Opened by sarranz 2 months ago - 3 comments
Labels: question

#983 - Set Uniform Inductive Parameters

Pull Request - State: closed - Opened by eponier 2 months ago - 1 comment

#982 - Rebase of 1719489c was incorrect

Pull Request - State: closed - Opened by eponier 2 months ago

#981 - Makefile: change ordering in the test suite

Pull Request - State: closed - Opened by vbgl 2 months ago

#980 - Get rid of recursive types

Pull Request - State: closed - Opened by vbgl 2 months ago

#979 - Check no for loop in coq

Pull Request - State: closed - Opened by vbgl 2 months ago

#978 - Dune: restore standard flags

Pull Request - State: closed - Opened by vbgl 2 months ago

#977 - subst: small clean-up

Pull Request - State: closed - Opened by vbgl 2 months ago - 3 comments

#976 - Add message in the result of jasmin2tex about location of .sty file

Pull Request - State: closed - Opened by lyonel2017 3 months ago - 5 comments

#975 - Propagate errors from compiler in CT checker

Pull Request - State: closed - Opened by sarranz 3 months ago - 3 comments

#974 - Catch exceptions in jasmin2tex

Pull Request - State: closed - Opened by sarranz 3 months ago

#973 - fix ec semantics of shift operators

Pull Request - State: closed - Opened by bgregoir 3 months ago
Labels: bug, EasyCrypt

#973 - fix ec semantics of shift operators

Pull Request - State: open - Opened by bgregoir 3 months ago

#972 - extraction after a given pass

Pull Request - State: closed - Opened by bgregoir 3 months ago

#971 - Fix EC extraction in case on nested loops

Pull Request - State: open - Opened by lyonel2017 3 months ago - 1 comment
Labels: bug, EasyCrypt

#971 - Fix EC extraction in case on nested loops

Pull Request - State: closed - Opened by lyonel2017 3 months ago - 11 comments
Labels: bug, EasyCrypt

#970 - SCT-checker: do not build a (large) list of booleans

Pull Request - State: closed - Opened by vbgl 3 months ago
Labels: SCT checker

#969 - Add metadata to while conditions

Pull Request - State: closed - Opened by vbgl 3 months ago - 2 comments
Labels: bug

#968 - Export global constants

Issue - State: open - Opened by sarranz 3 months ago - 7 comments
Labels: feature request

#967 - toEC: make leakage part of functions return instead of a global variable

Pull Request - State: closed - Opened by cassiersg 3 months ago - 5 comments

#966 - Compiler emits unreachable assembly code

Issue - State: open - Opened by vbgl 3 months ago - 1 comment

#965 - Use liveness info to speed up allocation

Pull Request - State: closed - Opened by eponier 3 months ago - 2 comments

#964 - Update CHANGELOG after release 2024.07.2

Pull Request - State: closed - Opened by vbgl 3 months ago

#963 - Fix printing of underscores in jasmin2tex

Pull Request - State: closed - Opened by sarranz 3 months ago - 8 comments

#962 - MSF and type SCT annotations

Issue - State: open - Opened by sarranz 3 months ago - 3 comments
Labels: bug, question, SCT checker

#962 - MSF and type SCT annotations

Issue - State: open - Opened by sarranz 3 months ago - 3 comments
Labels: bug, question, SCT checker

GitHub / jasmin-lang/jasmin issues and pull requests