59f9ebc59e
From vaptvupt-codec tag v2.65.3. Output is byte-identical to 2.65.0 (same ratio, wire format v1.6 unchanged) but extreme-mode encode is ~1.6-2x faster (Sprint 132 optimal-parser speedup) and the extreme prepass window allocation is capped at wlog=20 = 8 MiB virtual instead of up to 128 MiB (Sprint 133 memory hygiene). Our AVX2 offset-read decoder guard is now UPSTREAM (dropped from the local patch set); the ANS safe-zone 2*SAFEZONE_MAX_RUN reserve is re-applied on top (still not upstream). make check 16/16, KAT 16/16, cross- version roundtrip with 5.1.0 archives verified.
43 lines
1.2 KiB
C
43 lines
1.2 KiB
C
/*
|
|
* SPDX-License-Identifier: AGPL-3.0-or-later
|
|
* Copyright (c) 2026 Cristian Cezar Moisés
|
|
*
|
|
* Zupt — ACSL Custom Predicates for Frama-C/WP
|
|
*
|
|
* Usage: frama-c -wp -wp-rte -wp-model Typed+Cast
|
|
* -cpp-extra-args="-Iinclude -Isrc" src/zupt_crypto.c
|
|
*/
|
|
#ifndef ZUPT_ACSL_H
|
|
#define ZUPT_ACSL_H
|
|
|
|
#ifdef __FRAMAC__
|
|
#include <stdint.h>
|
|
|
|
/*@ predicate ValidBuffer{L}(uint8_t *p, size_t n) =
|
|
@ \valid_read(p + (0..n-1)) &&
|
|
@ \initialized(p + (0..n-1));
|
|
@
|
|
@ predicate ValidWriteBuffer{L}(uint8_t *p, size_t n) =
|
|
@ \valid(p + (0..n-1));
|
|
@
|
|
@ predicate Separated2(uint8_t *a, size_t an,
|
|
@ uint8_t *b, size_t bn) =
|
|
@ \separated(a + (0..an-1), b + (0..bn-1));
|
|
@
|
|
@ predicate KeyWiped{L}(uint8_t *k, size_t n) =
|
|
@ \forall integer i; 0 <= i < n ==> \at(k[i],L) == 0;
|
|
@
|
|
@ predicate ValidKey{L}(uint8_t *k, size_t n) =
|
|
@ ValidBuffer{L}(k, n) && n == 32;
|
|
@
|
|
@ predicate ConstantTimeCompare{L}(uint8_t *a, uint8_t *b,
|
|
@ size_t n) =
|
|
@ \forall integer i; 0 <= i < n ==>
|
|
@ \initialized(\at(a+i,L)) && \initialized(\at(b+i,L));
|
|
@
|
|
@ predicate MACValid{L}(uint8_t *mac) =
|
|
@ ValidBuffer{L}(mac, 32);
|
|
*/
|
|
#endif /* __FRAMAC__ */
|
|
|
|
#endif /* ZUPT_ACSL_H */
|