Certifying derivation of state machines from coroutines

One of the biggest implementation challenges in security-critical network protocols is nested state machines. In practice today, state machines are either implemented manually at a low level, risking bugs easily missed in audits; or are written using higher-level abstractions like threads, depending on runtime systems that may sacrifice performance or compatibility with the ABIs of important platforms (e.g., resource-constrained IoT systems). We present a compiler-based technique allowing the best of both worlds, coding protocols in a natural high-level form, using freer monads to represent nested coroutines , which are then compiled automatically to lower-level code with explicit state. In fact, our compiler is implemented as a tactic in the Coq proof assistant, structuring compilation as search for an equivalence proof for source and target programs. As such, it is straightforwardly (and soundly) extensible with new hints, for instance regarding new data structures that may be used for efficient lookup of coroutines. As a case study, we implemented a core of TLS sufficient for use with popular Web browsers, and our experiments show that the extracted Haskell code achieves reasonable performance.

State-Space Measurement Update for GNSS/INS Integrated Navigation

This paper theoretically derives the equivalence conditions for the loosely and tightly coupled GNSS/INS integration algorithms. Firstly, the equivalence is proved when using single epoch GNSS measurements, which means the GNSS processor provides standalone solution. Then, the equivalence proof is further extended for the filtering solutions, which are usually applied for differential GNSS and precise point positioning. Based on these, different state and measurement models for GNSS/INS integration navigation are summarized, and natural differences among these models are discussed. This indicates that once the same measurement and predict information are used, the integration would be equivalent no matter what kind of coupling schemes are used. A flight dataset with GNSS and tactical IMU data is used to evaluate the equivalence and discrepancies among four different measurement models, and the results confirm the theoretical derivations.

A note on the polynomial Freĭman–Ruzsa conjecture over ℤ

The polynomial Freĭman–Ruzsa conjecture over the integers is often phrased in terms of convex progressions. We give an alternative, apparently stronger formulation in terms of the more restrictive “ellipsoid progressions”, and show that these formulations are in fact equivalent. The key input to the equivalence proof comes from strong results in asymptotic convex geometry.

REVERSE MATHEMATICS, YOUNG DIAGRAMS, AND THE ASCENDING CHAIN CONDITION

LetSbe the group of finitely supported permutations of a countably infinite set. Let$K[S]$be the group algebra ofSover a fieldKof characteristic 0. According to a theorem of Formanek and Lawrence,$K[S]$satisfies the ascending chain condition for two-sided ideals. We study the reverse mathematics of this theorem, proving its equivalence over$RC{A_0}$(or even over$RCA_0^{\rm{*}}$) to the statement that${\omega ^\omega }$is well ordered. Our equivalence proof proceeds via the statement that the Young diagrams form a well partial ordering.

The Equivalence Proof of Two Methods for Foundation Excitation

In this paper, the two methods for the finite element analysis of foundation excitation would be proved mathematically equivalent. Although the two methods, i.e. the method of degree-of-freedom transformation and the Lagrange multiplier method, are absolutely different in appearance, but their mathematical essence would be proved completely identical. In other words, although the equations derived from the two methods have different degree-of-freedoms, i.e. the latter much more than the former, while in essence they could be deduced from each other and vice versa. And finally a numerical example will be presented and discussed to demonstrate the correctness of the present theory.